• 沒有找到結果。

On the verification of state-coding in STGs

N/A
N/A
Protected

Academic year: 2021

Share "On the verification of state-coding in STGs"

Copied!
5
0
0

加載中.... (立即查看全文)

全文

(1)

On the Verification

of

State-Coding in

STGs

Kuan-

J e n Lin and

Chen-Shang Lin

Department

of

Electrical Engineering

National Taiwan University

Abstract

One primary property for an Signal Transition Graph (STG) t o be synthesized in an asynchronous circuit is the realizable state coding

(RSC)

- more relaxed than USC. A procedure and its theoretical basis have been develope- d to verify t h e

RSC

property of a STG which contains multi-cycle signals and has a underlying free-choice Petri net. The procedure is carried out wholly on STG domain and is successful to verify the RSC of benchmarks[3].

1

Introduction

T h e synthesis of asynchronous circuits from specifications given in Signal Transition Graphs (STGs) has become an active research area[2, 4 , 5, 6, 71 since its first introduction by Chu[l]. One major factor of its popularity is the con- ciseness of the representation, the complexity of which is only linearly proportional to the number of signals involved in the specification.

The prevalent synthesis procedure from STG descrip- tions is comprised of (1) ensuring t h a t the STG is fea- sible for realization; (2) synthesizing hazard-free circuits. An S T G should possess some properties before the circuit can be realized. One primary requirement is t o ensure the corresponding state-diagram of STG to have a realiz- able state-coding. Usually the more restricted unique state coding property is sought. The verification and rectifica- tion for realizable state-coding are non-trivial tasks, since the size of state diagram is exponential with respect t o the signal number. Furthermore, the design optimizations are much intended t o be explored on higher level descrip- tion. Therefore, it is much desirable to suggest methods by which synthesis tools or designers can satisfy this require- ment directly on S T G domain rather t h a n state diagram. Previous works[4, 51 had presents techniques based on lock-relations among signals t o treat the state-coding prob- lem wholly on STG domain. However, their STG descrip- tions are restricted t o be marked graphs which exclude any conditional behaviors. Furthermore, the more constrained unique state-coding are considered i n their works, which might incur extra cost.

In this paper, new theoretical foundations and a new verification procedure based on transitive lock relation[5]

are developed to solve state-coding problem wholly on STG domain for S T G s containing multi-cycle signals and con-

ditional behaviors. The state coding problem considered here is the realizable state-coding which is a more relaxed requirement than the unique state coding. For STGs with multi-cycle signals, single-cycle transformation is proposed to transform the problem into ones with single-cycle signal- s. For STGs with conditional behaviors, two novel opera- tion, branch reversing and self-loop unfolding are proposed t o significantly simplify the verification process. T h e pro- posed algorithmic approaches have been shown successful on over thirty examples from academic and industry.

In next section, the state coding problem and relevant established results will be reviewed. Then the verification of state coding for STG with multi-cycle signals will be p- resented. In Section 4, two novel operations, branch reuers- ing and self-loop unfolding, will be introduced to facilitate the solving state-coding problem on STG with conditional behaviors. A procedure incorporating these operations will then be illustrated with an example. Finally, we will give our evaluation results on over thirty examples and then the conclusion.

2

STG

Synthesis and State-

Coding

An STG can be viewed as an interpreted Petri net. T h e STG under consideration has the underlying Petri net be- ing a free-choice net. In such STG, t h e places of single fanin and single fanout of the underlying net are removed and only two types of nodes are retained: the signal tran- sitions and the multiple fanin or multiple fanout places. The transitions of signal a denoted by a+ and a- repre- sent the rising and falling transitions respectively, and if i t has underline, it is an input transition. A transition of signal a , t,, can be either a+ or 4- and if t, = a+ then

t , = a - . A signal is single-cycle if it only contains two transitions, otherwise it is multi-cycle. In STG, if there is an arc from a transition tl to another transition 1 2 , we denote it by tr -+ t z

.

And tl =+ t z ...

+

t k , t r , t z , ... th are in a loop and these transitions occur in the order of their indexes.

A live and safe free-choice Petri-net can be covered by a set of live and safe MG-components and SM- components[l]. An Marked-Graph(MG) is a net in which each place has a t most one fanin and at most one fanout.

(2)

By duality, a n State-Machine(SM) is a net in which each transition has a t most one fanin and a t most one fanout. T h e M G can model concurrent behaviors and SM condi- tional behaviors.

For a given S T G t o be synthesized, it should possess certain properties as follows[l].

D e f i n i t i o n (Liveness) A S T G is live iff

(1) the underlying Petri net is live and safe,

( 2 ) every SM-component contains exactly one token,

(3) for each signal a , transitions t , and Definition:(Realizable State Coding(RSC))

A live S T G has RSC property iff any two states which enable different sets of non-input signal transitions have distinct state codes.

Note that t h e RSC is more relaxed than the USC (U-

nique State Coding) which requires all state codes to be distinct. To satisfy RSC property before circuit realiza- tion is a mandatory task. However, it is a non-trivial task, since t h e size of s t a t e diagram is exponential with respec- t t o the signal number. Here th e verification of RSC is to be approached on the S T G domain. T h e complexity of the problem depends on the underlying Petri net of the given STG. We denote an S T G by STG/MG if i t only con- tains exactly one marked graph and by S T G / F C if it has input free-choice behaviors (conditional behaviors). An STG/MG is a n STG/MG-S, if each signal is single-cycle. In an STG/MG-S, special relations between signals have been shown to have significant impact on the realizability. D e f i n i t i o n (Lock)

In an STG/MG, there is a lock relation between single- cycle signals a and b , denoted as a L b , iff

are ordered.

U +

=+

b+ =+ U - 3 b- V U +

+

b - 3 U -

+

b+ D e f i n i t i o n (Transitive Lock)

tween single-cycle signals a and b , denoted as a Lt b, iff In an STG/MG, there is a transitive lock relation be-

a L b V ( a L' c A c L' b ) , c is another signal in STG. Note that the lock relation is not defined for a multi-

cycle signal. T h e transitive lock relation is crucial not only for state-coding problem but also the synthesis of hazard- free implementations[8]. T h e following useful theorem is derived in [4, 51 as a sufficient condition to satisfy RSC.

Theorem 1: A live STG/MS-S has USC(Unique State

Coding) property if there is Lt relation between any two signals.

3

RSC

for

STG/MG

For a live STG/MG, our basic strategy is to transform or split each cycle of a multi-cycle signal into a distinct single- cycle signal and then t o apply the results for STG/MG-S t o solve t h e realizable state coding problem. T h e detail will be described in this section.

Let us firstly describe the more general strategy. Let z1+, z l - , 22+

,...,

zn+, zn- be all transitions of z

and with the relation: ZI+

+

21-

+

ZZ+

+

2 2 -

+

... z,+ j zn-. Since there are two ways t o

group adjacent transitions into a cycle, the corresponding two single-cycle transformations are as follows: ( 1 ) odd or- der: (zI+, .I-), ( z z + , Z Z - ) ,

...,

(zn+s zn-); ( 2 ) even order: ( Z I - , ZZ+), (ZZ-, z 3 + ) ,

...,

(z,--,z~+).

Based on the transformation strategy, the following the- orem allows us to verify RSC property for STG/MG with multi-cycle signals directly on S T G domain.

Theorem 2 : A live STG/MG has realizable state coding

if in each single-cycle transformation on all multi-cycle sig- nals, a L* b is true for each non-input signal a and any of it's enabling signal b .

Proof see [Ill.

The usefulness of the above results evidently depend- s on the number of multi-cycle signals in the STG, since it incurs

( z N )

possible transformation combinations for

N

multi-cycle signals. To reduce the complexity, we have ob- served that for a multi-cycle signal satisfying certain con- ditions, i t can be considered as a set ofindependent single- cycle signals when checking RSC property by Theorem 2.

In other words, only either odd- or even-order transforma- tion of the signal is sufficient to derive RSC. This desirable condition is described in the following.

V i r t u a l Single-Cycle Signal: A signal m with n cycle can be considered as a set of single-cycle signals from it's even(odd) order transformation if

V i , i = 0, 2 ,

...,

2 n - 2 ( i = 1, ..., 2 n - 1 ) , there are two real or virtual single-cycle signal transitions t and t.2 having

t,l = t.2 or 21

L'

2 2 relation, such that t k

+

t,l =+-

t?' =$

t2'

=+

t.2 3

t Z 3 ,

where t i = t i m o d

'".

The application and importance of this technique are shown by the following theorem.

Theorem 3: For a live STG/MG, after virtual single- cycle signal transformation, if i t satisfies the RSC condi- tion of Theorem 2, the original STG/MG also have RSC property.

Proof see [ I l l .

To illustrate the approach, we take the example shown in Fig. 1, where the /number is used to distinguish between multiple transitions of the same signal. In the beginning the signal c is found to be virtual single-cycle signals by

e . Then e , d , c l , and c2 are found to have Lt relation between each other. By their transitions, e+ and c - / 2 , b thereby can be regarded as two virtual single-cycle signals. Fig. l ( c ) shown the final lock-graph. The example is found to have RSC property but not USC.

With a preprocessed Relation-Table[lO], if all multi- cycle signals can be iteratively treated as virtual single- cycle signals, the complexity of verification will be O( N z x

M + M 2 x

N),

where

N

is the number of single-cycle signal- s and

M

of multi-cycle. Specifically, for one iteration, in which we try to transform all remaining multi-cycle signal- s using real or transformed virtual single-cycle signals, we need

( N 2 )

for the derivation of Lt relation and

( N

x M ) for

virtual single-cycle signal transformations. In worst case,

M iterations are required.

The virtual single-cycle concept has been found to be ex- tremely useful in practical cases. In our experiment, most of STG/MGs derived from Berkely[3] can be evaluated by

(3)

b+/l

a -(b+/l,b-/l)

( C )

(a)

Figure 1: (a) A n initial

STG

with t w o multi-cycle sig- nals and (b) it's lock g r a p h after c transformed t o vir- t u a l single-cycle signals a n d (c) it's lock g r a p h after c a n d

b

transformed to v i r t u a l single-cycle signals.

this technique only.

4

Branch Reversing and Self-

loop

Unfolding

Since a live S T G / F C can be covered by a set of live STG/MGs[l], it is possible t o verify the RSC of the S T G / F C from those of MG components and their com- binations. Although i t is not difficult t o verify whether these smaller covering S T G / M G components to have RSC based on the results in the previous section, it is not trivial to verify markings in different MG-components whether t o satisfy RSC requirement. To simplify the latter task, two operations, branch reversing and self-loop unfolding, will be introduced in this section. By appropriate usage of these two operations, the S T G / F C can be transformed in- to such a way t h a t the RSC is checked for each covering MG component and each pair.

Consider a free-choice Petri net with a given initial marking. Define a place with multiple fanouts as a f o r k

and a place with multiple fanins as a j o i n . A place can be both a f o r k and a j o i n . Between a f o r k and a set of concurrent j o i n s , the arcs and places which form a con- nected segment of a covering MG-component is a branch.

A branch is a self-loop if its two ends are the same place. A branch is said t o be reversed if the direction of all arcs connected t o transitions as well as the transition directions in the branch are reversed. In Fig. 2(b), when the branch e- --t B+ -+ c+ is reversed, the resultant net is shown in Fig. Z(c). And self-loop is said t o be unfolded if its common place is split into two places such that one con- sists only of the fanouts to the self-loop and the original fanins except those from the self-loop, and the other place consists of the remaining fanins and fanouts. The other structural relations are retained. In other words, the self-

loop is straightened as can be seen from Fig. 2(b) in which one self-loop in Fig. 2(a) is unfolded.

The application of these two operations on a live S T G will still retain the liveness property. From [9], when an live and safe net is entirely reversed, it will behave as backward firings as the original. Hence, it is still live and safe, and can generate equivalent markings(one-to-one correspond- ing) as the original. In our application, only some specific parts of net are reversed. Those parts, in essence, can be removed and the original net is still live and safe. Based on this fact, we can prove that the liveness and safeness of net, the liveness of STG are retained after an S T G / F C reversing an Branch[ll]. To unfold an self-loop, can be considered as to force the self-loop t o be chosen each time when the f o r k of self-loop is marked. In essence, they are legal firing sequences in original net. Therefore, liveness and safeness of net, the liveness of S T G are retained after one self-loop is unfolded[ll].

Given an initial marking, we are able t o traverse the STG from this given marking and identify all the feedback branches similar to identify all feedback loops from a se- quential circuit. Reversing all feedback branches except self-loops without the initial marking and unfolding those self-loops, the resultant net has the desirable property that all covering MG-components of the transformed net con- tain the given initial marking. In other words, the running MG contains all the tokens and thus determines the states.

As a result, t o verify the

RSC

property of the transformed net, we need only t o check the

RSC

of each MG-component and whether two markings of different MGs have the same state code. The key question is whether the transformed net has the equivalent RSC problem as the original one. The answer is affirmative as established in the following two theorems.

Theorem 4: For a live S T G / F C with initial marking mol

after one of it's branch is reversed, each marking in original STG has a corresponding marking in the transformed S T G and they have the same coding.

Proof see [Ill.

From the above theorem, it can be easily shown t h a t the USC is preserved after branch reversing. RSC can also be easily treated by observing that the predecessor and successor relation is reversed in the reversed branch.

Theorem 5 : For a live S T G / F C with initial marking mo,

after one of it's self-loop is unfolded, the S T G has equiva- lent BSC problem as the original.

Proof see [11].

5

An RSC Verification Proce-

dure for STG/FC

Based on the discussion in the last section, the principle of BSC property verification for an S T G / F C can be de- scribed.

From the previous section, given an initial marking of an STG/FC, we are able to transform the given net into a net without internal feedback branch so that each covering

(4)

d-

-

T

d- F d-

-

-G

a+

A

c- e+

I f

(0

Figure 2: (a) A n initial S T G / F C ; (b) T h e S T G / F C f r o m (a) unfolding one self-loop; (c) T h e S T G / F C f r o m (b) reversing one feedback branch; (d) (e) MG- components from (c); (f) Disjoint set of ( d ) and (e); (g) A n S T G / M G f r o m ( f ) reversing one branch.

MG-component contains the initial marking. Hence each running MG contains all the tokens and thus determines the states. As a result, t o verify the RSC property, we need only to check the RSC of each MG-component and whether two markings of different MGs have the same state code. The former can be solved by those described in Section 3, and the latter is simplified because all MG-components have one common marking. The disjoint set between any two MG-components then contains only pairs of conj7ic- t branches which are two b u n c h e s with the same foTk and join. Only these conflict pairs need to be checked for state code equivalence, and each pair of the conflic- t branches, by branch reserving and self-loop unfolding, can be transformed into MGs with equivalent state cod- ing problem. Since the conflict-branch pair has the same f o r k and j o i n , i f f ork and j o i n are distinct nodes, we can

reverse one branch of the pair such that the two connect- ed segments of MG-components are strongly connected t o become one live and safe MG. If f o T k and join are the same node, this means these two branches are actually t-

wo entire MG-components. One branch is then unfolded and linked t o the other to become one larger MG. Both two cases allow us apply the techniques for STG/MG to verify RSC.

Based on the above descriptions, a procedure to verify the RSC property of S T G / F C is given below.

Procedure: RSC Verification for STG/FC :

(Given a live STG/FC with an initial mdrking m 0 )

1. Unfold all Self-loops not marked an m 0 .

2. Reverse all Feedback-Branches.

3. Derive all transition relations.

4 .

Foreach MG-component, perform verification

5. Foreach pair of Conflict-Branch ( C B i , C B j )

Reverse or Unfold CBi

+

CB:.

perform verification for C B j

+

CB:.

}endforeach

Let us illustrate the Procedure by an example shown in Fig. 2(a). After the first two steps, the initial S T G / F C is transformed to the STG in Fig. 2(c). This transformed STG/FC has two MG-components, as shown in Fig. 2(d) and Fig. 2(e). Both these MG-components can be easily verified by techniques for STG/MG. There is one pair of

conflict branch in the transformed STG, as shown in Fig. 2(f). We can reverse one brunch to make them t o be an STG/MG shown in Fig. 2(g). Again, it is verified by the method for STG/MG. The complexity of this procedure mainly depends on the number of MG-components and pairs of conflict-branches.

6

Discussion and Conclusion

The proposed verification procedures in this paper have been successfully evaluated with the set of S T G bench- marks from Berkely[3]. Table 1 contains those STGs hav- ing multi-cycle signals or conditional behaviors. The sec- ond column shows the total number of signal transitions in STG. STG/MG and S T G / F C can be distinguished by the No. of MG-components(MG) since an STG/MG have only one MG-component. For an STG/FC, Pairs of Conflict- branches(CB) is the number of STG/MGs to be processed in step 4 of the RSC Procedure to verify markings in d- ifferent covering MGs. The N o . of MG-components plus Pairs of Conflict-branches are the total times required to employ techniques for STG/MG to verify RSC. In all ex- amples, the number is quite small and the number of tran- sitions in each such MG, in general, is much smaller than the number in whole STG/FC.

Another useful indicator of the complexity is the num- ber of Iterations of Virtual Single-Cycle Transforma- tion(VSC). It is the iterations needed to transform an

(5)

S T G / M G t o STG/MG-S with the virtual single-cycle sig- nal technique. Most examples can be completed in one

from Graphical Specifications,’’ Proceeding of the In- ternational Conference on Computer-Aided Design, p- iteration and the complexity of RSC verification for those p. 322-325, 1991.

S T G / M G is close t o

(N’),

where

N

is the number of sig- nals in t h a t STG. Furthermore, all cases except Lavagn0.g and pe-send-ifc.g, including all STG/MGs during the RSC verification of STG/FCs, can be verified with this tech- nique only. This demonstrates the effectiveness of virtual

single-cycle signal transformation.

In this paper, we have proposed a new verification pro- cedure and the theoretical foundations based on transi- tive lock relation t o solve state-coding problem wholly on S T G domain for STGs containing multi-cycle signals and conditional behaviors. Rather than approach directly on state-diagram, our procedure does not incur the exponen- tial complexity with respect to the signal numbers. The s- t a t e coding problem considered here is the realizable state- coding which is a more relaxed requirement than the u-

nique state coding. For STGs with multi-cycle signals, single-cycle transformation is proposed t o transform the problem into ones with single-cycle signals. T h e experi- mental results have shown the complexity for most cases is near t h a t for an STG/MG-S. For STGs with condition-

al behaviors, two novel operations, branch reversing and self-loop unfolding are proposed t o significantly simplify the verification process. After transformation with these two operations, this verification can be performed by the techniques for STG/MGs. The proposed algorithmic ap- proaches have been shown successful on over thirty exam- ples from academic and industry.

References

[l] T. A. Chu, “Synthesis of Self-Timed Control Circuit- s from Graphical Specifications”, P h D thesis, MIT, June, 1987.

[2] T. H.-Y. Meng, Robert W. Brodersen, David

G. Messerschimitt, ”Automatic Synthesis of Asyn- chronous Circuits from High-Level Specification,”

IEEE Trans. on CAD., pp. 1185-1205, No. 11, 1989. [3] L. Lavagno and Cho W. Moon, “Private Communica-

tion”.

[4] Peter Vanbekbergen, Francky Catthoor, Jef Van Meerbergen, Hugo DE Man, “Optimized Synthesis of

Asynchronous Control Circuits from Graph-theoretic Specifications,” Proceeding of the International Con- ference on Computer-Aided Design, pp. 1 8 4 1 8 7 , 1990.

[SI K. J. Lin and C. S. Lin, “Automatic Synthesis of Asynchronous Circuits,” Proceeding of 28th Design Automatic Conference, pp. 296-301, 1991.

[6] L. Lavagno,

K.

Keutzer, A. Sangiovanni Vincentel- li, “Algorithms for Synthesis of Hazard-free Asyn- chronous Circuits,” Proceeding of 28th Design Auto- matic Conference, pp. 302-308, 1991.

[7] Cho W. Moon, Paul R. Stephan and Robert K. Bray- ton, Tynthesis of Hazard-free Asynchronous Circuits

[8] K. J. Lin and C. S . Lin, “A Realization Algorithm of of Asynchronous Circuits from STG,” Proceeding of 1992 European Conference on Design Automation,

pp. 322-326.

[9] 3. L. Peterson, “Petri net theory and the modeling of system,” prentice Hall, 1981.

[lo] K . J. Lin, “Automatic Synthesis of Asynchronous Cir- cuits,’’ Ms. thesis, EE Department of National Taiwan University, 1990.

[I11 K . J. Lin and C. S. Lin, “The verification of State- Coding in STGs,” Technical report, EE Department of National Taiwan University, 1992.

T: No. of transitions.

MC: Maximal No. of Multi-Cycle signals in MGs. MG: No. of MG-component.

CB: Pairs of Conflict-Branches.

VSC: Iterations of Virtual Single-Cycle signals.

(a) Some STG/FCs are rewritten by merging apparent equiv-

(b) (c) The RSC verification for this STG/MG requires gen- alent structures in conflict-branches.

eral singlccycle transformation on some multi-cycle signals.

數據

Figure  1: (a) A n   initial  STG  with  t w o  multi-cycle  sig-  nals  and  (b)  it's  lock  g r a p h   after  c  transformed  t o  vir-  t u a l  single-cycle  signals a n d   (c) it's  lock  g r a p h   after  c  a n d   b  transformed  to  v i r t u
Table  1.  Experimental Results.

參考文獻

相關文件

In this paper, we propose a practical numerical method based on the LSM and the truncated SVD to reconstruct the support of the inhomogeneity in the acoustic equation with

In this paper, we have studied a neural network approach for solving general nonlinear convex programs with second-order cone constraints.. The proposed neural network is based on

In this paper, we build a new class of neural networks based on the smoothing method for NCP introduced by Haddou and Maheux [18] using some family F of smoothing functions.

In this paper, we have shown that how to construct complementarity functions for the circular cone complementarity problem, and have proposed four classes of merit func- tions for

The purpose of this talk is to analyze new hybrid proximal point algorithms and solve the constrained minimization problem involving a convex functional in a uni- formly convex

• Strange metal state are generic non-Fermi liquid properties in correlated electron systems near quantum phase transitions. • Kondo in competition with RVB spin-liquid provides

In addition to examining the influence that the teachings of Zen had on Shi Tao’s art and theoretical system, this paper proposes further studies on Shi Tao’s interpretation on

In this thesis, we have proposed a new and simple feedforward sampling time offset (STO) estimation scheme for an OFDM-based IEEE 802.11a WLAN that uses an interpolator to recover