Hierarchical gate-level verification of speed-independent circuits

Hie a chical Ga e-Le el Ve i ica ion o Speed-Independen Ci cui s o as O iol Roig, Jo di Co adella and En ic Pas o * Depa men o Compu e A chi ec u e Uni e si a Poli kcnica de Ca alunya G an Capi & s/n, Mbdul D6, 08071-Ba celona, Spain Abs ac This pape p esen s a me hod o he e i ica ion speed-independen ci cui s. The main con ibu ion he educ ion o he ci cui o a se : o complex ga es ha makes he e i ica ion ime complexi y de- pend only on he numbe o s a e signals (C elemen s, RS iip-jlops) o he ci cui . Despi e he educ ion o complex ga es, e ijica- ion is kep exac . The speci ica ion o he en i on- men only equi es o desc ibe he ansi ions o he inpu /ou pu signals o he ci cui and is allowed o ex- p ess choice and non-de e minism. Expe imen al e- sul s ob ained om ci cui s wi h mo e han 500 ga es show ha he compu a ional cos can be d as ically e- duced when using hie a chical e i ica ion. 1 In oduc ion Asynch onous ci cui s can be conside ed as a p ac- ical al e na i e o ace some o he c i ical p oblems ha appea when designing complex, low powe , high pe o mance digi al sys ems. The clock signal in synch onous ci cui s enables o in oduce a le el o abs ac ion in he ime domain and o e look mos empo al ela ions among he sig- nals o he ci cui . Only he concep o c i ical pa h is ele an o he pe o mance o he sys em bu no o i s unc ional co ec ness. Un o una ely o he designe , he absence o a clock in asynch onous ci - cui s makes hei design an e o -p one ask. Mos di icul ies come om he need o ensu e ha all sig- nals a e ee o undesi able ansi ions, haza ds, ha can p oduce ci cui mal unc ions. The addi ional complexi y in oduced by he anal- ysis o he empo al ela ions makes e i ica ion essen- ial o asynch onous ci cui s. Bu while only he ou - pu s o memo y elemen s, e.g. lip- lops, a e equi ed o ep esen he s a e o a synch onous ci cui , he ou - pu o all nodes (ga es and memo y elemen s) mus be p obed o de ine he s a e o an asynch onous ci cui . Gi en ha , in he wo s case, he size o he s a e space can be 0(2.), TI being he numbe o signals o de ine he s a e, his space can become ex emely la ge e en o mode a e size asynch onous ci cui s. Se e al au ho s ha e p oposed e i ica ion ech- niques o a oid he explici enume a ion o all he *Wo k suppo ed by ACID-WG (Esp i 7225), CYCIT TIC 94-0531-E and Depa men d’Ensenyaxnen de la Gene ali a de Ca alunya. s a es: un oldings [ll], pa ial o de s [14], symbolic model checking [4] and ace heo y [6] among o he s. This pape p esen s su icien condi ions o au- oma ically educe he complexi y o he ci cui o be e i ied o speed-independence. The p oposed me hod aims a he educ ion o he numbe o a i- ables equi ed o e i ica ion. I has been combined wi h symbolic model checking echniques o e icien ly ep esen he s a e space o he ci cui . 1.1 Con ibu ions The me hod p esen ed in his pape aims a he e i ica ion o ga e-le el speed-independen ci cui s. Bee el e al. [a] obse ed ha , i he e i ie we e old by some o acle ha he ci cui is haza d- ee, check- ing i s co ec ness agains i s speci ica ion coiild he educed, oughly speaking, o pe o m a e i ica ion B la synch onous wi h only he ou pu s o he memo y elemen s (e.g. C-elemen s o RS lip- lops) as s a e a iables. Based on his obse a ion, ou app oach e i ies co ec ness in wo s eps: (1) sa is iabili y o he speci ica ion assuming he absence o haza ds and (2) haza d de ec ion. The majo con ibu ions o his pape a e he ollowing: The ci cui , a la ne lis o ga es, is au oma ically educed o a se o complex ga es. The ime com- plexi y o e i ica ion is made dependen on he numbe o memo y elemen s a he han on he numbe o signals o he ci cui . E en wi h he educ ion o complex ga es, e i i- ca ion is kep exac , i.e. nei he alse posi i e no alse nega i e e i ica ion esul s a e possible. The en i onmen is desc ibed by a s a e g aph ha only needs o con ain he ansi ions o he inpu /ou pu signals o he ci cui . Choice and non-de e minism o he en i onmen a e allowed. The pape is o ganized as ollows. Sec ion 2 dis- cusses he basic ideas o hie a chical ga e-le el e i- ica ion by means o an example. Sec ion 3 p esen s some basic de ini ions used along he pape . Sec ion 4 analyzes he condi ions unde which exac hie a chical e i ica ion can be pe o med. Sec ion 5 discusses he mos signi ican implemen a ion issues o ou e i ie . Compa a i e esul s be ween la and hie a chical e - i ica ion a e p esen ed in Sec ion 6. Finally, Sec ion 7 concludes he pape . 0-8186-7098-3/95 $04.00 0 1995 IEEE 128 I I d+ cc (b) Figu e 1: (a) Ci cui wi h a haza d- ee beha io , (b) The same ci cui wi h a haza dous beha io , (c) Equi alen haza d- ee complex-ga e ci cui . 2 Hiew chical e i ica ion: o e iew This sec ion p esen s hie a chical e i ica ion by means o wo examples. In his sec ion, speed- independence will be conside ed equi alen o haza d- eeness unde he unbounded ga e delay model. Mo e p ecise de ini ions will be gi en in Sec ion 3. Speed-independence is no a p ope y o a ci cui by i sel bu o he beha io o a ci cui unde a ce ain en i onmen . In ou amewo k, he beha io o he en i onmen will be ep esen ed by a Signal T ansi ion G aph [5] in which he ou pu signals will be inpu s o he ci cui and ice e sa. Figu es l.(a) and l.(b) depic a ci cui exci ed by wo di e en en i onmen s. The ci cui is haza d- ee wi h en i onmen (a), bu haza dous wi h en i onmen (b). In he la e case, a s a ic haza d can be p oduced on signal d when, in he s a e (abcde) = (11110), he e en e-- a i es be o e e has swi ched o 1. Howe e , no e ha an equi alen complex-ga e implemen a ion o he same ci cui (Figu e l.(c)) can be haza d- ee. Figu e 2 shows he s a e g aph ob ained by a each- abili y analysis o he sys em in Figu e l.(a). In he wo s case, he numbe o s a es can be as la ,ge as 2” , n being he numbe o signals o he ci cui . Ve i i- ca ion h ough eachabili y analysis [4] would simply check ha each ansi ion p oduced a he ou pu s o he ci cui can be accep ed by he en i onmen , i.e. a ansi ion wi h he same label is enabled in he STG. 2.1 Func ional and beha io al co ec ness Two impo an concep s mus now be in oduced o se up he basis o e i ica ion: unc ional co ec ness and beha io al co ec ness. A ci cui is said o be unc ionally co ec i an ap- p op ia e combina ion o he delays o i s componen s can p oduce he beha io expec ed by he en i on-- men . A unc ionally co ec ci cui is said o be behaw io ally co ec i i p oduces he beha io expec ed by he en i on nen ega dless he delay assigned o each componen , p o ided ha he delays a e wi hin he ma gins assumed o he delay model and he echnol- ogy. Fo speed-independen ci cui s, delays a e in he ange (0, a). (abcde) 00000 1 1000 11001 11011 11111 Fk C+ , /01000~ 1 00010 I d- b- e- C- e- b- ~01010] I 00011 I 01110 01111 Figu e 2: S a e G aph o he ci cui in Figu e l.(a). We can say now ha he ci cui in Figu e l.(b) is unc ionally co ec , since by assigning he AND ga e a delay sho e han he delay be ween he ansi ions b+ --+ e-, he gene a ed beha io is he one expec ed by he en i onmen . Howe e , his ci cui is beha - io ally inco ec , since long delays on he AND ga e may p oduce a s a ic haza d on d. The ci cui in Fig- u e l.(c) is bo h unc ionally and beha io ally co ec ( he complex-ga e a chi ec u e basically assumes ze o delay o he AND ga e). 2.2 Ve i ica ion o unc ional co ec ness A speed-independen ci cui mus beha e co ec ly o any ini e delay o i s componen s. A pa icula case consis s in “mo ing” he delay o a ga e o i s an-ou ga es. Le us ake as example he ci cui in Figu e l.(b). We can mo e he delay o ga e e o i s an-ou ga e d, and we ob ain he complex ga e in Figu e l.(c). We e e o his kind o ga e clus e ing as collapsing. Since all he delays a e in he ange (0, a), he sum o he delays o d and e is s ill in he same ange. The beha io o he ou pu o a complex ga e is included in he beha io o he o iginal ci cui (p io o collapsing). In ou amewo k, unc ional co ec ness is e i ied 129 (abed) “haza d” (b) Figu e 3: (a) S a e g aph a e e i ica ion o unc- ional co ec ness. (b) S a e g aph a e e i ica ion o beha io al co ec ness. by collapsing some o he ga es o he ci cui . In his way, mul iple ga es can be collapsed in o one complex ga e and, hus, in e nal signals elimina ed o he e i- ica ion. Only o memo y elemen s (e.g. C elemen s) o ou pu s o complex ga es, he signals canno be elimina ed. Ve i ica ion o unc ional co ec ness becomes sim- ple and as e because o he elimina ion o in e nal signals. Mo eo e , design e o s ha do no depend on he delays o he ga es can be de ec ed soon, wi hou equi ing an exhaus i e e i ica ion o he empo al ela ions among all signals. In he example o Figu e l.(b), unc ional co ec - ness is e i ied by i s collapsing he AND and OR ga es in o one complex ga e and elimina ing signal e. Nex , he s a e g aph o he ci cui /en i onmen is buil and e i ied o co ec ness (Figu e 3.(a)). 2.3 Ve i ica ion o beha io al co ec ness In gene al, la ge ci cui s will be collapsed in o se - e al complex ga es. As illus a ed in Figu e 4, his can be done hie a chically acco ding o e iciency c i e ia o e i ica ion. Figu e 4: (a) Fla ci cui (8 ga es). (b) Hie a chical complex-ga e o ganiza ion (3 complex ga es). The second s ep o e i ica ion is de o ed o de- ec haza ds inside he complex ga es. In ui i ely, his is pe o med as ollows. Gi en a complex ga e, he s a e g aph o he collapsed ci cui is p ojec ed on o he inpu /ou pu signals o he complex ga e. This p ojec ion maps all s a es wi h he same alues o he inpu /ou pu signals o he complex ga e (e en i hey a e seman ically di e en ) on o he same s a e. We will show ha his appa en loss o en i onmen- al in o ma ion is no ele an o he e i ica ion o haza d- eeness. Finally, he complex ga e is e i ied o be haza d- ee unde he p ojec ed g aph as en i- onmen . Isomo phic g oups o ga es can be mapped on o he same complex ga e. In he example in Figu e 4 he e is a pa e n epea ed wice: an OR ga e which inpu s a e an AND ga e and a p ima y inpu . We will show in Sec ion 4 ha we can p ojec he en i onmen o se e al complex ga es on o one single s a e g aph and e i y hey haza d- eeness a a ime. This hie a chy allows us o e i y isomo phic subci cui s oge he . I is impo an o no ice ha he en i onmen o each complex ga e is calcula ed as i i we e haza d- ee. In Sec ion 4 we will show ha , e en wi h his es ic ed en i onmen , haza d- eeness can be exaclly e i ied. Figu e 3.(a) shows he s a e g aph o he collapsed ci cui . By chance, his g aph coincides wi h i s p o- jec ion on o he signals {a, b,c,d} as he whole ci - cui has been collapsed in o one complex ga e. When gene a ing he s a e g aph o he complex ga e (Fig- u e 3.(b)), an unexpec ed ansi ion (d-) is de ec ed in s a e ii010, since he co esponding s a e o he en i onmen (1101) can only accep ansi ion a-. In case he complex ga e we e e i ied o be haza d- ee, i s co esponding s a e g aph would be p ojec ed on o he inpu /ou pu signals o i s componen s and he same ope a ion would be pe o med a he nex le el o he hie a chy. This is illus a ed in Figu e 5 ha depic s he en i onmen o he AND ga e a e p ojec ing he g aph o Figu e 3.(b) on o he signals (%b, ell. ‘This en i onmen is only depic ed as an example, since he e is no need o de i e i o simple ga es o o ga es con- ained in haza dous complex ga es. 130 Figu e 5: En i onmen o he AND ga e a e he p o- jec ion o he s a e g aph on o he signals a, b and e. Only one ques ion emains o be answe ed: why is hie a chical e i ica ion exac ? In ou amewo k, he absence o haza ds is p o ed by e i ying ha he ci cui is semz-modula , i.e. no ga e can be disabled by changing he alue o i s inpu s. Le us assume ha C is a ci cui amd 6 is an equi alen ci cui in which some ga es ha e lbeen collapsed in o complex ga es and he co esponding in e nal signals elimina ed. In Sec ion 4 we will p o e ha : a) i 6 is no semi-modula , hen C is no semi- b) i C is semi-modula bu C is no semi-modula , he e is a complex ga e o e o which he beha - io o he co esponding decomposed ga e, unde he p c)jec ion o he s a e g aph o 6 on o he inpu /ou pu s o he ga e, is no semi-modula . Conjec u e a) gua an ees no alse nega z es, Why is hie a chical e i ica ion mo e e icien ? A c i ical ac o ha de e mines he complexi y o e i ica ion is he numbe o signals o he ci cui . Wi h hie a chical e i ica ion he numbe o signals ele an a each s ep o he e i ica ion is d as ically educed: du ing e i ica ion o unc ional co ec ness only he inpu /ou pu signals o he complex ga es a e equi ed; du ing e i ica ion o beha io al co ec ness o a complex ga e only he in e ace and in e nal sig- nals o he ga e a e equi ed. The e is only one limi o he minimum numbe o a iables equi ed o unc ional e i ica ion: he num- be o ou pu signals o he memo y elemen s, such as C-elemen s o RS lip- lops. modula ei he . h whe eas conjec u e b) gua an ees no alse posz z es. 2.4 app oach imp ac ical when a la ne lis o ga es, wi h no explici hie a chical o ganiza ion, mus be e i ied. Following Dill’s app oach, a subse o ga es o he la ci cui (po en ially subs i u able by a complex ga e) should be subs i u ed by an equi alen ace s uc u e. No knowing how he en i onmen o he complex ga e will be inside he ci cui , he ace s uc- u e should conside all possible inpu /ou pu ansi- ions and, he e o e, include he s a e o all in e nal signals, which would p eclude he subse o ga es o be handled as a complex ga e. Conse a i e e i ica ion Bee el e al. [2] also p opose a wo-s ep app oach. A - e e i ying he ci cui is complex-ga e equi alen o i s speci ica ion, haza d- eeness is e i ied by subse- quen ly checking he mono onici y and acknowledg- men o all signal ansi ions. A cube app oxima ion ha o e es ima es he se o s a es o he ci cui is p oposed o conse a i ely p o e he absence o haz- a ds. Al hough ne e ound in he examples p esen ed by he au ho s, alse nega i es a e heo e ically possi- ble. O he limi a ions o his app oach a e ha i is limi ed o ex e nally-cu ci cui s (all memo y elemen s mus appea in he speci ica ion) and ha he speci- ica ion o he ci cui is no allowed o exp ess ou pu choice (a bi a ion). Polynomial me hods o signal g aphs Kishine sky e al. [7] p esen ed a polynomial algo- i hm o e i y dis ibu i i y (a subclass o speed- independence) om ci cui beha io s desc ibed by sig- nal g aphs. The main limi a ion o hei app oach is ha he signal g aph mus speci y he ansi ions o all signals o he ci cui and ha nei he choice no non-de e minism a e allowed in he signal g aphs. 3 De ini ions We will conside a ci cui o be a se o ga es con- nec ed o an en i onmen . The beha io o he en i- onmen will be modeled by means o a s a e g aph. In ou e i ie , he s a e g aph is de i ed om a Sig- nal T ansi ion G aph ha desc ibes he in e ac ion o he en i onmen wi h he inpu /ou pu signals o he ci cui . Thus. en i onmen s wi h choice and non- 2.5 Rela ed wo k de e minism a e allowed. In his sec ion, some o he mos ele an e o s e- la ed wi h 8he e i ica ion o speed-independence and closes o he app oach desc ibed in his pape a e p esen ed. Hie a chical e i ica ion De ini ion 3.1 (Ci cui ) A ci cui is a pai C = (A, “1, whe e A = {al, ..., a,} is a se o signals (. = AI) and F maps each signal a; E A o a boolean unc ion ; o a i y n, ha ep esen s he unc ion compuied by he ga e ha d i es a;. In his hesis [B], Dill al eady p oposed hie a c!hical e - i ica ion o speed-independence: i a componen con- o ms o a ace s uc u e, he beha io o ha compo- nen can be sa ely subs i u ed by he ace s uc u e. Howe e , his app oach equi es he designe o iden i y he basic componen s o he ci cui and know hei expec ed beha io in ad ance. This makes he De ini ion 3.2 (Fan-in and an-ou o a signal) The an-in o signal a; E A, anin(a;) C A, is ihe se o signals ha i depends on. Fo ga es ha hold s a e, a; E anin(a;). The an-ou o signal a; E A, anou (a;) C_ A, is he se o signals ha depend on ai, i.e. anou (a;) = {ak E Ala; E anin(ak)}. 131 De ini ion 3.3 (S a e g aph) A s a e g aph (SG) is a 4- uple, (A,S, E,X), whe e A = {a1 ,..., a,} is he se o signals, S is he se o s a es, E C S x S is he se o ansi ions and X is he labeling unc ion o s a es ha maps each s a e wi h a bi - ec o o e A. The ac ha (s, s’) E E will be also deno ed by SES’. E* deno es he ansi i e closu e o E, and sE*s‘ de- no es ha he e is a pa h om s a e s o s a e s’ in he s a e g aph. In hose cases jn which he labeling unc ion is he iden i y, he s a e g aph will be deno ed simply as (A, S, E). De ini ion 3.4 S a e g aph o a ci cui The s a e g aph o a ci cui C = (A, F) wi h ini ial s a e so is a s a e g aph, SG(C, so) = (A, S, E), such ha S and E a e s ic ly de ined by he ollowing ecu sion: 1. so E s . 2. [(S E S)A(Vi#kSi = Si)A(SL # Sk)A(SL = k(s))] ==+ [(s’ E S) A (s, s‘) E E] . Rela ion E can be pa i ioned in o n subse s as ol- lows: Ei = {(s,s’) E Elsi =Si} , E = UEi. a,EA No e ha he labeling unc ion X is he iden i y. This means ha each s a e s E S is a bi - ec o o e A such ha he i h elemen o s, deno ed by si, speci ies he alue o signal ai in s a e s. Gi en a s a e s E S, i he e exis s s’ E S such ha sEis‘ we will say ha signal ai is exci ed in s a e s. O he wise we will say ha ai is s able in s. De ini ion 3.5 (P ojec ion o he s a e g aph o a ci cui ) Gi en he s a e g aph o a ci cui , SG(C, so) = (A, S, E), and a subse o signals X C A, he p ojec ion o SG(C,so) on o X is a s a e g aph, Vs = (SI ,... , Sn) E s, p ojx(s),= (SI,..., Sk), i.e. he sub- ec o o s con aining only he signals in X (we assume 1x1 = k and X o be he i s IC elemen s o A), p ojx(S) = (~’13s E S : p ojx(s) = s’} , P..& (E) { (P o& (s) 9 P o& ( 4) I SE’ s’ and only one signal in X ansi ions om s o s’} . = No e ha he de ini ion o a s a e as a bi - ec o implies ha seman ically di e en s a es can be p ojec ed on o he same s a e (i.e. p ojx(s) = p ojx (s’) = i’ and s # s’). The ollowing p oposi ion is a esul o he p e ious de ini ion. P oposi ion 3.1 Le C = (A, F) be a ci cui , SG(C, so) = (A, S, E) i s s a e g aph, and anin(ai) U {ai} & X E, A. Le p ojx(SG(C,so)) = (X,s^,@ be he p ojec ion o SG(C,so) on o X. Le s,s’ E S and SE S such ha p ojx(s) = p ojx(s’) = 2. Then ai exci ed in s e ai exci ed in s’ e ai exci ed in i? . P oposi ion 3.1 is c ucial o ou me hod, since i s a es ha he exci a ion/s abili y o a complex ga e (and subsequen ly semi-modula i y) can be lo- cally checked by only knowing he alues o he in- pu /ou pu signals o he ga e and ega dless he s a e o he es o he ci cui . Wi hou loss o gene ali y and o he sake o sim- plici y, we will conside au onomous ci cui s, i.e. wi h no in e ace, o e i ica ion. The ob ained esul s can be na u ally ex ended o ci cui s wi h in e ace. Nex , obse a ional equi alence [12] is de ined. This is a concep ha es ablishes an equi alence among hose ci cui s ha p oduce he same e en s on a gi en se o signals. Fo simplici y, we will use a es ic ed de ini ion, since we a e only in e es ed in ci cui s in which he signals o one o hem is a subse o he signals o he o he . De ini ion 3.6 (Obse a ional equi alence be- ween wo ci cui s) Le C = (A, F) and 6 = (X, @) be wo ci cui s wi h X C A, and le SG(C,so) = (A,S,E) and SG(G,?’) = (X,,!?,, ?) be hei s a e g aphs. C and C a e obse a ionally equi alen om so and ?’ espec i ely i : h h I. i ’ = p ojx(so) . 2. Vs E S,? E s^ such ha 2 = p ojx(s) and Vai E a) i sEis’ hen 31 E s^ such ha Z&? and b) i ?,!$? hen 3s‘ E S such ha sE>EjE>s‘ whe e E: deno es any sequence o non-obse able ansi ions. X: 9- s - p.ojx(s’) . and Z’ = p ojx(s‘) . In his pape we p opose o e i y semi-modula i y a he han speed-independence. Semi-modula i y is mo e obus han speed-independence and bo h con- cep s a e igh ly ela ed o mos p ac ical cases, as subsequen ly explained (see [17] o u he de ails). De ini ion 3.7 (Semi-modula i y) A signal ai is semi-modula wi h espec o signal ab E anin(ai) (ai # ak) i he ga e ha d i es ai, ha ing been exci ed, canno become s able by changing he alue o ak. In e ms o he SG o he ci cui , a signal ai is semi- modula wi h espec o ab in SG(C, so) = (A, s, E) i sE~s’ * [si # i(s) ==+ # i(~’)] . 132 4 = a3 . a5 + a4 . (a3 + as) 4 := a3 . (a1 + a2) + a4 . (a1 + a2 + u3) Figu e 6: O:R and C ga es collapsed in o a complex ga e. A signal ai is semi-modula i i is semi-modula wi h espec o a ‘l i s an-in signals. A ci cui is semi- modula i ail i s signals a e semi-modula . De ini ion i3.8 (S ongly-li e ci cui [17]) A ci - cui is s ongly li e z i s s a e g aph is s ongly con- nec ed and o each signal ai he e exis s a s a e s E S in which ai is exci ed. Theo em 3.1 ([17]) I a ci cui is s ongly li e, hen he ci cui is speed-independen i i is semi-modula . 4 Reduc ion o complex ga es This sec ion p o ides he means ha enable o elim-. ina e some signals o a ci cui o simpli y i s e i ica- ion. We p opose o collapse se e al ga es in o one complex ga e wi h he same unc ional beha io and elimina e he in e nal signals. Le us assume we ha e a ci cui C = (A,F) wi h signal a, being d i en by a combina ional ga e, Le. a, @ anin(a,). Le us build a new ci cui e = (X, F), wi h X = A-{a,}. Le 2= p ojx(s) and he boolean exp essions o he ga es o e de ined as ollo s: h i a, 4 anin(ai) , i a, E anin(ai) . No e ha he abo e exp ession subs i u es s, by ,(s) and, he e o e, i(2) does no depend on s,, as a, anin(a,). Figu e 6 shows how he boolean exp ession o a complex ga e is de i ed om he exp essions o he simple ga es. In case ] anou (a,)l > 1, mul iple com- plex ga es will be c ea ed, as illus a ed in Figu e 7. h Theo em 4.1 Gi en wo ci cui s C = (A, F) and e = (X,P), wi h X = A - {a,} and dejined as abo e, and hei s a e g aphs, SG(C, so) =AA, SI E) and SG(e, p ojx(so)) = (X, 2, g). C and C a e ob- se a ionally equi alen om so and p oj, (so) espec- i ely i all signals in anou (a,) a e semi,-modula wi h espec o a, in SG(C,sn). P oo Condi ion 1 o de ini ion 3.6 holds by cons uc ion. Le s E S, 2 E S, g = p ojx(s) and ai E X. In hose cases whe e we p o e ha a(s) = ;(Z), i imme- dia ely ollows ha obsez a ional equi alence holds. Mo e p ecisely, i(s) = i(g) = si implies ha ai is s able in bo h s and S and, he e o e, condi ions 2.a and 2.b hold. I i(s) = i(2) = Si he e exis s’ and s such ha sEis’ and SEi? and ? = p ojx(s’), since he same signal ansi ions om s and 2. The e o e, condi ions 2.a and 2.b also hold. I a, @ anin(ai) hen s(2) = i(s) and, he e o e, obse a ional equi alence holds. I a, E anin(ai) hen h h h h /y h i (2) = i(S1,. . . , Sn- l,O).K(.)+ i (s1 ,. . . , S,-l,l). n (s). 1 semi-modula i y obse a ional equi alence I ~ ~~~ Since ai is semi-modula wi h espec o a,, a change on signal a, canno disable ai. Hence, i(s) does no depend on s, when signals ai and a, a e simul aneously exci ed, i.e. I only emains he case which desc ibes he si ua ion in which ai is s able, a, is exci ed, and i(s) depends on he alue o signal a,. Hence, h i(2) = K(s1,. .., Sn-l,l).S,+ i(S1,...,S,-l,l).~n - - - ;(s) = si . Clea ly, condi ion 2.a holds o s a e s, since ai is no exci ed in s. To p o e 2.b, le us ake ? such ha 133 Figu e 7: (a) Ga e wi h mul iple- an-ou . (b) Complex ga e conside ed o unc ional co ec ness (c) and o beha io al co ec ness. h 2EiS’. We will p o e ha he e exis s’, s” E S such ha sE,s“Eis‘ and S’ = p ojx(s’). Since a, is exci ed in s hen we ha e s“ E S such ha sE,s”. Bu now, ai is also exci ed in s” as - i(S1,...,sn-1,0) = - ’i(~~,...,sn-~, 1) , and hus he e exis s s’ E S such ha d’Eis’. Finally, s and s’ only di e in he i h and n h elemen s and he e o e 2 = p ojx(s’). 17 semi-modula i y -3 7 obse a ional equi alence I I ai is no semi-modula wi h espec o a,, hen 3s,s‘,s// E S such ha sEis’, sE,s” and ai is no exci ed in s”. Since only a, changes be ween s and s“, we ha e ha s = p ojx(s) = p ojx(s/’). Thus, h Since ai is exci ed in s and s able in s” (a e a an- si ion o a,) hen i(s1,..., sn-l,~) = i(sl,..., sn-1,1) . Mo eo e , n(s) = S, and i(s) = Si, as a, and ai a e exci ed in s. The e o e, h i(2) = ;(sl ,..., sn-1,1) ‘sn + i(sl,..., sn-1,1) ‘5, - = i(S) = si , which means ha ai is no exci ed in 2 and, he e o e, condi ion 2.a does no hold. 0 Theo em 4.1 is he basis o p o e ha hie a chical e i ica ion is exac . This is he pu pose o he nex co olla ies. Co olla y 4.1 C no semi-modula om 9 ==+ C no semi-modula om so. h P oo This immedia ely ollows om he ac ha he s a e g aph o e is he p ojec ion o he s a e g aph o c. 0 Co olla y 4.1 gua an ees ha hie a chical e i ica- ion will no gi e alse nega i es. Co olla y 4.2 I 2 is semi-modula om and C is no semi-modula om so, hen ei he a, o some signal ai E anou (a,) a e no semi-modula in C. P oo (by con adic ion) Assume ha a, and all i s anou signals a e semi-modula . Then, by heo- em 4.1, C and e should be obse a ionally equi alen . Since C is semi-modula and C is no semi-modula , hen a, ( he only non-obse able signal) should be non-semi-m-odula , which con adic s he ini ial as- sump ion. 0 Co olla y 4.2 shows ha hie a chical e i ica ion does no p oduce alse posi i es. Conside a complex ga e ha d i es ai E anou (a,), and ha Xi is he se o inpu /ou pu signals o he ga e, i.e. h x, = (ai} U ( unqai) - {a,}) U unin(a,) . I can be de i ed ha , by aking p ojx,(SG(e,2’)) as he en i onmen o he complex ga e, and SE as he ini- ial alue o signal a,, non-semi-modula i y o ai and a, in SG(C, so) is also de ec ed in p ojx, (SG(e, 2’)) (by p oposi ion 3.1). In ui i ely i can be p o ed by showing he e is al- ways one s a e s o C in which non-semi-modula i y is mani es ed o he i s ime om so. Because o he obse a ional equi alence while semi-modula i y holds om so, he p ojec ion o s on oAXi will also belong o he se o s a es o p ojx,(SG(C,?’)). 4.1 En i onmen o a complex ga e and ci cui s wi h en i onmen Complex ga es ob ained om collapsing can be seen as ex e nally-cu ci cui s [l]. An impo an p ope y o ex e nally-cu ci cui s is ha hey ha e no hidden s a e. The s a e o such ci cui s is comple ely cap u ed by he alues o he in e ace signals, i.e. he alues o he in e ace signals uniquely de ine he alue o which all in e nal signals would e en ually se le i he in e ace we e held ixed [l]. This ollows om he ac ha memo y elemen s in ex e nally-cu ci cui s can be ega ded as combina ional ga es when gi en an in e ace s a e. Fo example, a C-elemen will ope a e as an AND ga e in hose s a es in which he ou pu is ze o, bu as an OR ga e i he ou pu is one. The p ojec ion o he s a e g aph on o he in e - ace signals will keep he edges in ol ing in e ace signal swi ches (see p oposi ion 3.1). This p ojec- ion, howe e , may old seman ically di e en s a es on o he same s a e, hus in oducing addi ional non- de e minism (choice). Ne e heless, inpu choice is 134 no a p oblem because in he second e i ica ion s ep we a e dealing wi h ex e nally-cu ci cui s. Since he e a e no hidden a iables, he ci cui eac ion will de- pend only on he s a e and on he signal ha has swi ched. The e o e, he beha io o an ex e nally-cu ci cui in such cases will be he same independen ly o whe he hei e is a s a e wi h nonde e minis ic choice o wo di e en s a es (wi h de e minis ic choice). Le us assume ha a ci cui has se e al iins ances o he same l(comp1ex) ga e. Figu e 8 shows wo AND ga es o he same ci cui wi h a di e en en i onmen o each. As p e iously men ioned, he en i onmen o a complex ga e is calcula ed as he p ojec ion o he s a e g a ph on o X,. In his is example he s a es labeled wi h 010 o he en i onmen o G2 esul om he p ojec ion o wo di e en s a es2. To e i y he semi-modula i y o each AND ga e, we calcula e he union o he en i onmen s o all AND ga es o he ci cui (en i onmen o he gene ic ga e G in Figu e 13). This many- o-one mapping may in o- duce choice and/o non-de e minism no mani es ed in he ini ial s a e g aph. In ac , he se o sequences o ansi ions accep ed by he union o p ojec ed s a e g aphs can be la ge han he union o he se s o sequences gene a ed by each indi idual ga e. How- e e , semi-modula i y is a local p ope y o a ga e ha needs o be checked only be ween adjacen s a es o i s en i onmen . Since any ansi ion o he p ojec ed s a e g aph esul s om a leas one p ojec ion o he o iginal s a e g aph, e i ica ion is no pessimis ic bu exac . In e es ingly, i he union o he p ojec ed s a e g aphs p oduces a semi-modula beha io o G ( he gene ic ga e), i also desc ibes a se o sequences o e en s ha , i applied o each ga e indi idually, would p oduce a semi-modula beha io . Needless o say ha , wi h he p e ious conside a- ions, he p esen ed app oach allows o e i y ci cui s agains an en i onmen desc ibed by a s a e g aph, possibly con aining choice, non-de e minism and/o s a e a iables ha do no co espond o alues o in- pu /ou pu signals. 5 Impleimen a ion issues A e i ie based on symbolic model checking has been implemen ed. I s inpu s a e a Signal T ansi ion G aph, desc ibing he beha io o he en i onmen , and a ne lis o ga es. The en i onmen only needs o speci y ansi ions o he in e ace signals o he ci cui . Inpu /ou pu choice and non-de e minism a e allowed. The ma kings (s a es) o he Signal T ansi ion G aph a e symbolically ep esen ed by using encoding echniques such as he ones p esen ed in [8]. Disjunc- i ely pa i ioned ansi ion ela ions and b ead h i s sea ch algo i hms o symbolic a e sal [4] h we been used o calcula e he se o eachable s a es. Nex , some implemen a ion issues a e discussed. 'Fo he sake o clea ness, hey a e depic ed as di e en s a es in he iigu e 5.1 Reduc ion o complex ga es The algo i hm cu en ly implemen ed is e y sim- ple. Each combina ional ga e is collapsed wi h i s an- ou ga es. Only when he ou pu o a combina ional ga e is one o i s inpu s ( eedback loop), he educ ion is no possible. A he end o he educ ion s ep, only one signal o each memo y elemen and combina ional loop is kep . These signals a e he ones used o unc ional e i ica ion. 5.2 Ou pu choice Ci cui s wi h ou pu choice (a bi a ion) can also be e i ied wi h ou me hod. The non-semi- modula i y o a bi a ion signals (e.g. ou pu s o a mu ex) is conside ed hidden inside he ga e and no mani es ed ex e nally. This equi es a special ad-hoc desc ip ion o a bi a ion elemen s in he lib a y o ga es. Fo example, a mu ex elemen wi h wo inpu s (RI,R2) and wo ou pu s (Al,A2) can be modeled by wo boolean equa ions: AI = RI A E; A2 = R2 A In his case, non-semi-modula i y is allowed o A1 and A2 wi h espec o A2 and A1 espec i ely. 5.3 Isoch onic o ks Ve i ica ion o speed-independence assumes ha wi e delays a e negligible wi h ega d o ga e delays. As shown in Figu e 7, ga es wi h mul iple an-ou a e spli in o se e al ins ances, each one collapsed wi h one o he an-ou ga es. Howe e , o ks mus be con- side ed isoch onic du ing he de ec ion o haza ds on he in e nal signals. The e o e, ga es ha sha e some inpu signals mus be simul aneously e i ied o be- ha io al co ec ness, wi h only one common ins ance o he mul iple- an-ou in e nal ga es. As i is shown in Figu e 7.(c), signals a5 and a6 mus be simul a- neously e i ied wi h only one ins ance o he ga e ha d i es a7. This would no be necessa y i delay- insensi i eness we e e i ied, since o ks a e no as- sumed o be isoch onic. 6 Expe imen al esul s Table 1 epo s he esul s ob ained om unning se e al expe imen s on ou e i ie . All he examples a e scalable, i.e. hey can be enla ged by simply in- c easing he numbe o ins ances o he basic cells. Howe e , hei in insic egula i y has no been ex- ploi ed o e i y he ci cui . The examples used a e he ollowing: mas e - ead (ob ained om au oma ic syn hesis ools), a Dis- ibu ed Mu ual Exclusion (DME) ci cui [9, 61, a ee a bi e [lS], an asynch onous FIFO [IO], a egis e ile [I31 and a demul iplexe [3]. Resul s on la (no educ ion o complex ga es) and hie a chical e i ica ion a e shown3. The numbe o signals o hie a chical e i ica ion co esponds o he 3F~ he DME, esul s a e compa able o hose p esen ed in [4] when mul iple ini ial s a es a e used. He e, we only p esen esul s ob ained wi h one ini ial s a e ( o a oid aking ad an age o he egula i y o he ci cui ) 135 cl- 000 - 010 al++ bl- 100 011 bl+i al- 110d 111 Cl+ 01 0 001 Figu e 8: Union o en i onmen s o di e en ins ances o he same ga e. numbe o s a es signals o he ci cui , since all com- bina ional ga es a e elimina ed. All he ci cui s a e domina ed by memo y elemen s. The one wi h mos combina ional ga es is he DME (hal o he signals). The FIFO is a peculia case, as all he signals a e ou pu s o memo y elemen s and, he e o e, no di e ence exis s be ween la and hie - a chical e i ica ion. The epo ed BDD sizes a e he la ges ones encoun e ed du ing he a e sal o he ci cui . The CPU ime o hie a chical e i ica ion is mos ly domina ed by he i s s ep ( unc ional e i ica- ion). The numbe o s a es o hie a chical e i ica ion is he one ob ained du ing unc ional e i ica ion. The size o he BDDs, o en c ucial o a oid unning ou o space, is educed by he ac ha many a iables a e elimina ed when educing o complex ga es. The signi ican imp o emen s in CPU ime a e basically due o wo ac o s: 1) he educ ion o he size o he BDDs and 2) he educ ion o he logic dep h o he ci cui , which di ec ly in luences on he numbe o i e a ions equi ed o each a ixed poin du ing he a e sal. The p esen ed esul s con i m ha hie a chical e - i ica ion makes ime complexi y depend on he numbe o s a e signals o he ci cui , a he han he numbe o ga es. We belie e ha e en be e esul s can be ob ained o ci cui s gene a ed by au oma ic syn hesis echniques, in which he a io o combina ional ga es may be highe . Howe e , a his momen he e a e no examples la ge enough o be conside ed c i ical o e i ica ion ( he la ges ones can be e i ied in oughly a dozen o seconds). As ools o syn hesis and com- posi ion o ci cui s become ma u e, he complexi y o he ci cui s will inc ease signi ican ly. 7 Conclusions The complexi y o o mal e i ica ion o asyn- ch onous ci cui s undamen ally depends on he size o he ci cui , i.e. he numbe o ga es. Reducing he size o a ci cui by collapsing ga es in o complex ga es only allows a pa ial e i ica ion in which a alse pos- i i e migh be gi en as esul . In his pape , su icien condi ions o hie a chically e i ying speed-independence ha e been p esen ed. I has been shown ha an exac e i ica ion can s ill be done i he ci cui is educed o complex ga es and he en i onmen o each complex ga e is calcula ed du ing he e i ica ion o unc ional co ec ness. Ci cui s a e allowed o be e i ied agains an en i onmen ha may speci y inpu /ou pu choice and non-de e minism. A e i ie based on symbolic model checking has been implemen ed and se e al expe imen s wi h la ge ci cui s epo ed. I has been shown ha , by educing he numbe o ele an a iables du ing e i ica ion, bo h he size o he BDDs and he compu a ional cos d as ically d op. As u u e wo k, echniques o egula i y ex ac ion will be explo ed [15]. They should allow o u he e- duce he compu a ional cos o hose ci cui s in which combina ional ga es domina e o e memo y elemen s. Acknowledgmen s We would like o hank Lucian0 La agno, Alex Yako le , Michael Kishine sky and Alex Kond a ye o nume ous insigh ul discussions on imp o ing he cla i y and p esen a ion o his wo k. Re e ences [I] P. A. Bee el. CAD Tools o he Syn hesis, Ve i ica ion, and Tes abili y o Robus Asynch onous Ci cui s. PhD hesis, S an o d Uni ., Aug. 1994. [a] P.A. Bee el, J. R. Bu ch, andT. H.-Y. Meng. Su icien condi ions o co ec ga e-le el speed-independen ci - cui s. In P oc. In . Symp. on Ad anced Resea ch in Asynch onous Ci cui s and Sys ., pages 33-43. IEEE Compu e Socie y P ess, No . 1994. 131 P. A. Bee el and T. H.-Y. Meng. Semi-modula i y and es abili y o speed-independen ci cui s. In eg a ion, he VLSljou nal, 13(3):301-322, Sep . 1992. 136