source: vis_dev/vis-2.3/doc/blifmv.ps @ 67

Last change on this file since 67 was 14, checked in by cecile, 13 years ago

vis2.3

File size: 36.0 KB
Line 
1%!PS-Adobe-2.0
2%%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software
3%%Title: blifmv.dvi
4%%Pages: 8
5%%PageOrder: Ascend
6%%BoundingBox: 0 0 612 792
7%%DocumentFonts: Times-Roman Times-Bold Courier Times-Italic
8%%EndComments
9%DVIPSCommandLine: dvips -o blifmv.ps blifmv.dvi
10%DVIPSParameters: dpi=300, comments removed
11%DVIPSSource:  TeX output 1996.05.31:1133
12%%BeginProcSet: tex.pro
13/TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N
14/X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72
15mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1}
16ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale
17isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div
18hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul
19TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if}
20forall round exch round exch]setmatrix}N /@landscape{/isls true N}B
21/@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B
22/FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{
23/nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N
24string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N
25end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{
26/sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]
27N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup
28length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{
29128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub
30get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data
31dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N
32/rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup
33/base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx
340 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff
35setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff
36.1 sub]{ch-image}imagemask restore}B /D{/cc X dup type /stringtype ne{]}
37if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup
38length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{
39cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin
400 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul
41add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore showpage
42userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook
43known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X
44/IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for
4565781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0
460]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V
47{}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7
48getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false}
49ifelse}{false}ifelse end{{gsave TR -.1 .1 TR 1 1 scale rulex ruley false
50RMat{BDot}imagemask grestore}}{{gsave TR -.1 .1 TR rulex ruley scale 1 1
51false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave newpath transform
52round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg
53rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail
54{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M}
55B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{3 M}B /k{
564 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{
57p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p
58a}B /bos{/SS save N}B /eos{SS restore}B end
59%%EndProcSet
60%%BeginProcSet: texps.pro
61TeXDict begin /rf{findfont dup length 1 add dict begin{1 index /FID ne 2
62index /UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll
63exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics
64exch def dict begin Encoding{exch dup type /integertype ne{pop pop 1 sub
65dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def}
66ifelse}forall Metrics /Metrics currentdict end def[2 index currentdict
67end definefont 3 -1 roll makefont /setfont load]cvx def}def
68/ObliqueSlant{dup sin S cos div neg}B /SlantFont{4 index mul add}def
69/ExtendFont{3 -1 roll mul exch}def /ReEncodeFont{/Encoding exch def}def
70end
71%%EndProcSet
72TeXDict begin 40258437 52099154 1000 300 300 (blifmv.dvi)
73@start /Fa 138[23 14 16 18 1[23 21 23 35 12 2[12 1[21
7414 18 23 18 1[21 17[32 5[16 2[25 1[30 30 5[24 6[21 2[21
7521 21 2[10 46[{}27 41.666668 /Times-Bold rf /Fb 2 109
76df<06070600000000384C4C8C98181830323264643808147F930C>105
77D<3C0C181818183030303060606060C0C8C8C8D06006147F930A>108
78D E /Fc 205[15 15 49[{}2 29.166668 /Times-Roman rf /Fd
796 94 df<00800100020006000C000C00180018003000300030006000600060006000E000
80E000E000E000E000E000E000E000E000E000E000E0006000600060006000300030003000
81180018000C000C000600020001000080092A7C9E10>40 D<800040002000300018001800
820C000C000600060006000300030003000300038003800380038003800380038003800380
8303800380038003000300030003000600060006000C000C00180018003000200040008000
84092A7E9E10>I<0006000000060000000600000006000000060000000600000006000000
850600000006000000060000000600000006000000060000FFFFFFE0FFFFFFE00006000000
86060000000600000006000000060000000600000006000000060000000600000006000000
8706000000060000000600001B1C7E9720>43 D<7FFFFFC0FFFFFFE0000000000000000000
880000000000000000000000000000000000000000000000FFFFFFE07FFFFFC01B0C7E8F20
89>61 D<FEFEC0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0
90C0C0C0C0C0C0FEFE07297C9E0C>91 D<FEFE060606060606060606060606060606060606
9106060606060606060606060606060606060606FEFE0729809E0C>93
92D E /Fe 12 122 df<60F0F06004047C830C>58 D<60F0F0701010101020204080040C7C
93830C>I<0000038000000F0000003C000000F0000003C000000F0000003C000000F00000
9403C000000F0000003C000000F0000000F00000003C0000000F00000003C0000000F00000
95003C0000000F00000003C0000000F00000003C0000000F000000038019187D9520>I<E0
96000000780000001E0000000780000001E0000000780000001E0000000780000001E00000
9700780000001E00000007800000078000001E00000078000001E00000078000001E000000
9878000001E00000078000001E00000078000000E000000019187D9520>62
99D<000FC100303300400F0080060180060300060300060600040600040700000700000780
1000003F00001FF0000FFC0003FE00003E00000F00000700000300000302000302000306000
101606000606000C0600080F00300CC060083F800181E7E9C19>83 D<01C003C003C0018000
10200000000000000000000001C00270047004700870087000E000E001C001C001C00380038
1038038807080710032001C000A1C7E9B0E>105 D<1F800380038007000700070007000E00
1040E000E000E001C001C001C001C0038003800380038007000700070007000E200E200E200
105E40064003800091D7F9C0C>108 D<381F81F04E20C6184640E81C4680F01C8F00F01C8E
10600E01C0E00E01C0E00E01C1C01C0381C01C0381C01C0381C01C070380380713803807138
1070380E1380380E2700700643003003820127E9124>I<3C1F004E61804681C04701C08F01
108C08E01C00E01C00E01C01C03801C03801C03801C0700380710380710380E10380E207006
1094030038014127E9119>I<1C03270747074703870187010E010E011C021C021C021C0418
11004180818081C100C2007C010127E9114>118 D<07878008C84010F0C020F1E020E3C040
111E18000E00000E00001C00001C00001C00001C000638080F38080F38100E5810084C60078
112780013127E9118>120 D<1C00C02701C04701C04701C08703808703800E03800E03801C
11307001C07001C07001C0700180E00180E00180E001C1E000C3C0007DC00001C0000180060
1143800F03000F06000E0C0004180003E0000121A7E9114>I E /Ff
115134[18 2[18 21 12 16 16 1[21 21 21 30 12 2[12 21 1[12
11618 21 18 21 21 35[28 11[21 3[14 45[{}22 41.666668 /Times-Italic
117rf /Fg 6 104 df<FFFFFF80FFFFFF8019027D8A20>0 D<400020C000606000C0300180
1181803000C0600060C0003180001B00000E00000E00001B000031800060C000C0600180300
1193001806000C0C0006040002013147A9320>2 D<03C00FF01FF83FFC7FFE7FFEFFFFFFFF
120FFFFFFFF7FFE7FFE3FFC1FF80FF003C010107E9115>15 D<400002C00006C00006C00006
121C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006
122C00006C00006C0000660000C60000C3000181C00700F01E003FF8000FE00171A7E981C>
12391 D<003C00E001C0018003800380038003800380038003800380038003800380038003
12480030007001C00F0001C0007000300038003800380038003800380038003800380038003
1258003800380018001C000E0003C0E297D9E15>102 D<F0001C0007000300038003800380
1260380038003800380038003800380038003800380018001C000E0003C00E001C001800380
127038003800380038003800380038003800380038003800380030007001C00F0000E297D9E
12815>I E /Fh 130[25 1[25 1[25 25 25 25 25 25 25 25 1[25
12925 25 25 25 25 1[25 25 25 25 25 25 25 25 25 1[25 16[25
13015[25 25 25 5[25 25 25 25 25 25 25 1[25 25 25 2[25 25
1316[25 33[{}43 41.666668 /Courier rf /Fi 134[25 25 1[25
13228 17 19 22 2[25 28 1[14 2[14 28 2[22 28 22 28 25 10[36
1331[33 28 36 2[39 1[47 33 5[30 14[25 25 25 25 25 25 25
1342[12 17 45[{}34 50.000000 /Times-Bold rf /Fj 134[29 29
1351[29 32 19 23 3[29 32 48 3[16 32 1[19 26 1[26 32 29 10[42
1361[39 32 5[55 39 2[23 2[36 3[39 14[29 29 29 3[19 45[{}28
13758.333336 /Times-Bold rf /Fk 80[23 23 49[8 1[18 21 21
13830 21 21 12 16 14 21 21 21 21 32 12 21 12 12 21 21 14
13918 21 18 21 18 10[30 1[25 23 2[23 30 30 37 25 2[14 30
1401[23 25 1[28 28 30 38 18 1[23 2[12 1[21 21 21 21 21 21
14121 21 21 12 10 14 10 23 21 14 14 14 2[21 21 1[14 33[{}69
14241.666668 /Times-Roman rf /Fl 134[25 2[25 25 14 19 17
1431[25 25 25 39 14 25 14 14 25 1[17 22 25 22 25 22 7[36
1442[36 36 30 28 5[44 1[36 1[17 1[36 3[33 33 1[46 6[25 2[25
1452[25 1[25 2[12 1[12 44[{}39 50.000000 /Times-Roman rf
146/Fm 169[51 8[63 43 2[23 2[39 3[47 20[23 45[{}7 70.833336
147/Times-Roman rf end
148%%EndProlog
149%%BeginSetup
150%%Feature: *Resolution 300dpi
151TeXDict begin
152
153%%EndSetup
154%%Page: 1 1
1551 0 bop 833 482 a Fm(BLIF-MV)823 602 y Fl(Y)-6 b(uji)12
156b(K)o(ukimoto)823 695 y(The)h(VIS)e(Group)637 754 y(Uni)o(v)o(ersity)h
157(of)g(California,)g(Berkele)o(y)727 812 y(vis@ic.eecs.berkele)o(y)m
158(.edu)839 908 y(May)g(31,)h(1996)324 1062 y Fk(BLIF-MV)i(is)g(a)h
159(language)f(designed)g(for)g(describing)f(hierarchical)h(sequential)g
160(systems)262 1112 y(with)c(non-determinism.)19 b(A)13
161b(system)f(can)h(be)g(composed)f(of)g(interacting)f(sequential)h
162(systems,)262 1162 y(each)17 b(of)f(which)g(can)h(be)f(again)g
163(described)h(as)g(a)g(collection)e(of)h(communicating)f(sequential)262
1641211 y(systems.)g(This)8 b(makes)h(it)f(possible)f(to)h(describe)h
165(systems)g(in)f(a)h(hierarchical)f(fashion.)14 b(Although)262
1661261 y(BLIF)m(,)h(the)f(input)g(language)h(for)f(the)h(logic)f
167(optimization)f(system)j(SIS,)f(also)g(has)g(constructs)262
1681311 y(for)e(describing)h(hierarchies,)i(the)o(y)f(are)g(automatically)
169e(\257attened)i(into)e(a)i(single-le)o(v)o(el)f(circuit)262
1701361 y(once)k(the)o(y)g(are)h(read)g(in)f(because)i(the)e(internal)f
171(data)h(structure)g(of)g(SIS)g(does)h(not)e(support)262
1721411 y(hierarchical)h(representations.)39 b(In)18 b(VIS,)h(ho)o(we)o(v)
173o(er)n(,)i(the)d(original)f(hierarchy)h(is)g(preserv)o(ed)262
1741460 y(in)c(internal)h(data)h(structures)f(so)g(that)g(true)g
175(hierarchical)h(synthesis/v)o(eri\256cation)e(is)h(possible.)262
1761510 y(Another)9 b(important)g(e)o(xtension)h(to)g(BLIF)g(is)g(that)g
177(BLIF-MV)g(can)h(describe)g(non-deterministic)262 1560
178y(beha)o(viors.)30 b(This)16 b(is)f(done)g(by)h(allo)o(wing)d
179(non-deterministic)h(gates)i(in)f(descriptions.)29 b(Non-)262
1801610 y(deterministic)9 b(gates)i(generate)g(an)h(output)c(arbitrarily)h
181(from)i(the)f(set)h(of)g(pre-speci\256ed)g(outputs.)262
1821660 y(These)i(allo)o(w)e(us)h(to)g(model)g(non-deterministic)e
183(systems)j(in)e(the)h(VIS)g(en)n(vironment,)g(which)g(is)262
1841709 y(crucial)i(in)f(formal)h(v)o(eri\256cation)g(since)h(designs)e
185(in)h(early)g(stages)h(are)g(likely)d(to)i(contain)g(non-)262
1861759 y(determinism.)k(Lastly)11 b(BLIF-MV)g(supports)f(multi-v)o(alued)
187g(v)o(ariables,)i(which)f(can)h(be)g(used)f(to)262 1809
188y(simplify)d(system)j(descriptions.)262 1949 y Fj(1)58
189b(Syntax)262 2050 y Fi(1.1)50 b(Models)262 2128 y Fk(A)9
190b(model)h(is)f(a)i(system)f(that)f(can)h(be)g(used)g(in)f(de\256ning)g
191(a)h(hierarchical)g(system.)15 b(An)o(y)10 b(BLIF-MV)262
1922178 y(\256le)f(contains)h(one)f(or)h(more)g(model)g(de\256nitions.)j
193(If)d(there)g(is)f(more)h(than)g(one)f(model)h(de\256nition,)262
1942228 y(one)e(model)g(is)g(speci\256ed)h(as)g(the)f(root)g(model)g(by)g
195(putting)e(the)i Fh(.root)g Fk(construct)f(in)h(the)g(ne)o(xt)g(line)
196262 2278 y(of)h(the)g Fh(.model)g Fk(declaration.)14
197b(An)9 b(entire)g(hierarchy)g(is)g(created)h(from)g(this)e(model)h
198(recursi)o(v)o(ely)m(.)262 2327 y(If)h(no)g(model)g(is)g(declared)h(as)
199g(the)f(root)g(model,)g(the)h(\256rst)f(model)g(serv)o(es)i(as)f(the)f
200(root)f(mode.)16 b(The)262 2377 y Fh(.root)10 b Fk(construct)h(can)h
201(optionally)d(ha)o(v)o(e)j(an)g(ar)o(gument,)g(which)f(speci\256es)h
202(the)f(instance)h(name)967 2574 y(1)p eop
203%%Page: 2 2
2042 1 bop 262 307 a Fk(of)12 b(the)g(root)f(node.)21 b(If)12
205b(no)g(ar)o(gument)g(is)h(used,)g(the)f(instance)h(name)g(is)f(the)g
206(same)i(as)f(the)f(model)262 357 y(name.)k(A)10 b(model)g(is)g
207(declared)h(as)g(follo)o(ws:)262 440 y Fh(.model)24 b(<model-name>)262
208490 y(.inputs)g(<input-list>)262 540 y(.outputs)g(<output-list>)262
209590 y(<command>)262 639 y(...)262 689 y(<command>)262
210739 y(.end)324 822 y Fg(\017)c Ff(model-name)6 b Fk(is)g(a)g(string)g
211(gi)o(ving)g(the)g(name)g(of)g(the)g(model.)12 b(A)6
212b(string)g(should)g(be)g(composed)365 872 y(of)11 b(lo)o(wer)o
213(-case/upper)o(-case)h(alphabetic)e(characters,)j(numbers,)e(or)f
214(symbols)g($,)h Fe(<)p Fk(,)h Fe(>)p Fk(,)p 1671 872
21513 2 v 26 w(,)365 922 y(?,)f(|,)h(+,)f(*,)f(@.)16 b(An)o(y)10
216b(string)f(used)h(in)g(BLIF-MV)g(has)h(to)f(satisfy)f(this)h
217(constraint.)324 1002 y Fg(\017)20 b Ff(input-list)9
218b Fk(is)i(a)i(white-space)e(separated)i(list)d(of)i(strings)e
219(\(terminated)h(by)h(the)f(end)h(of)f(the)365 1051 y(line\))16
220b(gi)o(ving)e(the)i(formal)g(input)f(terminals)h(for)f(the)h(model)g
221(being)g(declared.)34 b(If)16 b(this)365 1101 y(is)f(the)g(root)g
222(model,)h(then)f(signals)g(can)h(be)f(identi\256ed)f(as)i(the)f
223(primary)g(inputs)f(of)h(this)365 1151 y(system.)h Ff(input-list)7
224b Fk(can)j(be)g(null,)f(in)g(which)h(case)h(the)f Fh(.inputs)f
225Fk(line)g(may)i(be)f(remo)o(v)o(ed)365 1201 y(altogether)n(.)33
226b(Multiple)15 b Fh(.inputs)h Fk(lines)g(are)i(allo)o(wed,)g(and)e(the)h
227(lists)e(of)i(inputs)e(are)365 1251 y(concatenated.)324
2281330 y Fg(\017)20 b Ff(output-list)12 b Fk(is)j(a)h(white-space)f
229(separated)h(list)e(of)h(strings)f(\(terminated)g(by)h(the)g(end)g(of)
230365 1380 y(the)h(line\))e(gi)o(ving)g(the)h(formal)g(output)f
231(terminals)h(for)f(the)i(model)f(being)g(declared.)31
232b(If)365 1430 y(this)14 b(is)h(the)g(root)f(model,)i(then)e(signals)h
233(can)g(be)g(identi\256ed)f(as)i(the)f(primary)f(output)f(of)365
2341480 y(this)i(system.)33 b Ff(output-list)13 b Fk(can)k(be)f(null,)h
235(in)e(which)h(case)h(the)f Fh(.outputs)g Fk(line)f(may)365
2361530 y(be)e(remo)o(v)o(ed)g(altogether)n(.)21 b(Multiple)10
237b Fh(.outputs)i Fk(lines)g(are)h(allo)o(wed,)g(and)f(the)h(lists)e(of)
238365 1579 y(outputs)e(are)i(concatenated.)324 1659 y Fg(\017)20
239b Fk(Input)9 b(v)o(ariables)i(and)f(output)f(v)o(ariables)h(ha)o(v)o(e)
240i(to)e(be)g(disjoint,)f(i.e.)16 b(a)11 b(v)o(ariable)f(cannot)g(be)365
2411709 y(both)f(an)i(input)e(and)h(an)h(output)d(in)i(a)h(model.)324
2421789 y Fg(\017)20 b Ff(command)14 b Fk(is)g(one)g(of)f
243Fh(.mv)p Fk(,)i Fh(.table)p Fk(,)g Fh(.latch)p Fk(,)g
244Fh(.reset)e Fk(and)h Fh(.subckt)p Fk(,)h(which)365 1839
245y(de\256nes)f(the)f(detailed)g(functionality)e(of)h(the)i(model.)24
246b(All)12 b(the)h Fh(.mv)g Fk(declarations)g(must)365
2471888 y(precede)f(the)e(others)g(in)f(a)i(model)f(declaration.)262
2482006 y Fi(1.2)50 b(Multi-valued)9 b(V)-5 b(ariables)262
2492084 y Fk(A)14 b(multi-v)o(alued)e(v)o(ariable)i(is)g(a)h(v)o(ariable)f
250(that)g(can)h(take)f(a)h(\256nite)e(number)i(of)f(v)o(alues.)27
251b(There)262 2133 y(are)18 b(two)e(classes)i(of)f(multi-v)o(alued)f(v)o
252(ariables.)36 b(The)18 b(class)g(of)f Ff(enumer)o(ative)h(variables)f
253Fk(are)262 2183 y(v)o(ariables)10 b(whose)h(domain)g(is)g(the)f
254Fe(n)h Fk(inte)o(gers)g Fg(f)p Fk(0)p Fe(;)c(:)g(:)g(:)t(;)g(n)i
255Fg(\000)h Fk(1)p Fg(g)p Fk(.)17 b(Note)10 b(that)h(Boolean)f(v)o
256(ariables)262 2233 y(are)f(enumerati)o(v)o(e)h(v)o(ariables)f(where)h
257Fe(n)h Fd(=)h Fk(2.)j(Enumerati)o(v)o(e)9 b(v)o(ariables)g(are)h
258(declared)g(as)g(follo)o(ws.)262 2316 y Fh(.mv)24 b
259(<variable-name-list>)f(<number-of-values>)324 2399 y
260Fg(\017)d Ff(variable-name-list)8 b Fk(is)i(a)h(comma)g(separated)g
261(list)e(of)h(strings)f(\(terminated)g(by)h(the)g(end)g(of)365
2622449 y(the)g(line\))g(gi)o(ving)e(the)i(names)i(of)e(v)o(ariables)g
263(being)g(declared.)967 2574 y(2)p eop
264%%Page: 3 3
2653 2 bop 324 307 a Fg(\017)20 b Ff(number)o(-of-values)10
266b Fk(is)g(a)h(natural)e(number)n(,)i(which)f(speci\256es)h(the)f
267(number)h(of)f(v)o(alues)g Fe(n)p Fk(.)324 390 y Fg(\017)20
268b Fk(Example:)15 b Fh(.mv)25 b(x,y)g(3)p Fk(.)324 482
269y(The)8 b(second)h(class,)g Ff(symbolic)f(variables)p
270Fk(,)g(is)g(more)h(general)f(than)f(the)h(\256rst)g(one.)14
271b(A)8 b(symbolic)262 531 y(v)o(ariable)f(can)h(take)g(a)g(set)f(of)h
272(arbitrary)e(v)o(alues.)15 b(F)o(or)7 b(e)o(xample,)j(a)e(v)o(ariable)f
273(that)g(takes)h(three)g(v)o(alues)262 581 y(red,)h(green,)h(and)g(blue)
274e(is)h(a)h(symbolic)e(v)o(ariable.)15 b(Symbolic)8 b(v)o(ariables)h
275(are)h(declared)g(as)g(follo)o(ws.)262 672 y Fh(.mv)24
276b(<variable-name-list>)f(<number-of-values>)g(<value-list>)324
277764 y Fg(\017)d Ff(variable-name-list)11 b Fk(and)i Ff(number)o
278(-of-values)f Fk(are)i(the)e(same)j(as)e(for)g(the)g(declaration)f(of)
279365 814 y(enumerati)o(v)o(e)f(v)o(ariables.)324 897 y
280Fg(\017)20 b Ff(value-list)10 b Fk(is)h(a)h(white-space)g(separated)g
281(list)e(of)h(strings)f(\(terminated)h(by)g(the)g(end)g(of)g(the)365
282946 y(line\))c(gi)o(ving)f(the)h(list)g(of)g(v)o(alues)h(the)f(v)o
283(ariable)h(can)g(take.)14 b(The)8 b(number)g(of)f(v)o(alues)h(declared)
284365 996 y(and)j(the)f(range)g(size)h(should)e(match.)324
2851079 y Fg(\017)20 b Fk(Example:)15 b Fh(.mv)25 b(x,y)g(3)f(red)h(green)
286g(blue)p Fk(.)324 1171 y(If)9 b(a)h(v)o(ariable)f(is)g(not)g(de\256ned)
287g(using)g Fh(.mv)g Fk(in)g(a)h(model,)g(then)f(the)g(v)o(ariable)g(is)g
288(assumed)i(to)d(be)262 1220 y(a)i(Boolean)g(v)o(ariable.)324
2891270 y(T)m(wo)g(v)o(ariables)g(are)h(said)f(to)g(ha)o(v)o(e)h(the)f
290(same)i(type)e(if)313 1353 y(1.)21 b(the)10 b(v)o(ariables)h(are)g
291(enumerati)o(v)o(e)g(v)o(ariables)f(with)f(the)h(same)i(domain)e(size,)
292h(or)313 1436 y(2.)21 b(the)15 b(v)o(ariables)g(are)h(symbolic)e(v)o
293(ariables)h(with)f(the)h(same)i(domain)e(size)g(and)g(the)g(same)365
2941486 y(symbolic)10 b(v)o(alues)g(de\256ned)h(in)f(the)g(same)h(order)f
295(in)g(the)g Fh(.mv)g Fk(construct.)262 1569 y(Consider)f(the)h(follo)o
296(wing)e(e)o(xample.)262 1652 y Fh(.mv)24 b(x)h(2)262
2971702 y(.mv)f(y)h(2)g(red)f(blue)262 1785 y Fe(x)7 b Fk(and)g
298Fe(y)j Fk(are)e(not)e(of)h(the)h(same)g(type)f(because)i
299Fe(x)e Fk(is)h(an)f(enumerati)o(v)o(e)h(v)o(ariable)g(and)f
300Fe(y)i Fk(is)e(a)h(symbolic)262 1835 y(v)o(ariable)i(although)e(both)h
301(are)i(two-v)o(alued)e(v)o(ariables.)262 1918 y Fh(.mv)24
302b(x)h(2)g(red)f(blue)262 1968 y(.mv)g(y)h(2)g(blue)f(red)262
3032051 y Fe(x)13 b Fk(and)h Fe(y)h Fk(in)e(the)h(abo)o(v)o(e)h(e)o
304(xample)f(are)h(not)e(of)g(the)h(same)h(type)e(because)i(symbolic)e(v)o
305(alues)h(are)262 2100 y(de\256ned)c(in)g(dif)o(ferent)f(orders.)262
3062219 y Fi(1.3)50 b(T)-5 b(ables)262 2297 y Fk(A)14 b(table)h(is)f(an)h
307(abstract)g(representation)f(of)g(a)h(physical)f(gate.)28
308b(A)15 b(table)f(is)h(dri)o(v)o(en)f(by)g(inputs)262
3092347 y(and)g(generates)h(outputs)e(follo)o(wing)f(its)h(functionality)m
310(.)25 b(Although)12 b(a)j(real)g(gate)f(generates)h(an)262
3112397 y(output)d(deterministically)h(depending)h(on)g(what)h(inputs)e
312(are)i(supplied,)g(tables)g(in)f(BLIF-MV)262 2447 y(can)h(represent)h
313(non-deterministic)d(beha)o(viors)i(as)h(well.)29 b(The)16
314b(functionality)c(of)j(the)g(table)g(is)967 2574 y(3)p
315eop
316%%Page: 4 4
3174 3 bop 262 307 a Fk(described)13 b(as)h(a)f(symbolic)g(relation,)g
318(i.e.)25 b(the)13 b(table)g(enumerates)h(symbolically)e(all)h(the)g(v)o
319(alid)262 357 y(combination)h(of)h(v)o(alues)h(among)g(the)f(inputs)g
320(and)h(the)f(outputs.)30 b(Note)15 b(that)h(BLIF-MV)f(can)262
321407 y(handle)e(multi-output)e(tables,)k(unlike)d(BLIF)m(,)i(where)g(e)o
322(v)o(ery)h(table)e(is)h(single-output.)23 b(A)14 b(table)262
323457 y(without)9 b(input)h(represents)i(a)g(constant)f(generator)n(.)18
324b(If)12 b(the)f(table)g(allo)o(ws)g(more)h(than)f(one)h(v)o(alue)262
325506 y(for)h(its)h(output,)f(then)h(the)g(table)g(is)f(a)i
326Ff(nondeterministic)d Fk(constant)i(generator)n(,)h(which)f(we)h(call)
327262 556 y Ff(pseudo)9 b(input)p Fk(.)14 b(T)m(ables)d(are)g(declared)g
328(in)f(the)g(follo)o(wing)e(way)m(.)262 646 y Fh(.table)24
329b(<in-1>)g(<in-2>)h(...)f(<in-n>)h(->)f(<out-1>)h(<out-2>...)e(<out-m>)
330262 696 y(<relation>)262 745 y(...)262 795 y(<relation>)324
331885 y Fg(\017)d Ff(in-1)p Fk(,)p Fe(:)7 b(:)g(:)e Fk(,)p
332Ff(in-n)14 b Fk(are)j(strings)d(gi)o(ving)f(the)i(names)h(of)f(the)g
333(inputs)f(to)h(the)g(table)g(being)g(de-)365 935 y(\256ned.)h(The)10
334b(v)o(ariables)g(ha)o(v)o(e)h(to)e(be)i(de\256ned)f(using)f(the)h
335Fh(.mv)f Fk(construct)h(before)g(the)g(table.)365 984
336y(Otherwise,)h(the)o(y)f(are)h(assumed)g(to)f(be)h(Boolean)e(v)o
337(ariables.)324 1067 y Fg(\017)20 b Ff(out-1)p Fk(,)p
338Fe(:)7 b(:)g(:)e Fk(,)p Ff(out-m)14 b Fk(are)i(strings)e(gi)o(ving)f
339(the)h(names)j(of)d(the)h(outputs)e(to)i(the)g(table)f(being)365
3401116 y(de\256ned.)28 b(The)15 b(v)o(ariables)g(ha)o(v)o(e)g(to)f(be)h
341(de\256ned)g(using)e(the)h Fh(.mv)h Fk(construct)e(before)i(the)365
3421166 y(table.)g(Otherwise,)9 b(the)o(y)f(are)h(assumed)g(to)f(be)h
343(Boolean)f(v)o(ariables.)14 b(An)o(y)8 b(table)h(must)f(ha)o(v)o(e)365
3441216 y(at)j(least)f(one)g(output.)324 1298 y Fg(\017)20
345b Fk(If)10 b(a)h(table)f(has)h(a)g(single)e(output,)g
346Fh(->)h Fk(is)g(optional.)324 1388 y(A)h Ff(r)n(elation)f
347Fk(is)g(a)i(white-space)f(separated)h(non-null)d(list)g(of)i
348Fe(n)f Fd(+)f Fe(m)j Fk(strings,)e(gi)o(ving)f(a)j(v)o(alid)262
3491438 y(combination)c(of)i(v)o(alues)g(among)h(inputs)d(and)j(outputs.)i
350(The)e Fe(i)p Fk(-th)f(string)e(in)i(a)h(relation)e(speci\256es)262
3511488 y(a)k(set)g(of)f(v)o(alues)h(for)f(the)g Fe(i)p
352Fk(-th)h(v)o(ariable)f(in)g(the)g(input/output)d(declaration)j(of)h
353Fh(.table)p Fk(.)22 b(Each)262 1537 y(relation)6 b(denotes)i(the)f
354(Cartesian)h(product)f(of)g(all)h(the)f(sets)h(of)g(v)o(alues.)14
355b(The)9 b(input-outpu)o(t)c(relation)262 1587 y(of)12
356b(a)h(table)f(is)g(de\256ned)h(as)g(the)f(union)g(of)g(all)g(the)g
357(relations.)21 b(A)13 b(set)f(of)g(v)o(alues)h(can)g(be)g(declared)262
3581637 y(recursi)o(v)o(ely)d(in)f(the)h(follo)o(wing)e(form.)313
3591726 y(1.)21 b(a)11 b(v)o(alue)f Fe(v)q Fk(,)i(or)313
3601809 y(2.)21 b Fg(\000)p Fk(,)11 b(which)f(is)g(the)g(uni)o(v)o(erse,)h
361(or)313 1891 y(3.)21 b(a)11 b(range)g Fg(f)p Fe(v)538
3621897 y Fc(1)563 1891 y Fg(\000)f Fe(v)625 1897 y Fc(2)642
3631891 y Fg(g)p Fk(,)g(or)313 1973 y(4.)21 b(a)11 b(list)e
364Fd(\()p Fe(S)496 1979 y Fc(1)513 1973 y Fe(;)e(S)557
3651979 y Fc(2)574 1973 y Fe(;)g(:)g(:)g(:)e(;)i(S)692 1979
366y Fb(l)704 1973 y Fd(\))p Fk(,)k(where)g Fe(S)878 1979
367y Fb(i)903 1973 y Fk(\()p Fe(i)g Fd(=)h Fk(1)p Fe(;)7
368b(:)g(:)g(:)e(;)i(l)q Fk(\))j(is)g(a)g(set)h(of)f(v)o(alues,)h(or)313
3692056 y(5.)21 b(!)p Fe(S)r Fk(,)12 b(which)e(is)g(a)g(complement)h(of)f
370(a)h(set)f(of)g(v)o(alues)h Fe(S)r Fk(.)324 2145 y(Let)e
371Fe(x)g Fk(be)g(an)g(enumerati)o(v)o(e)h(v)o(ariable)e(which)h(takes)f
372(4)h(v)o(alues.)15 b(The)9 b(follo)o(wing)e(are)i(e)o(xamples)262
3732195 y(of)g(a)i(set)g(of)f(v)o(alues)g(for)g Fe(x)p Fk(.)324
3742285 y Fg(\017)20 b Fk(1)324 2367 y Fg(\017)g(\000)324
3752449 y(\017)g(f)p Fk(2)9 b Fg(\000)h Fk(3)p Fg(g)967
3762574 y Fk(4)p eop
377%%Page: 5 5
3785 4 bop 324 307 a Fg(\017)20 b Fd(\()p Fk(0)p Fe(;)7
379b Fg(f)p Fk(2)h Fg(\000)i Fk(3)p Fg(g)p Fd(\))324 390
380y Fg(\017)20 b Fk(!)p Fg(f)p Fk(2)9 b Fg(\000)g Fk(3)p
381Fg(g)324 482 y Fk(If)g(a)i(v)o(ariable)e(is)h(a)g(symbolic)f(v)o
382(ariable,)h(the)g(range)g(construct)f(in)g(the)g(abo)o(v)o(e)i(cannot)f
383(be)g(used)262 531 y(since)g Fg(f)p Fk(red-green)p Fg(g)p
384Fk(,)g(for)g(e)o(xample,)i(does)f(not)e(make)i(sense.)324
385581 y(Let)f(us)h(consider)f(the)g(follo)o(wing)e(e)o(xample.)262
386672 y Fh(.mv)24 b(x,y)h(4)262 722 y(.table)f(x)h(->)f(y)262
387772 y(!2)g({1-3})262 822 y(-)g(0)262 872 y(2)g(\(0,3\))324
388963 y Fk(The)13 b(relation)e(speci\256ed)i(in)f(this)f(table)h(is:)18
389b Fd([\()p Fk(0)p Fe(;)7 b Fk(1)p Fe(;)g Fk(3)p Fd(\))i
390Fg(\002)h Fd(\()p Fk(1)p Fe(;)d Fk(2)p Fe(;)g Fk(3)p
391Fd(\)])i Fg([)h Fd([\()p Fk(0)p Fe(;)d Fk(1)p Fe(;)g
392Fk(2)p Fe(;)g Fk(3)p Fd(\))g Fg(\002)k Fd(\()p Fk(0)p
393Fd(\)])f Fg([)262 1013 y Fd([\()p Fk(2)p Fd(\))e Fg(\002)i
394Fd(\()p Fk(0)p Fe(;)d Fk(3)p Fd(\)])p Fk(.)262 1123 y
395Fa(1.3.1)41 b(=)10 b(Construct)262 1201 y Fk(One)j(can)h(also)f(use)h
396(the)f Ff(=)g(construct)g Fk(in)g(table)g(speci\256cations.)24
397b(Assume)14 b(that)e(in)h(the)g(column)262 1251 y(corresponding)8
398b(to)i(v)o(ariable)g Fe(y)q Fk(,)i(we)e(ha)o(v)o(e)i
399Fd(=)g Fe(x)e Fk(as)h(in)e(the)h(follo)o(wing)e(e)o(xample.)262
4001342 y Fh(.table)24 b(x)h(->)f(y)262 1392 y(-)g(=x)324
4011483 y Fk(The)11 b(interpretation)d(of)h(this)h(construct)f(is)h(that)g
402(the)g(v)o(alue)g(of)g Fe(y)i Fk(should)d(be)h(equal)g(to)g
403Fe(x)p Fk(.)15 b(This)262 1533 y(enables)10 b(us)h(to)e(describe)i(a)g
404(multi-v)o(alued)d(multiple)o(xor)h(compactly)h(\(see)h(belo)o(w\).)262
4051616 y Fh(.mv)24 b(select)g(2)262 1666 y(.mv)g(data0,data1,output)f
406(256)262 1716 y(.table)h(select)g(data0)h(data1)f(->)h(output)262
4071766 y(0)f(-)h(-)g(=data0)262 1816 y(1)f(-)h(-)g(=data1)262
4081899 y Fk(Note)11 b(that)h(two)f(v)o(ariables)h(related)g(with)f(the)h
409(=)h(construct)f(should)e(be)j(of)f(the)g(same)h(type.)21
410b(An)o(y)262 1948 y(v)o(ariable)10 b(referred)g(to)g(with)f(the)h(=)h
411(construct)f(must)g(be)g(an)h(input)e(of)h(the)g(table.)262
4122059 y Fa(1.3.2)41 b(Default)10 b(Output)262 2137 y Fk(It)e(is)h
413(sometimes)h(con)n(v)o(enient)g(to)e(de\256ne)i(a)g(default)e(output)g
414(for)h(the)g(input)f(patterns)h(not)f(speci\256ed)262
4152187 y(in)g(a)h(gi)o(v)o(en)g(relation.)14 b(The)9 b
416Fh(.default)g Fk(construct)f(is)h(used)g(for)f(this)g(purpose.)15
417b(In)8 b(the)h(follo)o(wing)262 2236 y(e)o(xample,)i(no)e(relation)g
418(is)g(speci\256ed)i(for)e(the)g(case)j(where)e(either)f
419Fe(x)p Fk(1)g(or)h Fe(x)p Fk(2)f(is)h(0.)k(Since)d(we)f(ha)o(v)o(e)262
4202286 y(a)f(default)f(statement)h(in)f(the)h(table,)g(output)e(00)h(is)h
421(related)g(for)f(those)h(unspeci\256ed)g(input)e(patterns.)262
4222336 y(Therefore,)14 b(the)f(relation)f(of)h(this)f(table)g(is:)20
423b Fd([\()p Fk(1)p Fd(\))10 b Fg(\002)h Fd(\()p Fk(1)p
424Fd(\))g Fg(\002)g Fd(\()p Fk(1)p Fd(\))g Fg(\002)g Fd(\()p
425Fk(1)p Fd(\)])f Fg([)h Fd([\()p Fk(0)p Fd(\))f Fg(\002)h
426Fd(\()p Fk(0)p Fd(\))g Fg(\002)g Fd(\()p Fk(0)p Fd(\))f
427Fg(\002)262 2386 y Fd(\()p Fk(0)p Fd(\)])f Fg([)g Fd([\()p
428Fk(0)p Fd(\))g Fg(\002)h Fd(\()p Fk(1)p Fd(\))g Fg(\002)g
429Fd(\()p Fk(0)p Fd(\))g Fg(\002)g Fd(\()p Fk(0)p Fd(\)])f
430Fg([)g Fd([\()p Fk(1)p Fd(\))h Fg(\002)g Fd(\()p Fk(0)p
431Fd(\))f Fg(\002)h Fd(\()p Fk(0)p Fd(\))g Fg(\002)g Fd(\()p
432Fk(0)p Fd(\)])p Fk(.)18 b(Each)12 b(table)f(can)h(ha)o(v)o(e)g(at)f
433(most)262 2436 y(one)f Fh(.default)f Fk(declaration.)967
4342574 y(5)p eop
435%%Page: 6 6
4366 5 bop 262 307 a Fh(.mv)24 b(x1,x2,y1,y2)g(2)262 357
437y(.table)g(x1)h(x2)f(->)h(y1)g(y2)262 407 y(.default)f(0)g(0)262
438457 y(1)g(1)h(1)g(1)324 548 y Fk(The)8 b Fh(.default)g
439Fk(construct)f(can)h(be)g(used)g(e)o(v)o(en)h(for)e(tables)h(without)e
440(inputs.)13 b(Ho)o(we)o(v)o(er)n(,)d(one)262 598 y(has)i(to)g(be)g
441(careful)g(about)g(the)g(semantics.)21 b(There)13 b(are)g(two)e
442(possible)g(cases.)23 b(One)12 b(case)i(is)d(that)262
443648 y(a)g(table)f(has)h(a)g(default)f(declaration,)h(b)o(ut)f(has)h(no)
444f(relation)g(speci\256ed,)h(where)h(the)e(interpretation)262
445697 y(of)i(the)g(table)h(is)f(that)g(it)g(always)g(takes)h(the)f
446(default.)21 b(The)14 b(other)e(case)i(is)e(that)g(a)h(table)g(has)g
447(both)262 747 y(a)f(default)g(declaration)g(and)g(a)h(non-null)e
448(relation)g(speci\256ed,)j(then)e(the)g(default)g(can)h(be)g(simply)262
449797 y(ignored.)262 916 y Fi(1.4)50 b(Latches)12 b(and)g(Reset)g(T)-5
450b(ables)262 994 y Fk(A)10 b(latch)g(is)g(a)h(storage)g(element)f(which)
451g(updates)h(its)e(stored)h(v)o(alue)h(at)f(e)o(v)o(ery)h(clock)g(tick.)
452k(A)10 b(latch)262 1043 y(has)h(an)g(input)f(and)h(an)g(output.)16
453b(At)11 b(each)h(clock)f(tick)f(the)h(latch)g(output)e(is)i(set)g(to)g
454(the)f(latch)h(input)262 1093 y(v)o(alue)g(before)g(the)g(tick,)g(and)h
455(keep)f(the)g(v)o(alue)g(till)f(the)h(ne)o(xt)g(clock)h(tick.)17
456b(Ev)o(ery)12 b(latch)f(has)h(to)e(be)262 1143 y(initialized)g
457(although)h(the)h(latch)g(is)g(allo)o(wed)g(to)g(ha)o(v)o(e)i(more)e
458(than)g(one)h(initial)d(v)o(alue,)j(in)f(which)262 1193
459y(case)h(the)f(latch)g(takes)g(an)g(initial)e(v)o(alue)i
460(nondeterministically)e(from)h(the)h(speci\256ed)h(v)o(alues.)21
461b(A)262 1243 y(latch)14 b(can)g(be)h(seen)g(as)g(a)g(multi-v)o(alued)d
462(\257ip-\257op)h(with)g(possibly)g(multiple)g(initial)f(states.)27
463b(In)262 1293 y(BLIF-MV)-5 b(,)9 b(there)i(is)f(an)g(implicit)e
464(assumption)i(that)f(the)h(whole)g(system)g(is)g(clocked)g(by)g(a)g
465(single)262 1342 y(global)f(clock)h(although)f(the)h(clock)g(is)g(ne)o
466(v)o(er)h(declared)g(in)f(BLIF-MV)g(declarations.)324
4671392 y(A)g(latch)g(is)g(declared)h(as)g(follo)o(ws.)262
4681483 y Fh(.latch)24 b(<latch-input>)g(<latch-output>)324
4691575 y Ff(latc)o(h)11 b(input)f Fk(and)h Ff(latc)o(h)g(output)f
470Fk(are)i(strings,)f(gi)o(ving)f(the)h(name)i(of)e(the)g(latch)g(input)f
471(and)i(the)262 1625 y(latch)h(output.)24 b(The)14 b(two)e(v)o(ariables)
472i(should)f(be)g(of)h(the)f(same)i(type.)25 b(A)14 b(latch)g(must)f(ha)o
473(v)o(e)i(one)262 1674 y(reset)d(table,)h(which)f(is)h(used)f(to)g
474(initialize)f(the)h(latch)g(output)f(at)h(the)g(be)o(ginning.)21
475b(A)12 b(reset)h(table)262 1724 y(is)e(a)h(single)f(output)f(table)i
476(whose)g(only)e(output)g(is)i(the)f(output)f(of)i(a)g(latch.)19
477b(Notice)12 b(that)f(we)h(use)262 1774 y Fh(.reset)c
478Fk(instead)h(of)g Fh(.table)g Fk(for)g(reset)g(tables.)15
479b(If)9 b(a)h(latch)f(is)g(reset)g(to)g(a)h(constant)e(v)o(alue,)i(then)
480262 1824 y(the)f(latch)h(table)g(has)g(no)g(input.)j(The)e(follo)o
481(wing)c(e)o(xample)k(is)f(for)g(the)f(latch)h Ff(latc)o(h)p
4821459 1824 13 2 v 14 w(output)f Fk(whose)262 1874 y(reset)h(state)h(is)f
483(0.)262 1965 y Fh(.reset)24 b(latch_output)262 2015 y(0)324
4842106 y Fk(One)15 b(can)g(specify)g(multiple)e(initial)g(states)i(by)f
485(specifying)g(more)h(than)f(one)h(v)o(alue)g(in)f(the)262
4862156 y(latch)9 b(output.)14 b(Adding)8 b(one)i(more)h(line)e(to)g(the)h
487(abo)o(v)o(e)h(e)o(xample,)g(the)f(latch)g(has)g(no)o(w)g(two)f
488(initial)262 2206 y(states.)262 2297 y Fh(.reset)24 b(latch_output)262
4892347 y(0)262 2397 y(1)967 2574 y Fk(6)p eop
490%%Page: 7 7
4917 6 bop 324 307 a Fk(This)13 b(is)g(one)h(way)f(to)g(introduce)f
492(non-determinism)g(in)h(system)g(descriptions.)24 b(Also,)14
493b(one)262 357 y(could)d(create)i(comple)o(x)g(reset)g(circuitry)e
494(sensiti)o(v)o(e)g(to)h(other)g(v)o(ariables)g(by)f(introducing)f
495(inputs)262 407 y(to)h(the)h(latch)f(table.)20 b(The)13
496b(follo)o(wing)c Fh(.reset)j Fk(statement)g(initializes)e(the)i(latch)g
497(to)f(1)h(if)f Fe(x)h Fk(is)g(0)262 457 y(and)e(to)g(0)g(if)f
498Fe(x)h Fk(is)h(1.)262 548 y Fh(.reset)24 b(x)h(latch_output)262
499598 y(0)f(1)262 648 y(1)g(0)262 766 y Fi(1.5)50 b(Subcir)o(cuits)262
500844 y Fk(In)16 b(a)h(model,)h(another)e(model)g(can)h(be)g
501(instantiated)e(as)i(a)g(subcircuit)f(using)f(the)h Fh(.subckt)262
502894 y Fk(construct.)262 985 y Fh(.subckt)24 b(<model-name>)g
503(<instance-name>)f(<formal-actual-list>)324 1077 y Fk(This)11
504b(construct)f(instantiates)h(a)g(reference)i(model)e
505Ff(model-name)g Fk(as)h(an)f(instance)g Ff(instance-)262
5061127 y(name)i Fk(in)f(the)h(current)g(model.)23 b Ff
507(formal-actual-list)9 b Fk(speci\256es)15 b(the)d(association)h
508(between)h(each)262 1176 y(formal)i(v)o(ariable)g(in)g
509Ff(model-name)g Fk(and)g(its)g(corresponding)f(actual)i(v)o(ariable)f
510(in)g(the)g(current)262 1226 y(model.)26 b(F)o(ormal)14
511b(v)o(ariables)g(are)g(declared)h(in)e(the)h(reference)h(model,)g
512(while)f(actual)g(v)o(ariables)262 1276 y(are)e(v)o(ariables)g
513(declared)g(in)f(the)h(current)f(model.)20 b Ff(formal-actual-li)o(st)9
514b Fk(is)i(a)i(list)d(of)i(assignments)262 1326 y(separated)f(by)f(a)g
515(white)g(space.)17 b(The)10 b(declaration)g(of)g Ff(formal-actual-li)o
516(st)d Fk(is)k(of)f(form:)262 1417 y Fh(formal-1)24 b(=)g(actual-1)h
517(formal-2)f(=)h(actual-2)f(...)g(formal-n)h(=)f(actual-n)324
5181508 y Fk(The)11 b(order)f(of)g(formal)g(v)o(ariables)g(is)g
519(unimportant.)262 1627 y Fi(1.6)50 b(Miscellaneous)12
520b(F)o(eatur)o(es)262 1705 y Fa(1.6.1)41 b(Comments)262
5211783 y Fk(An)o(y)10 b(line)f(starting)g(from)h(#)h(is)f(a)g(comment.)16
522b(It)10 b(is)g(ignored)f(by)h(the)g(parser)n(.)262 1893
523y Fa(1.6.2)41 b(Including)10 b(Files)262 1971 y Fk(The)j
524Fh(.include)g Fk(construct)f(can)i(be)f(used)h(to)e(include)h(another)f
525(\256le)i(from)e(a)i(\256le)f(being)g(read.)262 2021
526y(The)d(syntax)g(is)g Fh(.include)24 b(fileName)p Fk(.)262
5272140 y Fi(1.7)50 b(Old)11 b(Syntax)262 2218 y Fk(Pre)o(viously)m(,)e
528(the)g(three)h(constructs)f Fh(.table)p Fk(,)g Fh(.default)p
529Fk(,)h Fh(.reset)f Fk(were)h(called)g Fh(.names)p Fk(,)262
5302268 y Fh(.def)p Fk(,)17 b Fh(.r)f Fk(respecti)o(v)o(ely)m(.)33
531b(The)17 b Fh(read)p 877 2268 13 2 v 15 w(blif)p 992
5322268 V 14 w(mv)f Fk(command)h(in)f(VIS)g(supports)f(these)i(old)262
5332317 y(constructs)9 b(as)i(well.)967 2574 y(7)p eop
534%%Page: 8 8
5358 7 bop 262 307 a Fj(2)58 b(Semantics)262 400 y Fk(In)11
536b(this)g(section)h(we)h(describe)f(the)g(semantics)h(of)f(BLIF-MV)-5
537b(.)11 b(The)i(semantics)g(is)f(de\256ned)g(o)o(v)o(er)262
538450 y(\257attened)f(networks)f(where)h(all)g(the)g Fh(.subckt)f
539Fk(constructs)h(are)h(substituted)d(recursi)o(v)o(ely)i(until)262
540500 y(leaf)16 b(models.)34 b(Leaf)18 b(models)e(are)i(models)e(without)
541e(an)o(y)j Fh(.subckt)f Fk(declarations.)34 b(In)16 b(the)262
542549 y(follo)o(wing,)8 b(a)i(\257attened)h(network)e(is)h(called)g(a)h
543Ff(system)p Fk(.)324 599 y(At)g(e)o(v)o(ery)g(time)g(point,)f(the)h
544(system)h(is)f(in)f(some)i(state,)g(where)g(each)g(latch)f(has)h(a)f(v)
545o(alue.)18 b(An)262 649 y(initial)9 b(state)k(of)e(the)h(system)g(is)g
546(a)h(state)f(where)g(e)o(v)o(ery)h(latch)e(is)h(set)g(to)g(an)g
547(initial)e(state)i(declared)262 699 y(using)f(the)i Fh(.reset)f
548Fk(constructs.)22 b(Notice)13 b(that)f(the)g(system)h(can)h(ha)o(v)o(e)
549g(more)f(than)f(one)h(initial)262 749 y(state)f(in)f(general.)20
550b(At)11 b(e)o(v)o(ery)i(clock)f(tick,)g(all)f(the)h(latches)g(update)g
551(their)f(v)o(alues.)20 b(These)13 b(v)o(alues)262 798
552y(then)f(propagate)h(through)e(tables)j(until)d(all)i(the)g(wires)g(ha)
553o(v)o(e)h(a)g(consistent)e(set)h(of)g(v)o(alues.)24 b(If)13
554b(a)262 848 y(latch)f(is)g(encountered)g(during)e(the)i(propagation,)g
555(i.e.)h(an)f(output)f(of)h(a)g(table)g(is)g(an)h(input)e(of)g(an)262
556898 y(latch,)f(the)g(propagation)f(process)i(is)f(stopped.)15
557b(Note)10 b(that)g(because)i(of)e(nondeterminism,)g(gi)o(v)o(en)262
558948 y(a)g(single)g(state,)h(there)f(may)h(be)g(se)o(v)o(eral)g
559(consistent)e(sets)i(of)f(v)o(alues.)324 998 y(The)18
560b(semantics)g(can)f(be)h(seen)g(as)g(a)g(simple)f(e)o(xtension)f(of)h
561(the)g(standard)g(semantics)h(of)262 1048 y(synchronous)10
562b(single-clocked)g(digital)g(circuits.)18 b(In)11 b(fact,)h(if)f(e)o(v)
563o(ery)h(table)f(is)g(deterministic)g(and)262 1097 y(e)o(v)o(ery)k
564(latch)f(has)h(a)g(single)f(initial)f(state,)j(the)e(two)g(semantics)h
565(are)h(e)o(xactly)e(equal.)29 b(The)15 b(only)262 1147
566y(dif)o(ferences)8 b(are)i(in)d(the)i(interpretation)d(of)i
567(nondeterministic)e(tables)j(and)f(latches)h(with)e(multiple)262
5681197 y(initial)h(states)i(as)h(described)g(in)e(the)i(abo)o(v)o(e.)262
5691337 y Fj(3)58 b(The)14 b(VIS-v)h(Subset)g(of)g(BLIF-MV)262
5701430 y Fk(VIS-v)f(can)h(only)f(work)g(on)g(a)i(strict)e(subset)g(of)h
571(BLIF-MV)f(although)f(an)o(y)j(synthesis-related)262
5721480 y(commands)10 b(like)f Fh(read)p 625 1480 13 2 v
57314 w(blif)g Fk(and)h Fh(write)p 943 1480 V 15 w(blif)p
574Fk(,)f(are)i(applicable)e(to)g(the)g(full-set)g(of)g(BLIF-)262
5751529 y(MV)-5 b(.)10 b(If)g(the)g(user)g(generates)h(BLIF-MV)f(\256les)g
576(using)g(VL2MV)g(follo)o(wing)d(a)k(certain)f(restriction)262
5771579 y(\(See)15 b(the)f(VIS)g(users')h(manual)f(for)g(details\),)h(the)
578f(\256les)h(are)g(guaranteed)f(to)g(be)h(in)e(the)h(subset.)262
5791629 y(Ho)o(we)o(v)o(er)n(,)g(if)d(BLIF-MV)h(\256les)h(are)g(generated)
580g(manually)m(,)g(the)f(user)h(must)f(make)h(sure)f(that)g(the)262
5811679 y(\256les)f(are)g(in)f(the)h(VIS-v)f(subset.)17
582b(Otherwise,)11 b Fh(init)p 1045 1679 V 14 w(verify)f
583Fk(simply)g(fails,)h(thereby)f(making)262 1729 y(it)f(impossible)g(to)h
584(perform)g(the)g(v)o(eri\256cation.)324 1779 y(The)h(restriction)d(we)j
585(pose)g(is)f(as)h(follo)o(ws.)324 1862 y Fg(\017)20 b
586Fk(The)15 b(only)d(allo)o(wable)h(nondeterministic)f(tables)h(are)i
587Ff(pseudo-input)d(tables)p Fk(,)i(which)f(are)365 1911
588y(no-input,)7 b(single-output)e(tables)j(which)f(generate)i(more)f
589(than)g(one)g(output)e(nondetermin-)365 1961 y(istically)m(.)262
5902044 y(Note)k(that)h(one)g(can)h(always)f(transform)g(an)o(y)g(BLIF-MV)
591g(\256le)g(to)g(its)g(equi)o(v)o(alent)f(BLIF-MV)h(\256le)262
5922094 y(in)c(the)h(VIS-v)g(subset)g(by)g(determinizing)f(all)h
593(intermediate)g(nondeterministic)f(tables)h(by)g(adding)262
5942144 y(pseudo-inputs.)967 2574 y(8)p eop
595%%Trailer
596end
597userdict /end-hook known{end-hook}if
598%%EOF
Note: See TracBrowser for help on using the repository browser.