Formal Analysis of Single WAIT VHDL processes
for Semantic Based Synthesis

Ludovic Jacomme, Frédéric Pétrot and Rajesh K. Bawa
Département ASIM, LIP6
Université Pierre et Marie Curie
4 place Jussieu, F-75252 Paris Cedex 05
France
{Ludovic.Jacomme, Frederic.Petrot, Rajesh.Bawa}@lip6.fr

Abstract:

The problem of formally identifying flipflops, latches and three-state elements within VHDL descriptions of hardware systems is tackled in this paper. Due to the simulation based semantics of VHDL, the existing synthesis tools rely on explicit templates to guarantee memorizing element inference to avoid a complex formal analysis. Opposed to the pattern matching approach of the commercial tools, the approach proposed here is based on a formal representation of VHDL in terms of Interpreted Petri Nets (IPN). A Petri Net preserving the simulation semantic is build as a result of VHDL compilation. In order to simplify the formal recognition of the memorizing elements appearing in the description, the Petri net is reduced to a unique minimal form. This reduction phase has two different constraints, on the one hand to preserves the VHDL semantic and on the other hand to preserve as much as possible all intermediates equations, as required for an efficient synthesis process. Ultimately a set of equations is extracted, and a formal analysis is performed on all cyclic VHDL symbol assignments. The result is a register transfer level VHDL description, synthesizable by any existing synthesis tools. This methodology has been implemented and is illustrated on a representative set of simple VHDL descriptions.

Introduction

Existing synthesis tools such as the Synopsys VHDL Compiler [2] or Cadence Synergy [3] are able to treat sophisticated VHDL descriptions. However, they all impose their own description style for flipflops, latches or tristates inference. This allows the tool to avoid a complex analysis due to the underlying simulation semantic of VHDL [1]. In this work, we tackle the problem of sequential - and three-state - element identification without ressorting to templates but relying on a formal approach.

Formalisms were initially elaborated for the integration of formal verification techniques in the VHDL based circuit design methodology [4,7,8,9,10]. Some formalisms emerging lately are usable for the synthesis of VHDL descriptions [5,11,13,14,17]. Those applications consider a less restricted subsets of VHDL than the ones using templates and pattern matching techniques, but as far as we know, no general method for latch inference has been presented.

To solve this problem, we use a formal model based on Interpreted Petri Nets (IPN) [15]. Our model is an enhancement of the one defined in [5] that has been extended to be applicable for synthesis. We propose the use of an intermediate synthesis oriented formal model whose goal is specifically to alleviate the constraints on the programming style. We also guarantee that the behavioral simulation is identical before and after synthesis when the process is synthesizable.

Section 2 presents our synthesis oriented formal model based on Petri Nets. Section 3 deals with some of the main aspects of the memorizing elements recognition after the compilation into our formal model. Section 4 presents with experimental results and we conclude and present future prospects in Section 5.

Compilation of VHDL descriptions to Petri Nets

The VHDL description we consider is supposed to be elaborated. It is a collection of processes communicating through signals. In particular, all concurrent statements other than processes are supposed to be replaced by their equivalent process. All call statements are replaced by the body of the called procedure or function, by renaming the formal parameters with actual called arguments and by importing the local variables of the called function or procedure. The following restrictions have to be also satisfied :

1. The types and functions defined in the IEEE 1164 standard libraries, are the only one supported.
2. The temporal clauses are excluded both in signal assignment and WAIT statement.

We are not interested in the VHDL compilation aspect, so we can restrict the VHDL subset to a minimal subset, as long as it is sufficient to illustrate all critical examples for the memorizing elements recognition.

Each VHDL process can be seen as a synchronized automaton, where changing the state induces some transformations of internal variable's values and signal's drivers. Thus a process can be easily represented as a Interpreted Petri Net (IPN) [14,7]. Its translation should preserve the simulation semantic, the intermediate information relevant to synthesis, the execution's sequentiality of the process body and also the vectorized symbols.

Presentation of the Petri Net Formalism

The Petri Net is made of a control part and a data part. The control part represents each VHDL processes and their synchronization mechanisms. The data part represents the informations concerning all the symbols manipulated in the VHDL description such as constants, variables or signals.

The VHDL data part

An element of a set $\mathit{Data}$ is associated to each VHDL variable and signal of the description. It represents the variable or signal attributs, and the three subsets such that $\mathit{Data}~=~\{S,V,C\}$ are defined as follows :

• $S$ is the set of all signals $s$. Each element $s$ is a triplet $(s_\mathit{eff},s_\mathit{evt},s_\mathit{drv})$, and defined as follows : $s_\mathit{eff}$ the effective value of $s$, $s_\mathit{evt}$ its event attribute and $s_\mathit{drv}$ its driving value.
• $V$ is the set of all variables $v$ of process $p$. Each element $v$ is defined by $v~=~v^p_{val}$, where $v^p_{val}$ represents the current value of $v$.
• $C$ is the set of all constants $c$. Each element $c$ is defined by $c~=~c_{val}$, where $c_{val}$ is the constant value of $c$.

The control part

The control part is an Interpreted Petri Net representing the sequential instructions of each process. We distinguish two types of transitions : $T_{exe}$ associated to the EXECUTE phase of the VHDL simulation cycle, and $T_{res}$ corresponding to the RESUME phase :

