Asynchronous interface specification, analysis and synthesis

Asynch onous In e ace Speci ica ion, Analysis and Syn hesis  Michael Kishine sky Jo di Co adella In el Co po a ion Technical Uni e si y o Ca alonia Hillsbo o, OR, USA Ba celona, Spain Alex Kond a ye Luciano La agno The Uni e si y o Aizu Poli ecnico di To ino Aizu-Wakama su, Japan To ino, I aly Abs ac In e aces, by na u e, a e o en asynch onous since hey se e o connec ing mul iple dis- ibu ed modules/agen s wi hou common clock. Howe e , ecen de elopmen in heo y o asynch onous design in he a ea o asynch onous speci ica ions and models, analysis and e - i ica ion, syn hesis and echnology mapping, iming op imiza ion and pe o mance analysis is no widely known and a ely accep ed by indus y. The goal o his u o ial is o ill his gap and o p esen an o e iew o one popula sys em- a ic design me hodology o design o asynch onous in e ace con olle s. This me hodology is based on using Pe i ne s (PN)a o mal model ha , om he enginee ing s andpoin , is a o maliza ion o iming diag ams (wa e o ms) and om he sys em designe s andpoin is a concu en s a e machine, in which local componen s can pe o m independen o in e depen- den concu en ac ions, changing hei local s a es asynch onously. We will in oduce his model in o mally based on a simple example: a VME-bus con olle se ing eads om a de ice o a bus and w i es om he bus in o he de ice. 1 Speci ica ion wi h Pe i Ne s Le us s a wi h in oducing he Pe i Ne s speci ica ions wi h a simple example. 1.1 F om iming diag ams o PNs Figu e 1 depic s he in e ace o a de ice wi h a VME bus. The beha io o he con olle is as ollows: a eques o ead om o w i e in o he de ice is ecei ed by one o he signals DS o  Wo k pa ially suppo ed by ACiD-WG (Esp i 21949) and CICYT TIC 95-0419 DS DSw DTACK LDS LDTACK De ice VME Bus Con olle D T anscei e Da a Bus Figu e 1: VME bus con olle DS LDS LDTACK D DTACK Figu e 2: Wa e o ms o he READ cycle DS w espec i ely. In a ead cycle, a eques o ead is done h ough signal LD S . When he de ice has he da a eady ( LD T AC K ), he con olle mus open he anscei e o ans e da a o he bus (signal D ). In he w i e cycle, da a is i s ans e ed o he de ice. Nex , a eques o w i e is done ( LD S ). Once he de ice acknowledges he ecep ion o he da a ( LD T AC K ) he anscei e mus be closed o isola e he de ice om he bus. Each ansac ion mus be comple ed by a e u n- o- ze o o all in e ace signals, seeking o a maximum pa allelism be ween he bus and he de ice ope a ions. Figu e 2 shows a iming diag am o he ead cycle and Figu e 3 he co esponding o i s Ma ked G aph – a simple class o Pe i ne s, in which only concu ency and sequencing, bu no choice is allowed. All e en s in his Ma ked G aph a e in e p e ed as signal ansi ions: ising and alling signal ansi ions a e labeled wi h “ + ” and “ ; ” espec i ely. Pe i Ne s wi h such signal in e p e a ions a e called Signal T ansi ion G aphs (o STGs) [16]. APN has wo ypes o e ices: places (deno ed by ci cles) and ansi ions (deno ed by boxes), and a cs om places o ansi ions and om ansi ions o places. Places co espond o local s a es o he sys em and a e used o keeping in o ma ion abou sys em esou ces and condi ions o execu ion o ansi ions. Places can keep okens (deno ed by black do s). A oken in a place indica es ha a esou ce is a ailable o a condi ion sa is ied. In gene al mo e han one oken can be kep in a place, bu we will conside only he simples case: place can con ain no mo e han LDS+ LDTACK+ DS + LDTACK - D+ DTACK- LDS- DTACK+ D- DS - p0 p1 p2p3 p6 p7 p8 p9 p10 p5 p4 Figu e 3: STG o he READ cycle one oken (so-called sa e o 1-bounded PNs). A se o all places cu en ly ma ked wi h a oken co esponds o a cu en global s a e o he ne . Such global s a es a e called ma kings. The ini ial ma king o he PN in Figu e 3 is p 0 p 1 g . 1.2 Token game T ansi ions co espond o sys em e en s (signal ansi ionsin he example). A ansi ion is enabled i all inpu places con ain a oken. In he ini ial ma king o he PN in Figu e 3 only one ansi ion, DS + , is enabled; ano he one, LD S + , is no : only place p 1 among wo o i s inpu places, p 1 and p 2 , con ains a oken. E e y enabled ansi ion can i e. Fi ing emo es one oken om e e y inpu place o he ansi ion and pu s one oken o each o i s ou pu places. Fi ing o a ansi ion is an a omic ins an aneous ope a ion, while some unspeci ied ime can pass be ween enabling and i ing o he ansi ion. A e he i ing o ansi ion DS + he ne mo es o a new ma king p 1 p 2 g and hen LD S + becomes enabled, e c. 1.3 Concu ency This p ocess o mo ing okens a ound (a.k.a. oken game) in a ew s eps will i e ansi ion D ; . This leads he ne in o he ma king p 7 p 8 g . In his ma king wo ansi ions D T AC K ; and LD S ; become enabled. Since hei inpu places a e di e en hey do no con lic o okens and canno disable each o he . This ep esen s concu ency be ween DT AC K ; and LD S ; . In o al, he e a e ou pai s o concu en ansi ions: ( DT AC K ; LDS ; ) , ( D T AC K ;  LD T AC K ; ) , DS + LDS+ DTACK- LDTACK+ LDTACK- D+ LDS- LDTACK- DS + DTACK+ LDTACK- DTACK-DS + LDS- LDS-DTACK- DS - D- {p0,p1} {p1,p2} {p3} {p4} {p6} {p9} {p10} {p7,p8} {p0,p8} {p2,p8} {p2,p5} {p0,p5} {p5,p7} {p1,p7} 01*.11*.0 0*0.11*.0 10.11*.0 10.11.0* 10.0*1.0 10.1*0.0 10.00*.0 0*0.00.0 01*.00.0 01*.1*0.0 00.1*0.0 01.11.1* 1*1.11.1 <DS ,DTACK,LDTACK,LDS,D> 10*.11.1 Figu e 4: RG and SG o he READ cycle ( DS + LDS ; ) , and ( DS +  LD T AC K ; ) , whe e concu ency is a po en ial o i e a he same ime. 1.4 S a e g aphs Playing he oken game one can gene a e a T ansi ion Sys em (TS)– an abs ac s a e g aph in which each a c be ween a pai o s a es is labeled wi h he co esponding i ed ansi ion. Figu e 4 depic s a TS o he READ cycle i we igno e o a momen labels associa ed wi h s a es 1 . Each s a e in he TS gene a ed om a PN co esponds o a ma king, which is shown a he le om he co esponding s a e. A TS wi h s a es labeled wi h ma kings is called a eachabili y g aph o a PN. Fo Signal T ansi ion G aphs each s a e o he co esponding TS also can be associa ed wi h a bina y code o signal alues, which a e showna he igh om he s a es ( o he sake o eadabili y we sepa a e wi h do s le handshake signals, igh handshake signals, and da a anscei e con ol signal; enabled signals a e ma ked wi h an as e isk). A TS wi h s a es labeled wi h bina y codes o signals is called a s a e g aph o an STG. S a e g aphs a e o p ima y impo ance since hey o m he basis o logic syn hesis o asynch onous logic ne lis . 1.5 Choice and a bi a ion The en i onmen o he de ice has a choice o eques he ead o he w i e ope a ion. Simila ly, i an a bi a ion wi hin he de ice is in ol ed, hen he de ice i sel can in e nally make a non- 1 S a es a e deno ed wi h ci cles. Ini ial s a e is ma ked wi h a do . DS +DSw+ LDS+D+ DTACK- LDTACK+ LDS+ D+ DTACK+ DS - D- LDS- DSw- LDTACK- DTACK+ D- LDTACK+ p0 p1 p2 p3 Figu e 5: STG o READ and WRITE cycles de e minis ic choice be ween wo eques s. Choice is exp essed in PNs by choice places as shown in Figu e 5. He e places p 0 and p 3 a e choice places, places p 1 and p 2 me ge al e na i eb anches o he beha io and all o he places a e emo ed om he igu e, since hey ha e only one inpu and one ou pu a c ( hey a e called implici places and a e ep esen ed by a cs be ween wo ansi ions). In he ini ial ma king p 0 p 3 g wo inpu ansi ions a e enabled – DS w + and DS + , bu as soon as one o hem i es ano he becomes disabled, since he oken will disappea om place p 0 . 1.6 Timing ex ensions Di e en iming ex ensions ha e been p oposed o PNs o exp ess (a) assump ions abou delays and (b) deadline equi emen s. This in o ma ion could come in a o m o absolu e alues, e.g.  min max ] delay in e als associa ed wi h ansi ions o places, o in he o m o ela i e in o ma- ion, like ” ansi ion a will (o mus ) i e be o e ansi ion b ”. 2 Analysis and e i ica ion 2.1 P ope ies Analysis and e i ica ion a e used a di e en s ages o design.  P ope y e i ica ion. A e speci ying he design i is equi ed o check implemen abili y p ope ies o answe he ollowing ques ion: ”Can he speci ica ion be implemen ed wi h an asynch onous ci cui ?” [13, 15]. O he p ope ies o he speci ica ion can be o in e - es as well, e.g., absence o deadlocks, ai ness in se ing eques s, e c. Gene al pu pose e i ica ion echniques can be employed o his analysis [18].  Implemen a ion e i ica ion. A e design is done ully au oma ically o (especially) wi h some manual in e en ion i is o en desi able o check ha he implemen a ion is co ec wi h espec o he gi en speci ica ion [10, 23].  Pe o mance analysis and sepa a ion be ween e en s is equi ed (a) o de e mining la ency and h oughpu o he de ice and (b) o logic op imiza ionbased on iming in o ma ion [12, 21] (see also Sec ion 5). P ope ies equi ed o implemen abili y include:  boundedness o he PN o gua an ee ha he speci ied s a e space is ini e;  consis ency o an STG o ensu e ha ising and alling ansi ions al e na e o each signal;  comple eness o s a e encoding o check ha he e a e no con lic s in de ini ion o Boolean unc ions o each non-inpu (i.e. ou pu and in e nal) signals;  pe sis ency o he STG o e i y ha (a) no non-inpu signal ansi ion can be disabled by ano he signal ansi ion and (b) no inpu signal ansi ion can be disabled by a non-inpu signal ansi ion. The o me ensu es ha no sho gli ches, known as haza ds, can appea a he ga e ou pu s, while he la e ensu es ha no haza ds can occu a inpu s o he de ice. I all he abo e p ope ies a e sa is ied, hen he STG speci ica ion can be implemen ed as a, so-called, speed-independen ci cui [19] 2 . Speed-independence means no haza ds unde any a ia ions o ga e delays i a ia ions o some c i ical wi e delays a e o ks (so-called isoch onic o ks) s ay wi hin easonable bounds (e.g., wi hin one ga e delay). Le us illus a e wo o he abo e p ope ies wi h an example. Two s a es in he TS in Figu e 4 a e unde lined. They co espond o he di e en ma kings, p 4 g and p 2 p 8 g , bu hei bina y codes a e equal, 10110 . Mo eo e , enabling condi ions in hese wo s a es o ou pu signals LD S , and D a e di e en . The e o e, he implied alue o he nex s a e Boolean unc ion o signal LD S o ec o 10110 should be 1 ( o he i s s a e) and 0 ( o he second s a e). This is a con lic in 2 Also called quasi-delay-insensi i e in he li e a u e [17, 2] he de ini ion o he unc ion. To esol e his con lic wo me hods can be employed: (a) inse ing an addi ional s a e signal whose alue should dis inguish wo con lic s a es o (b) concu ency educ ion. In he i s case one easible solu ion is o inse ising ansi ion o he addi ional s a e signal igh be o e LD S + and i s alling ansi ion igh be o e D ; . So con lic ing s a es will be associa ed wi h di e en alues o he new s a e signal. In he second case, a possible solu ion is o emo e he con lic ing s a e p 2 p 8 g om he speci ica ion. The en i onmen should usually s ay un ouched o he composi ional easons, he e o e delaying inpu signals is no allowed. Hence, signal ansi ion DT AC K ; can be delayed un il LD S ; i es. The au oma ic echniques o sol ing he s a e encoding p oblem a e p esen ed, e.g., in [6, 26]. To illus a e he pe sis ency p ope y le us conside ansi ions DS w + and DS + in Figu e 5 assuming o a momen ha hey a e ou pu signals o be implemen ed. Bo h a e simul aneously enabled and disable each o he a e i ing. Such beha io canno be implemen ed wi hou haza ds unless special mu ual exclusion elemen s (a bi e s) a e used. 2.2 Techniques The e a e se e al echniques o igh ing wi h he “s a e explosion p oblem” in analysis o Pe i Ne -like speci ica ions.  Symbolic Bina y Decision Diag am-based (BDD) [3] a e sal o a eachabili y g aph allows i s implici ep esen a ion which is gene ally much mo e compac han an explici enume a- ion o s a es [23].  Pa ial o de educ ions ( [11], s ubbo n se s [25], iden i ica ion me hod [13]) igno es many (o e en mos ) o he s a es o analysis o ce ain p ope ies.  S uc u al p ope ies o PNs (e.g., place in a ian s) can p o ide as uppe app oxima ion o he eachabili y space [20, 9] and also can be used o dense a iable encoding o s a es in he eachabili y g aph. S uc u al educ ions a e use ul as a p ep ocessing s ep in o de o simpli y he s uc u e o he ne be o e a e sal o analysis, keeping all impo an p ope ies.  Un oldings [18, 15] a e ini e acyclic p e ixes o he PN beha io , ep esen ing all each- able ma kings. They a e o en mo e compac han he eachabili y g aph and due o he acyclic p ope y a e well-sui ed o ex ac ing o de ing ela ions be ween places and ansi- ions (concu ency, con lic and p eceding). Di e en ypes o un oldings a e also used o pe o mance analysis [12]. Figu e 6 is a esul o applying linea educ ions o he STG om Figu e 5. Using mo e elabo a e educ ions (place and ansi ion usions) i is possible o educe he whole PN om Figu e 3 o a single sel -loop ansi ion [20]. The BDD-based me hod used o de i ing he ansi ion unc ion and calcula ing he eachable ma kings o a PN a e simila o hose used o eachabili y analysis and equi alence checking o ini e s a e machines: s a ing om he ini ial ma king by i e a i e applica ion o he ansi ion unc ion he cha ac e is ic unc ion o he eachabili y se is calcula ed un il he ixed poin is eached. Howe e , he nai e encoding, one Boolean a iable pe place, can be oo cos ly o la ge designs. 0 0 1 1 00 00 00 11 11 11 0 0 0 1 1 1 00 00 00 00 11 11 11 11 0 0 0 0 1 1 1 1 00 00 00 00 00 11 11 11 11 11 0 0 0 1 1 1 00000 00000 00000 00000 00000 11111 11111 11111 11111 11111 0 0 0 0 1 1 1 1 0 0 0 1 1 1 000 000 000 000 111 111 111 111 B DCA F p5 p1 p4 p0 00 00 11 11 0 0 0 0 1 1 1 1 00 00 00 11 11 11 00 00 00 11 11 11 p2 p3 E 0 0 1 1 00 00 00 11 11 11 0 0 0 1 1 1 00 00 00 00 11 11 11 11 0 0 0 0 1 1 1 1 00 00 00 00 00 11 11 11 11 11 0 0 0 1 1 1 00000 00000 00000 00000 00000 11111 11111 11111 11111 11111 000 000 000 000 111 111 111 111 B DCA F p5 p1 p4 p0 00 00 00 11 11 11 00 00 00 11 11 11 00 00 00 11 11 11 p2 p3 E 00 00 00 11 11 11 0 0 0 1 1 1 00 00 00 11 11 11 p5 D B Figu e 6: STG a e line educ ion and wo s a e machine componen s The ollowing obse a ion can be made: he se s o places P 0 = p 2 p 3 p 5 g and P 1 = p 0 p 1 p 4 p 5 g o he PN in Figu e 6 de ine wo s a e machines [20, 9] wi h he ollowing se s o ansi ions T 0 = B D E g and T 1 = A B  C  D  F g , espec i ely. This in o ma ion can be s uc u ally ob ained by using algeb aic me hods. S a e machines (see he Figu e) co espond o place-in a ian s o he PN and p ese e hei oken coun in all eachable ma kings. The e o e, he ollowing a e wo in a ian s o he ne : I 1 ( p 2 p 3 p 5 ): p 2 + p 3 + p 5 = 1 I 2 ( p 0 p 1 p 4 p 5 ): p 0 + p 1 + p 4 + p 5 = 1 I in a ian s I 1 ( p 2 p 3 p 5 ) and I 2 ( p 0 p 1 p 4 p 5 ) a e ep esen ed as Boolean unc ions (e.g., using BDD), hen he AND ope a ion on hese wo unc ions will gi e us o his example an exac cha ac e is ic unc ion o he eachabili y se o ma kings. In gene al a conjunc ion o any se o in a ian s gi es an uppe app oxima ion o he eachabili y se , which is use ul o conse a i e e i ica ion. On he o he hand, due o he in a ian s abo e, he ollowing dense encoding o places can be p oposed: place 0 1 2 3  p p 2 00-- 0 1 p 3 01-- 0 1 p 5 1--- 1 p 0 --00 2 3 p 1 --01 2 3 p 4 --1- 2 p 5 ---- - Then, he cha ac e is ic unc ion o he eachabili y se is educed o a cons an : R ( V )= 0 1 ( 2 + 2 )+ 0 1 ( 2 + 2 )+ 0  1 : DS + csc0+ DTACK- LDS+ LDTACK- LDTACK+ LDTACK- DS +LDS- LDTACK- DTACK-LDS-DS + D+ LDS-DTACK- DTACK+ D- DS - csc0- 100000* 0*00000 100*101 1000*01 10110*1 10*1111 1*11111 011111* 01111*0 01*11*00 01*1*000 0*011*00 1011*00 101*000 0*01*000 01*0000 <DS ,DTACK,LDTACK,LDS,D,csc0> Figu e 7: SG o he READ cycle wi h comple e s a e coding. 3 Logic Syn hesis The goal o logic syn hesis is o de i e a ga e ne lis ha implemen s he beha io de ined by he speci ica ion. Fo simplici y, we willillus a e hiss ep by syn hesizinga speed-independen ci cui o he ead cycle o he VME bus (see Figu e 3). The main s eps in logic syn hesis a e he ollowing:  Encode he SG in such a way ha he comple e s a e coding p ope y holds. This may equi e he addi ion o in e nal signals.  De i e he nex -s a e unc ions o each ou pu and in e nal signal o he ci cui .  Map he unc ions on o a ne lis o ga es. 3.1 Comple e S a e Coding As men ioned in Sec ion 2.1, he SGo Figu e 4 has s a e con lic s. A possible me hod o sol e his p oblem is o inse new s a e signals ha disambigua e he encoding con lic s. Figu e 7 depic s a new SG in which a new signal, csc0, has been inse ed. Now, he nex -s a e unc ions o signals LD S and D can be uniquely de ined. The inse ion o new signals mus be done in such a way ha he esul ing SG p ese es he p ope ies o implemen abili y. [4] S. Bu ns. Gene al condi ions o he decomposi ion o s a e holding elemen s. In In e na ional Sym- posium on Ad anced Resea ch in Asynch onous Ci cui s and Sys ems, Aizu, Japan, Ma ch 1996. [5] J. Co adella, M. Kishine sky, A. Kond a ye , L. La agno, E. Pas o , and A. Yako le . Decomposi ion and echnology mapping o speed-independen ci cui s using boolean ela ions. In P oceedings o he In e na ional Con e ence on Compu e -Aided Design, pages 220–227, No embe 1997. [6] J. Co adella, M. Kishine sky, A. Kond a ye , L. La agno, and A. Yako le . A egion-based heo y o s a e assignmen in speed-independen ci cui s. IEEE T ansac ions on Compu e -Aided Design, 16(8):793–812, Augus 1997. [7] J. Co adella, M. Kishine sky, A. Kond a ye , L. La agno, and A. Yako le . Syn hesis o con ol ci cui s om STG speci ica ions. In handou s o he Summe School on Asynch onous Ci cui Design, Augus 1997. h p://www.lsi.upc.es/˜jo dic/pe i y/ e s/summe 97.ps.gz. [8] J. Co adella, M. Kishine sky, L. La agno, and A. Yako le . Syn hesizing Pe i ne s om s a e-based models. In P oceedings o he In e na ional Con e ence on Compu e -Aided Design, pages 164–171, No embe 1995. [9] J. Desel and J. Espa za. F ee-choice Pe i Ne s, olume 40 o Camb idge T ac s in Theo e ical Com- pu e Science. Camb idge Uni e si y P ess, 1995. [10] Da id L. Dill. T ace Theo y o Au oma ic Hie a chical Ve i ica ion o Speed-Independen Ci cui s. ACM Dis inguished Disse a ions. MIT P ess, 1989. [11] P. Gode oid. Using pa ial o de s o imp o e au oma ic e i ica ion me hods. In E.M Cla ke and R.P. Ku shan, edi o s, P oc. In e na ional Wo kshop on Compu e Aided Ve i ica ion, 1990. DIMACS Se ies in Disc e e Ma hema ica and Theo e ical Compu e Science, 1991, pages 321-340. [12] H. Hulgaa d, S. M. Bu ns, T. Amon, and G. Bo iello. An algo i hm o exac bounds on he ime sepa a ion o e en s in concu enc sys ems. IEEE T ansac ions on Compu e s, 44(11):1306–1317, No embe 1995. [13] M. A. Kishine sky, A. Y. Kond a ye , A. R. Taubin, and V. I. Va sha sky. Concu en Ha dwa e. The Theo y and P ac ice o Sel -Timed Design. John Wiley and Sons L d., 1994. [14] A. Kond a ye , M. Kishine sky, B. Lin, P. Vanbekbe gen, and A. Yako le . Basic ga e implemen a ion o speed-independen ci cui s. In P oceedings o he Design Au oma ion Con e ence, pages 56–62, June 1994. [15] A. Kond a ye , M. Kishine sky, A. Taubin, and S. Ten. Analysis o Pe i ne s by o de ing ela ions in educed un oldings. Fo mal Me hods in Sys em Design, 12(1):5–38, 1997. [16] L. La agno and A. Sangio anni-Vincen elli. Algo i hms o syn hesis and es ing o asynch onous ci cui s. Kluwe Academic Publishe s, 1993. [17] A. Ma in. P og amming in VLSI: F om communica ing p ocesses o delay-insensi i e ci cui s. In C. A. R. Hoa e, edi o , De elopmen s in Concu ency and Communica ions, The UT Yea o P og am- ming Se ies. Addison-Wesley, 1990. [18] K. McMillan. Symbolic Model Checking. Kluwe Academic Publishe s, 1993. [19] Da id E. Mulle and W. S. Ba ky. A heo y o asynch onous ci cui s. In P oceedings o an In e na- ional Symposium on he Theo y o Swi ching, pages 204–243. Ha a d Uni e si y P ess, Ap il 1959. [20] T. Mu a a. Pe i Ne s: P ope ies, analysis and applica ions. P oceedings o he IEEE, pages 541–580, Ap il 1989. [21] Ch is J. Mye s and Te esa H.-Y. Meng. Syn hesis o imed asynch onous ci cui s. IEEE T ansac ions on VLSI Sys ems, 1(2):106–119, June 1993. [22] S e en M. Nowick and Da id L. Dill. Exac wo-le el minimiza ion o haza d- ee logic wi h mul iple- inpu changes. IEEE T ansac ions on Compu e -Aided Design, 14(8):986–997, Augus 1995. [23] O iol Roig, Jo di Co adella, and En ic Pas o . Ve i ica ion o asynch onous ci cui s by BDD-based model checking o Pe i ne s. In 16 h In e na ional Con e ence on he Applica ion and Theo y o Pe i Ne s, olume 815 o Lec u e No es in Compu e Science, pages 374–391, 1995. [24] S. H. Unge . Asynch onous Sequen ial Swi ching Ci cui s. Wiley-In e science, John Wiley & Sons, Inc., New Yo k, 1969. [25] An i Valma i. S ubbo n se s o educed s a e space gene a ion. Lec u e No es in Compu e Science; Ad ances in Pe i Ne s 1990, 483:491–515, 1991. [26] P. Vanbekbe gen, B. Lin, G. Goossens, and H. De Man. A gene alized s a e assignmen heo y o ans o ma ions on Signal T ansi ion G aphs. Jou nal o VLSI Signal P ocessing, 7(1-2):101–116, 1994. [27] Pe e Vanbekbe gen, Albe Wand, and Ku Keu ze . A design and alida ion sys em o asynch onous ci cui s. In P oc. ACM/IEEE Design Au oma ion Con e ence, June 1995. [28] K. Y. Yun and D. L. Dill. Au oma ic syn hesis o 3D asynch onous s a e machines. In P oceedings o he In e na ional Con e ence on Compu e -Aided Design, No embe 1992.