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.