• We associate a list of ordered sequential assignments to the $T_{exe}$ transitions and eventually a firing condition, called GUARD condition. We assume that given one VHDL symbol, only one assignment to this symbol is permitted in a transition. The sequential assignments list modifies the data part of the Petri Net, with the same semantic than the execution of a VHDL sequential statement. If the transition $T_{exe}$ has a GUARD condition, the firing of $T_{exe}$ is possible only if it is true.
• The $T_{res}$ transitions correspond to the implicit or explicit wait statements of each process. They are used firstly to stop the process when it reaches one and secondly to wake it up on signal's events occurrences. The firing of a $T_{res}$ transition is possible only when an event occurs on its sensitivity list.

We note $\mathcal{B}$ the boolean set, and $\mathcal{B}_F$ the set of all boolean functions with parameters in is the power set of$\mathit{Data}$ noted $\mathcal{P}(\mathit{Data})$.

The Petri Net $\mathit{PN}_{Data}$ is defined by : $<P,T,\mathit{ArcPlace},\mathit{ArcTrans},G,\mathit{Trf},\mathit{Asg},M0>$ where

• $P$ is the set of all places.
• $T$ is a set of all transitions, $T~=~T_{exe}~\cup~T_{res}$ such that $T_{exe}~\cap~T_{res}~=~\varnothing$. $T_{exe}$ is the set of all transitions modifying elements of $\mathit{Data}$. $T_{res}$ is the set of all transitions sensible to the appearance of events on elements of $S$.
• $\mathit{ArcPlace}~:~P~\times~T~\rightarrow~\mathcal{B}$ defined as $\mathit{ArcPlace}(p,t)$ is true iff an arc exists from $p$ to $t$. A transition $t$ has got a maximum of one predecessor.
• $\mathit{ArcTrans}~:~T~\times~P~\rightarrow~\mathcal{B}$ defined as $\mathit{ArcTrans}(t,p)$ is true iff an arc exists from $t$ to $p$. A transition $t$ has got a maximum of one successor.
• $G~:~T~\rightarrow~\mathcal{B}$, $G(t)~\in~\mathcal{B}_F$ is the guard condition of $t$.
• $\mathit{Trf}~:~T~\rightarrow~\mathcal{P}(\mathit{Data})~\times~\mathcal{B}_F$, where $\mathit{Trf}(t)$ is an ordered set of couples $\{(d_i,f_i)\}$ with $d_i~\in~\mathit{Data}$ and $f_i~\in~\mathcal{B}_F$. $\mathit{Trf}(t)$ indicates the modification applied to a data $d$ while firing the transition $t$.
• $\mathit{Asg}~:~T~\rightarrow~\mathcal{P}(\mathit{Data})$ is the set of all modified symbols when the transition $t$ is fired.
• $M0$ is the initial marking of the Petri Net.

Principles of the VHDL compilation to Petri Nets

The compilation builds a sub Petri Net for each VHDL process. All sequential statements are individually mapped into an equivalent sub Petri Net. Those resulting sub Petri Nets are connected together by intermediate places. All VHDL instructions modifying VHDL symbols are associated to the $T_{exe}$ transitions.

Figure 1: VHDL Description of a flipflop

ENTITY DREG IS PORT ( CK, A : in  BIT;        T     : out BIT ) END DREG; ARCHITECTURE BEH OF DREG IS BEGIN   PROCESS( CK )     VARIABLE V : BIT;   BEGIN     IF (CK = '1') THEN       V := A;      END IF;     T <= V;   END PROCESS; END BEH;

Data = { (A.eff, A.drv, A.evt),          (CK.eff, CK.drv, CK.evt),          (V.val),          (TEST0.val),          (T.eff, T.drv, T.evt) } G(t0) = CK.evt G(t2) = TEST0.val G(t3) = NOT TEST0.val Trf(t1) = { TEST0.val, (CK.eff = '1') } Trf(t4) = { V.val, A.eff } Trf(t6) = { T.drv, V.val } Asg(t1) = { TEST0.val } Asg(t4) = { V.val } Asg(t6) = { T.drv }

All implicit or explicit statements of synchronization are translated to their equivalent $T_{res}$ transitions. The three main transformation principles are the following :

• A variable or a signal assignment is translated into a single transition $t$. The assignment it represents is associated to this transition $t$ as a set of couples $(d~\in~\mathit{Data},~f~\in~\mathcal{B}_f)$ in $\mathit{Trf}(t)$ : $\mathit{Trf}(t)~\leftarrow~\mathit{Trf}(t)~\cup~\{(d,f)\}$ where $d$ is the assigned VHDL symbol and $f$ a boolean function. $\mathit{Asg}(t)$ contains the set of all modified VHDL symbols when the transition $t$ is fired.
• A control statement, such as an IF, a CASE or a LOOP is mapped into a sub Petri Net representing its structure. An IF or a CASE statement is modeled by a first place followed by a set of guarded transitions. Expression of each alternative is associated to the corresponding transition as its guard condition. The end of all sub Petri Nets of each branch converge to an output place representing the END IF or the END CASE statement.


A FOR is first modeled with a sub Petri Net representing the initialization of the loop variable, and one corresponding to the increment of this variable.

For a WHILE or a FOR statement, a sub net corresponding to the test statement of the loop is build. This last sub net is build as an IF statement.

For all the kinds of loops, the sub net of the loop body is build. This sub net is connected respectively to the increment sub net for a loop of type FOR, to the test sub net for a WHILE and to the beginning of the loop for a simple LOOP statement.

Other statements such as NEXT and EXIT are treated in a similar fashion.

• A WAIT statement is mapped into a single transition. The sensitivity list of the transition is equal to the sensitivity list of the WAIT statement. If there is an until clause in the WAIT statement, the UNTIL condition is mapped like the equivalent LOOP and EXIT statement.

 

 

A VHDL description of a flipflop and the corresponding unreduced Petri Net and its $\mathit{Data}$ structure are given on Figure 1.

A certain number of reduction techniques [6,4,5] allow to obtain a smaller Petri Net, which preserves the underlying VHDL semantic and make the net easier to manage. The reduction method of the Petri Net can be different depending on the target application. For synthesis, we need to keep all sequences of execution and we also try to obtain a minimal reduced form, relatively independent of the initial description style.

We can apply two techniques of reduction. The first one called local reduction is based on the VHDL instructions structure. This local reduction takes place each time a VHDL instruction is translated. It is not always possible [5] to reduce completely a Petri Net with this first technique. Thus we have to apply another type of reduction, called global reduction, once the entire Petri Net is obtained.

Local reduction of sub Petri net representing VHDL processes

The local reduction is based on two basic algorithms that attempt to either merge several alternative transitions or two consecutive transitions called respectively lateral reduction and sequential reduction. In the following we note $V~=~V^\mathit{red}~\cup~V^\mathit{ini}$ where $V^\mathit{red}$ is set of all intermediate variables added during the reduction process and $V^\mathit{ini}$ the set of variables which have been declared in the initial VHDL description. We have $V^\mathit{red}~=~V^\mathit{drv}~\cup~V^\mathit{var}$ where the sets $V^\mathit{drv}$ and $V^\mathit{var}$ are respectively the set of possible signal's driver values, and the set of possible variable's values encountered during the reduction process. Those intermediate variables have the property to be assigned only once in a VHDL process.

In what follows, we assume that each process contains one and only one WAIT statement, since the semantic of VHDL imposes this fact for flipflop, latches and three-state buffers.

Lateral reduction

When applicable this reduction merges several alternative transitions and results in a single transition which is equivalent to the merged transitions. This reduction is applied after the translation of each CASE or IF statement, if they do not contain a WAIT statement. A lateral reduction can be applied to a set of transitions $T_\mathit{lat} = \{ t_1,..., t_n \}$ iff the following conditions hold :

• All transitions are of type EXECUTE and have a guard condition.
• $T_\mathit{lat}$ is equal to the set of all transitions which have a unique and identical preceding place $p_1$.
• The set of all the successors of $p_1$ is equal to $T_\mathit{lat}$.
• $T_\mathit{lat}$ is equal to the set of all transitions which have a unique and identical following place $p_2$.
• The set of all the predecessors of $p_2$ is equal to $T_\mathit{lat}$.

The lateral reduction of $T_\mathit{lat}$, replaces all transitions $t_i$ by an unique transition $t_\mathit{lat}$ in the sub Petri Net. The transition $t_\mathit{lat}$ is built as follow :

1. A transition $t_\mathit{lat}$ is added in $T_\mathit{exe}$ and two arcs from $p_1$ to $t_\mathit{lat}$ and from $t_\mathit{lat}$ to the place $p_2$ are created.
2. The guard condition of $t_{lat}$ is set to empty.
3. The data transformation defined by $\mathit{Asg}(t_\mathit{lat})$ and $\mathit{Trf}(t_\mathit{lat})$ is built.
4. The set of transitions $T_\mathit{lat}$ is deleted from $T$ and so are all associated arcs.

The construction of the data transformations is done using the following algorithm :

1. The transition $t_\mathit{lat}$ modifies all symbols assigned by each $t_i$ : $\mathit{Asg}(t_\mathit{lat})~\leftarrow~\bigcup_{i=1}^n~\mathit{Asg}(t_i)$.
2. The assignment of each intermediate variables appearing in each $t_i$ must be first added in the ordered set $\mathit{Trf}(t_\mathit{lat})$ : $\forall~t_i~\in~T_\mathit{lat}$, $\forall~(d_i,f_i)~\in~\mathit{Trf}(t_i)~\vert~d_i~\in~V^\mathit{red},\mathit{......t_\mathit{lat})~\leftarrow~\mathit{Trf}(t_\mathit{lat})~\cup~\{~(d_i,~f_i)~\}$
3. A combination of all others assignment of each VHDL symbols $d_i$ for each transition $t_i$ must be performed using the following method : $\forall~t_i~\in~T_\mathit{lat}$, $\forall~(d_i,f_i)~\in~\mathit{Trf}(t_i)~\vert~ d_i~\not\in~V^\mathit{red}$ :
1. $f_i^{lat}~\leftarrow~[G(t_i)~\wedge~f_i]$, $\mathit{Trf}(t_i)~\leftarrow~\mathit{Trf}(t_i)~-~\{(d_i,f_i)\}$
2. $\forall~t_j~\in~T_\mathit{lat}$, $t_i~\neq~t_j$ :

if $\exists (d_i, f_j) \in \mathit{Trf}(t_j)$ then $f_i^{lat}~\leftarrow~f_i^{lat} \vee [ G(t_j) \wedge f_j ]$, $\mathit{Trf}(t_j)~\leftarrow~\mathit{Trf}(t_j) - \{ (d_i, f_j) \}$
if $\nexists (d_i, f_j) \in \mathit{Trf}(t_j)$ then $f_i^{lat}~\leftarrow~f_i^{lat} \vee [ G(t_j) \wedge d^{lat}_i ]$,
where $d_i^{lat}$ is the driver of $d_i$ if $d_i$ is a signal and the current value of the variable $d_i$ otherwise.

Figure 2: An example of lateral reduction

This reduction has on the one hand propagated guard conditions of each $t_i$ in each assignment statement and on the other hand gathered all assignment statements for each symbol. The sequential execution of the transition $t_\mathit{lat}$ is behaviorally equivalent of the execution of each alternative transitions $t_i$, knowing its guard condition is true. This reduction is illustrated on a simple Petri Net on Figure 2.

Sequential reduction

When applicable, this reduction merges two consecutive transitions and results in a single transition whose behavior is equivalent to the one of the merged transitions. It is applied systematically after the translation of each signal or variable assignment. A notable difference with the one defined in [5] is that the sequence of instructions is preserved by introducing intermediate variables $V^\mathit{var}$ and $V^\mathit{drv}$. These intermediate variables are used to share subexpressions for efficient resource allocation and boolean optimization in later synthesis stages. Sequential reduction can be applied to an ordered set of two transitions $T^\mathit{seq}~=~\{t_1,t_2\}$ iff the following conditions hold :

• The two transitions $t_1$ and $t_2$ are of the type EXECUTE.
• The two transitions are different and sequentially connected with two intermediate places $p_1$ and $p_2$.
• The place $p_1$ has a unique predecessor $t_1$ and a unique successor $t_2$.
• The place $p_2$ has a unique predecessor $t_2$.

The sequential reduction replaces the two transitions $t_1$ and $t_2$ by a unique transition $t_\mathit{seq}$ in the sub Petri Net. We note $P^\mathit{seq}~=~\{p_1,p_2\}$ the ordered set of the two places $p_1$ and $p_2$ previously defined. We note also $p_0~\in P$ the place preceding transition $t_1$. The resulting transition $t_\mathit{seq}$ is built as follows :

1. A transition $t_\mathit{seq}$ is added in $T_\mathit{exe}$ and two arcs from $t_\mathit{seq}$ to $p_2$ and from $p_0$ to $t_\mathit{seq}$ are created.
2. The guard condition of $t_\mathit{seq}$ is the equal to the guard condition of $t_1$.
3. The data transformation defined by $\mathit{Asg}(t_\mathit{seq})$ and $\mathit{Trf}(t_\mathit{seq})$ is built.
4. The place $p_1$ and the two transitions $t_1$ and $t_2$ are deleted and all associated arcs are alose removed.

We note $V^\mathit{var}_\mathit{seq}~=~\{(v~\in~V^\mathit{ini},v^\mathit{var}~\in~V^\mathit{var})\}$, where $v^\mathit{var}$ is a new variable that shall replace $v$. We note $V^\mathit{drv}_\mathit{seq}~=~\{(s~\in~S,v^\mathit{drv}~\in~V^\mathit{drv})\}$, where $v^\mathit{drv}$ is a new variable associated to the driver of $s$. The data transformation defined by $\mathit{Asg}(t_\mathit{seq})$ and $\mathit{Trf}(t_\mathit{seq})$ is build as follows :

1. First we set initial value : $\mathit{Trf}(t_\mathit{seq})~\leftarrow~\varnothing$, $\mathit{Asg}(t_\mathit{seq})~\leftarrow~\varnothing$, $V^\mathit{drv}_\mathit{seq}~\leftarrow~\varnothing$, and $V^\mathit{var}_\mathit{seq}~\leftarrow~\varnothing$.
2. Then we proceed to the exploration of all assignments of $t_1$, $\forall~(d_i, f_i)~\in~\mathit{Trf}(t_1)$ we do :
1. $\mathit{Asg}(t_\mathit{seq})~\leftarrow~\mathit{Asg}(t_\mathit{seq})~\cup~\{d_i\}$.
2. if $d_i \in V^\mathit{ini}$ then we add a new temporary variable : $V^\mathit{var}~\leftarrow~V^\mathit{var} \cup \{ d_i^\mathit{var}) \}$, and we build two new assignment statements : $\mathit{Trf}(t_\mathit{seq})~\leftarrow~\mathit{Trf}(t_\mathit{seq})~\cup\{(d_i^\mathit{var},f_i),(d_i,d_i^\mathit{var})\}$

$V^\mathit{var}_\mathit{seq}~\leftarrow~V^\mathit{var}_\mathit{seq}~\cup~\{(d_i,d_i^\mathit{var})\}$, $\mathit{Asg}(t_\mathit{seq})~\leftarrow~\mathit{Asg}(t_\mathit{seq})~\cup~\{d_i^\mathit{var}\}$.
3. if $d_i \in S$ then we add also a new temporary variable : $V^\mathit{drv}~\leftarrow~V^\mathit{drv} \cup \{ d_i^\mathit{drv}) \}$, and we build two new assignment statements : $\mathit{Trf}(t_\mathit{seq})~\leftarrow~\mathit{Trf}(t_\mathit{seq})~\cup\{(d_i^\mathit{drv},f_i),(d_i,d_i^\mathit{drv})\}$

$V^\mathit{drv}_\mathit{seq}~\leftarrow~V^\mathit{drv}_\mathit{seq}~\cup~\{(d_i,d_i^\mathit{drv})\}$, $\mathit{Asg}(t_\mathit{seq})~\leftarrow~\mathit{Asg}(t_\mathit{seq})~\cup~\{d_i^\mathit{drv}\}$.
4. in the others cases we only duplicate the assignment statement in the new transition $t_\mathit{seq}$ : $\mathit{Trf}(t_\mathit{seq})~\leftarrow~\mathit{Trf}(t_\mathit{seq}) \cup\{ (d_i, f_i) \}$.
3. Let $\Delta(f_i)~=~\{d~\in~\mathit{Data}$, where $d$ appears in $f_i \}$ the support of the boolean function $f_i$.

We proceed to the exploration of all assignment of $t_2$, $\forall~(d_i,f_i)~\in~\mathit{Trf}(t_2)$ :
1. We must rename, in transition $t_2$, all references to previous variables assigned in transition $t_1$. $\forall~v~\in~V^\mathit{ini}~\vert~v_{val}~\in~\Delta(f_i)$ and $\exists~(v,~v^\mathit{var})~\in~V^\mathit{var}_\mathit{seq}$, then rename $v_{val}$ by $v^\mathit{var}_{val}$ in the boolean function $f_i$.
2. We must also rename in transition $t_2$, all references to previous signal's driver, assigned in transition $t_1$. $\forall~s~\in~S~\vert~s_\mathit{drv}~\in~\Delta(f_i)$ and $\exists~(s,~v^\mathit{drv})~\in~V^\mathit{drv}_\mathit{seq}$, then rename $s_\mathit{drv}$ by $v^\mathit{drv}_{val}$ in the boolean function $f_i$.
3. given one symbol, only one assignment to this symbol is permitted in a transition, so we erase all previous assignment of symbols of $t_1$ if they appear in $t_2$.

if $d_i \in \mathit{Asg}(t_\mathit{seq})$ then $\exists~(d_i, f_j)~\in~\mathit{Trf}(t_\mathit{seq})$, $\mathit{Trf}(t_\mathit{seq})~\leftarrow~\mathit{Trf}(t_\mathit{seq})~-~\{(d_i,f_j)\}$
4. $\mathit{Trf}(t_\mathit{seq})~\leftarrow~\mathit{Trf}(t_\mathit{seq})~\cup~(d_i, f_i)$

Figure 3: An example of two consecutive sequential reductions

We only have introduced auxiliary variables, and removed unused assignment statements in transition $t_\mathit{seq}$. The sequential execution of two consecutive transitions $t_1$ and $t_2$, is behaviorally equivalent to the execution of $t_\mathit{seq}$. This reduction technique is illustrated on Figure 3.

Global reduction of sub Petri Net representing VHDL processes

This reduction is purely based on Petri Net traversal. This traversal is done by identifying a set of reducible sequences of transitions. A set of transition $\mathit{Seq}(t_\mathit{from}, t_\mathit{to}) = \{ t_1, ...,t_n \}$ is called a sequence of transitions iff the following conditions hold :

• We note $t_0 = t_\mathit{from}$, $t_{n+1} = t_\mathit{to}$. The two transitions $t_\mathit{from}$ and $t_\mathit{to}$ are of type RESUME.
• Transitions included between $t_\mathit{from}$ and $t_\mathit{to}$ are of type EXECUTE.
• Transitions of the sequence are sequentially connected.

A $\mathit{Seq}(t_\mathit{from}, t_\mathit{to})$ is said to be completely reduced or a minimal sequence iff $\vert\mathit{Seq}(t_\mathit{from},t_\mathit{to})\vert~\le~1$.

Because we consider VHDL process with only one WAIT statement, the two transitions $t_\mathit{from}$ and $t_\mathit{to}$ are identicals. All the sequences of the process are treated one by one using sequential reduction technique. The resulting reduced sequences, which have the same initial and last transitions are merged by applying a lateral reduction technique. Let $\mathit{Seq}^\mathit{Proc}_{all} = \{ \mathit{Seq}(t_\mathit{from},t_\mathit{to}), \forall t_\mathit{from}, t_\mathit{to} \in T^\mathit{Proc}_{res}\}$, the set of all sequences of a VHDL process $\mathit{Proc}$. we note $p_\mathit{from}$ the successor of $t_\mathit{from}$, and$t_\mathit{to}$ the predecessor of $t_\mathit{to}$. The global reduction on a process is defined as follows :

For all the sequences $\mathit{Seq}(t_\mathit{from}, t_\mathit{to})$ of a process $\mathit{Proc}$,

1. A transition $t_\mathit{from}^{to}$ is added in $T_{exe}$ and two arcs from $p_\mathit{from}$ to $t_\mathit{from}^{to}$ and from $t_\mathit{from}^{to}$ to $p_\mathit{to}$ are created.
2. All the guard conditions of each transition of the sequence are merged in a unique guard :

$G(t_\mathit{from}^{to})~\leftarrow~\bigcup_{i=1}^n G(t_i)$ with $t_i~\in~\mathit{Seq}(t_\mathit{from},t_\mathit{to})$.
3. The new assignment statement list $\mathit{Trf}(t_\mathit{from}^{to})$ is the result of all successive sequential reduction of all couples $(t_i,t_{i+1})$, with $G(t_i)$ and $G(t_{i+1})$ sets to $\varnothing$.
4. If it exists several transitions $t_\mathit{from}^{to}$ then a lateral reduction is applied on all transitions $t_\mathit{from}^{to}$.

The global reduction transform each sequences, from a WAIT statement to another WAIT statement, in a single transition. All possible execution paths are preserved using multiplexors instead of branches, so the resulting Petri Net has the same behavior than the initial one.

The Petri Net can be reduced using exclusively the global reduction, but the computational complexity depends on the number of sequences $n$ to be minimized in $O(n^2)$. The objective of the local reduction is to reduce the number of sequences necessary for the global reduction. On a 32 bit micro-programmed processor DLXm control automaton [12], the global reduction without local reduction leaves with 64 sequences to be minimized, while local reduction leaves with only one.

Figure 4: Reduction of the sub Petri Net

Such an example is shown on Figure 4, where all sequences are minimized during local reduction. At this stage we have obtained a minimal Petri Net and the next section will deal with the memorizing element recognition from this reduced Petri Net.

Synthesis of VHDL processes with one WAIT statement

In this paper we are interested in processes with only one WAIT statement. Nevertheless our reduction technique is useful to synthesized process with more than one WAIT, but this is part of another study.

The synthesis of equivalent single wait processes differs between different synthesis tools. For example the four process given in Figure 5 are functionally equivalent.

Figure 5: Four equivalent VHDL Descriptions of a D-register

ENTITY DREG IS PORT ( CK, A : in  BIT;        T     : out BIT ) END DREG; ARCHITECTURE BEH_1 OF DREG IS BEGIN   PROCESS( CK )     VARIABLE R : BIT;   BEGIN     IF ((CK = '1') AND CK'EVENT)     THEN R := A;      END IF;     T <= R;   END PROCESS; END BEH_1;	ARCHITECTURE BEH_2 OF DREG IS   BEGIN     PROCESS     BEGIN       LOOP         WAIT ON CK;         NEXT WHEN (CK /= '1');         T <= A;       END LOOP;     END PROCESS;   END BEH_2;
ARCHITECTURE BEH_3 OF DREG IS BEGIN   PROCESS( CK )   BEGIN     IF (NOT(CK='0') AND CK'EVENT)     THEN       T <= A;     END IF;   END PROCESS; END BEH_3;	ARCHITECTURE BEH_4 OF DREG IS   BEGIN     PROCESS( CK )       VARIABLE R : BIT;     BEGIN       IF (CK = '1') THEN         R := A;        END IF;       T <= R;     END PROCESS;   END BEH_4;

They all represent a flipflop as far as VHDL simulation is concerned. Synopsis Synthesis tool [2] is incapable of treating the first three descriptions (Behavioral Compiler Error). However, the fourth one is synthesized as a latch ! Our approach will deduce a flipflop from all the four descriptions.

Once the Petri Net is completely reduced, we obtain a set of equations for each variable and signal of the process. The cyclic equation of the driver $T_\mathit{drv}$ of the signal $T$ derived from all the four descriptions is illustrated on the Figure 6. Identification of the memorizing elements is done in two distinct steps : the analysis of the sensitivity list and the analysis of the equation itself.

Figure 6: The Sub Petri Net of a flipflop and the corresponding data transformations

Data = { (A.eff, A.drv, A.evt),          (CK.eff, CK.drv, CK.evt),          (TEST0.val), (T.eff, T.drv, T.evt) } G(t0) = CK.evt Trf(t1) = { { TEST0.val, (CK.eff = '1') },             { T.drv, (A.eff AND TEST0.val) OR                      (T.drv AND NOT(TEST0.val) } }

Sensitivity list analysis

The analysis of the support of the assigned signal or variable and the sensitivity list of the corresponding process, as shown below, allows us to classify each signal or variable into three distinct classes : un-synthesizable assignment, noncyclic combinatorial assignment and cyclic combinatorial assignment.

Given the couple $(d,f_d)\in~\mathit{Trf}(t_{asg})$, we note $\Delta_+(f_d)$ the extended support of $f_d$, where all intermediate variables $v~\in~V^{red}~\vert~v~\in~\Delta(f)$ are replaced by their own extended support$\Delta_+(f_v)$.

By construction the extended support $\Delta_+(f)$ of the function $f$ contains only symbols of the two sets $S$ and $V~-~V^{red}$. Let $\mathit{Sens}$ the set of all signals $s_i$ that appear in the sensitivity list of the process, we note $\Delta_+^s(f_i)~=~\Delta_+(f_i)\cap\mathit{Sens}$ and we note $\overline{\Delta}_+^s(f_i)~=~\Delta_+(f_i)~-~\Delta_+^s(f_i)$.

An analysis is performed for all useful couples $(d_i, f_i)~\in~\mathit{Trf}(t_{asg})$ with $d_i\not\in V^{red}$ :

1. if $\Delta_+^s(f_i)~=~\varnothing$, then
1. if $d_i \in \Delta_+(f_i)$ it is un-synthesizable
2. or if $\Delta_+(f_i)~=~\varnothing$ it is a constant
3. or if $\overline{\Delta}_+^s(f_i)~=~\varnothing$ it is a combinatorial function
4. and otherwise it is un-synthesizable.
2. if $\overline{\Delta}_+^s(f_i)~=~\varnothing$ then
1. if $d_i \in \Delta_+(f_i)$ it is a cyclic function
2. and otherwise it is a simple combinatorial function.
3. if $\overline{\Delta}_+^s(f_i) \neq \varnothing$ then
1. if $d_i \in \Delta_+(f_i)$ it is a cyclic function,
2. and otherwise it is un-synthesizable

At this stage, we have classified each useful VHDL symbol into the two synthesizable categories : cyclic and noncyclic functions. Noncyclic functions are simply synthesized as combinatorial gates. The next step is to analyze the cyclic equations, that will possibly be synthesized as memorizing elements.

Analysis of cyclic equations

A one bit memorizing element can be modeled typically by a simple state graph, with a first state associated to the value one, and a second associated to the value zero. We treat all the symbols one by one and construct the boolean equations on all the arcs of the state transition graph to determine :

• The memorization condition,
• Eventual oscillation condition,
• Set and reset conditions,
• The equation of the data to be memorized.

The computation of these equations is performed using BDDs [16]. Given a couple $(d_i, f_i)~\vert~d_i \in \Delta_+(f_i)$ and two boolean equations $f^0_i~=~f_i(d_i=0)$ and $f^1_i~=~f_i(d_i=1)$ derived from $f_i$ we have :

• $f^\mathit{Oscil}_i~=~f^0_i \wedge \overline{f^1_i}$ and $f^\mathit{Mem}_i~=~f^0_i \vee \overline{f^1_i}$,
• $f^\mathit{Data}_i~=~f_i \downarrow f^\mathit{Mem}_i$, where $\downarrow$ is the cofactor function,
• $f^\mathit{Set}_i~=~\{ f^s \subseteq f^\mathit{Mem}_i~\vert~(f^s ~=~1) \Rightarrow (f^\mathit{Data}_i~=~1)\}$,
• $f^\mathit{Reset}_i~=~\{ f^r \subseteq f^\mathit{Mem}_i~\vert~(f^r ~=~1) \Rightarrow (f^\mathit{Data}_i~=~0)\}$
• $f^\mathit{Clock}_i~=~f^\mathit{Mem}_i -( f^\mathit{Set}_i \cup f^\mathit{Reset}_i )$.

Once the above equations have been obtained, we proceed further in the analysis to determine the type of hardware necessary for the synthesis :

• if $f^\mathit{Oscil}_i \neq 0 \rightarrow$ an oscillation is possible (undesirable behavior from the designer point of view).
• if $f^\mathit{Mem}_i~=~1 \rightarrow$ the couple $(d_i, f_i)$ is a simple combinatory assignment, the analysis is ended.
• if $f^\mathit{Mem}_i~=~0 \rightarrow$ the symbol $d_i$ is never assigned, it's a constant equal to its elaboration value.
• if $f^\mathit{Set}_i \neq 0$ or $f^\mathit{Reset}_i \neq 0~\rightarrow$ there is a set or reset condition.

An iteration of the previous step may be necessary to remove intermediate variables appearing in the memorizing condition. A more precise analysis has to be performed on the BDDs equations in order to separate the asynchronous, synchronous set or reset conditions, a write enable condition and the clock's edge type :

1. if $\exists~s~\in~S~\vert~s_\mathit{evt}$ appears in $f_i$ then
1. if $\exists~c_i~\vert~f^\mathit{Clock}_i~=~c_i~\wedge~f^\mathit{Enable}_i$, with $c_i~=~s_\mathit{eff}~\wedge~s_\mathit{evt}$ or $c_i~=~\overline{s_\mathit{eff}}~\wedge~s_\mathit{evt}~\rightarrow$ flipflop
2. otherwise $\rightarrow$ un-synthesizable
2. if $\nexists~s~\in~S~\vert~s_\mathit{evt}$ appears in $f_i$
1. if $\Delta_+(f^\mathit{Data}_i)~\subseteq~\mathit{Sens}~\rightarrow$ latch
2. otherwise $\rightarrow$ un-synthesizable

Those new checks have to follow the constraints given by the sensitivity list of the process.

It is important to note that these equations do not depend upon the VHDL description style, since the reduction process achieved a minimal form. The set of equations obtained for the descriptions of Figure 6 are the following :

• $d_i =~T_\mathit{drv}$
• $f_i =~ (A_\mathit{eff}~\wedge~CK_\mathit{eff}~\wedge~CK_\mathit{evt})~\vee~(T_\mathit{drv} \wedge~\overline{(CK_\mathit{eff}~\wedge~CK_\mathit{evt})})$
• $f^0_i =~A_\mathit{eff}~\wedge~CK_\mathit{eff}~\wedge~CK_\mathit{evt}$
• $f^1_i =~A_\mathit{eff}~\vee~\overline{CK_\mathit{eff}}~\vee~\overline{CK_\mathit{evt}}$
• $f^\mathit{Mem}_i =~(CK_\mathit{eff}~\wedge~CK_\mathit{evt})$
• $f^\mathit{Oscil}_i =~f^\mathit{Set}_i~=~f^\mathit{Reset}_i~=~0$
• $f^\mathit{Clock}_i =~(CK_\mathit{eff}~\wedge~CK_\mathit{evt})$
• $f^\mathit{Data}_i =~A_\mathit{eff}$

From this equation all four forms of VHDL process leads to the synthesis of flipflop.

Experimental results

 

Table 1: Experimental results after compilation of 54 VHDL descriptions

Synthesis tools	Error		Warning		Ok
Synopsys Compiler	26	48.5%	11	20%	17	31.5 %
Cadence Synergy	34	63%	0	0%	20	37 %
Our approach	0	0%	0	0%	54	100 %

We have implemented our approach and have applied it to a set of 54 simple VHDL descriptions. We have also used two well known commercial synthesis tools : Synopsys Design Compiler and Cadence Synergy. This set of descriptions is composed of multiplexors, latches and flipflops with various combinations of write enable, asynchronous or synchronous set and reset, rising or falling clock edges. We have written those descriptions by using numerous forms of WAIT, IF, ELSIF and LOOP statements.

In Table 1, the first column gives the name of the synthesis tool. The next two columns give the number and the percentage of VHDL descriptions that have been rejected with an error message by the synthesis tool during the compilation phase. The next two columns give the number and the percentage of descriptions which have been accepted with a warning message. The last two columns give the number and the percentage of descriptions which have been accepted without any message.
 
 

Table 2: Experimental results after synthesis of VHDL descriptions

Synthesis tools	Error
Synopsys Compiler	13	46%
Cadence Synergy	0	0%
Our approach	0	0%

In Table 2, the first column gives the name of the synthesis tool. The next two columns give the number and the percentage of VHDL descriptions that have been accepted during the compilation phases, but that were synthesized incorrectly without any error message by the tool.

The results Tables 1 and 2 underline three important points :

• Those two synthesis tools don't impose the same restrictions on the description style. This is damageable for the designs from a portability point of view.
• The Synopsys Compiler is not able to synthesize properly all the VHDL descriptions accepted during the compilation and analysis phases.
• Our analysis succeed in all cases to recognize the right hardware implantation, whatever the style of description.

Conclusion

We have presented an approach which exploits a formal model of VHDL in terms of Interpreted Petri Nets. Several reductions techniques preserving first the simulation semantic of VHDL and second the informations necessary for an efficient synthesis, have been developed.

Based on the reduced Petri Net, we are able to determine if a simple process, with only on WAIT statement, can be synthesized. This is done by the analysis of the cyclic and noncyclic data equations attached to the Petri Net, taking into account the sensitivity list of the process. If the process is synthesizable, we apply a formal recognition technique to find out the correct hardware required to implement the sequential behavior of the process.

This approach has been implemented and experimented on a set of 54 simple VHDL descriptions, whose goal is to illustrate many ways to describe the same sequential VHDL behavior, such as latches, flipflops, multiplexors or tristates.

Future use of these techniques include first the multi-wait processes synthesis, where both the formal model and the recognition algorithm are useful, and second, the translation to and from VERILOG as the existing translators make use of syntax based rules instead of taking into account the language semantic.

Bibliography

1

VHDL LRM (1992) IEEE Standard VHDL Language Reference Manual in IEEE Std 1076-1987.

2

Synopsys Inc. (1988-1996) VHDL Compiler v3.5a

3

Cadence System Inc. (1997) Synergy v3.0

4

Encrenaz E. (1995) Une Méthode de vérification de propriétés de programmes VHDL basée sur des modèles formels de réseaux de Petri. PhD thesis (in French), Pierre and Marie Curie University, Paris.

5

Bawa R. K. (1996) An Automated Framework for the Formal Verification and Analysis of Systems Described in VHDL, PhD thesis (in French), Pierre and Marie Curie University, Paris.

6

Müller J. and Krämer H. (1993) Analysis of Multi-Process VHDL Specifications with a Petri Net Model. in Proceedings of the Euro-Dac'93, 474-479, Germany.

7

Olcoz S. and Colom M. (1993) A Petri Net Approach for the Analysis of VHDL Descriptions, in Proceedings of the CHARME.

8

Déharbe D. and Borrione D. (1993) A Qualitative Finite Subset of VHDL and Semantics, in Technical Report of IMAG Institute, RR943.

9

Dohmen G. and Hermann R. (1995) A Deterministic Finite-State Model for VHDL, in formal Semantics for VHDL, edited by C. Delgado Kloos and P. T. Breur, Kluwer Academic Publishers.

10

Van Tassel. J. P. (1993) femto VHDL: The Semantics of a Subset of VHDL and Its Embedding in the HOL Proof Assistant, PhD Thesis, University of Cambridge .

11

ELES P. and Kushinski K. et al. (1994) Synthesis of VHDL Concurrent Processes, in Proceedings of the Euro-Dac'94, Grenoble.

12

John L. Hennessy and David A. Patterson (1990) in Computer architecture, a quantitative approach, Morgan Kaufmann Publisher Inc.

13

Mekenkamp G. and Middelhoek P. F. A. et al. (1996) A Syntax based VHDL to CDFG Translation Model for High-Level Synthesis, in Proceedings of VHDL International Users Forum, VIUF Spring'96, 89-97, Santa Clara.

14

Mirkowski J. and Bilinski K. et al. (1996) Petri Net Modelling of VHDL Simulation Cycle for High Level Synthesis Purposes, in Proceedings of VHDL User Forum in Europe SIG-VHDL Spring'96 working conference, Dresden.

15

Murata. A. (1989) Petri Nets: Properties Analysis and Applications, in Proceedings IEEE, vol. 77 N$^{\circ}$ 4, 541-580, April 1989.

16

Bryant R. E. (1986) Graph Based Algorithms for Boolean Function Manipulation, in Proceedings of IEEE Transactions on Computers, Vol C-35, 677-691, 1986.

17

Hsieh Y-W. and Levitan S. P. (1997) Control/Data-Flow Analysis for VHDL Semantic Extraction, in Proceedings of 4th Asia-Pacific Conference on Hardware Description Language, 68-75, 1997.

 

 

About this document ...

Formal Analysis of Single WAIT VHDL processes
for Semantic Based Synthesis

 This document was generated using the LaTeX2HTML translator Version 99.1 release (March 30, 1999)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.