%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: blifmv.dvi %%Pages: 8 %%PageOrder: Ascend %%BoundingBox: 0 0 612 792 %%DocumentFonts: Times-Roman Times-Bold Courier Times-Italic %%EndComments %DVIPSCommandLine: dvips -o blifmv.ps blifmv.dvi %DVIPSParameters: dpi=300, comments removed %DVIPSSource: TeX output 1996.05.31:1133 %%BeginProcSet: tex.pro /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if} forall round exch round exch]setmatrix}N /@landscape{/isls true N}B /@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B /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{ /nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{ /sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0] N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{ 128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 sub]{ch-image}imagemask restore}B /D{/cc X dup type /stringtype ne{]} if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{ cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore showpage userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V {}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7 getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false} ifelse}{false}ifelse end{{gsave TR -.1 .1 TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 .1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave newpath transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail {dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M} B /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{ 4 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{ p 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 a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet %%BeginProcSet: texps.pro TeXDict begin /rf{findfont dup length 1 add dict begin{1 index /FID ne 2 index /UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics exch def dict begin Encoding{exch dup type /integertype ne{pop pop 1 sub dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def} ifelse}forall Metrics /Metrics currentdict end def[2 index currentdict end definefont 3 -1 roll makefont /setfont load]cvx def}def /ObliqueSlant{dup sin S cos div neg}B /SlantFont{4 index mul add}def /ExtendFont{3 -1 roll mul exch}def /ReEncodeFont{/Encoding exch def}def end %%EndProcSet TeXDict begin 40258437 52099154 1000 300 300 (blifmv.dvi) @start /Fa 138[23 14 16 18 1[23 21 23 35 12 2[12 1[21 14 18 23 18 1[21 17[32 5[16 2[25 1[30 30 5[24 6[21 2[21 21 21 2[10 46[{}27 41.666668 /Times-Bold rf /Fb 2 109 df<06070600000000384C4C8C98181830323264643808147F930C>105 D<3C0C181818183030303060606060C0C8C8C8D06006147F930A>108 D E /Fc 205[15 15 49[{}2 29.166668 /Times-Roman rf /Fd 6 94 df<00800100020006000C000C00180018003000300030006000600060006000E000 E000E000E000E000E000E000E000E000E000E000E0006000600060006000300030003000 180018000C000C000600020001000080092A7C9E10>40 D<800040002000300018001800 0C000C000600060006000300030003000300038003800380038003800380038003800380 03800380038003000300030003000600060006000C000C00180018003000200040008000 092A7E9E10>I<0006000000060000000600000006000000060000000600000006000000 0600000006000000060000000600000006000000060000FFFFFFE0FFFFFFE00006000000 060000000600000006000000060000000600000006000000060000000600000006000000 06000000060000000600001B1C7E9720>43 D<7FFFFFC0FFFFFFE0000000000000000000 0000000000000000000000000000000000000000000000FFFFFFE07FFFFFC01B0C7E8F20 >61 D91 D93 D E /Fe 12 122 df<60F0F06004047C830C>58 D<60F0F0701010101020204080040C7C 830C>I<0000038000000F0000003C000000F0000003C000000F0000003C000000F00000 03C000000F0000003C000000F0000000F00000003C0000000F00000003C0000000F00000 003C0000000F00000003C0000000F00000003C0000000F000000038019187D9520>I62 D<000FC100303300400F0080060180060300060300060600040600040700000700000780 0003F00001FF0000FFC0003FE00003E00000F00000700000300000302000302000306000 606000606000C0600080F00300CC060083F800181E7E9C19>83 D<01C003C003C0018000 00000000000000000000001C00270047004700870087000E000E001C001C001C00380038 8038807080710032001C000A1C7E9B0E>105 D<1F800380038007000700070007000E00 0E000E000E001C001C001C001C0038003800380038007000700070007000E200E200E200 E40064003800091D7F9C0C>108 D<381F81F04E20C6184640E81C4680F01C8F00F01C8E 00E01C0E00E01C0E00E01C1C01C0381C01C0381C01C0381C01C070380380713803807138 0380E1380380E2700700643003003820127E9124>I<3C1F004E61804681C04701C08F01 C08E01C00E01C00E01C01C03801C03801C03801C0700380710380710380E10380E207006 4030038014127E9119>I<1C03270747074703870187010E010E011C021C021C021C0418 04180818081C100C2007C010127E9114>118 D<07878008C84010F0C020F1E020E3C040 E18000E00000E00001C00001C00001C00001C000638080F38080F38100E5810084C60078 780013127E9118>120 D<1C00C02701C04701C04701C08703808703800E03800E03801C 07001C07001C07001C0700180E00180E00180E001C1E000C3C0007DC00001C0000180060 3800F03000F06000E0C0004180003E0000121A7E9114>I E /Ff 134[18 2[18 21 12 16 16 1[21 21 21 30 12 2[12 21 1[12 18 21 18 21 21 35[28 11[21 3[14 45[{}22 41.666668 /Times-Italic rf /Fg 6 104 df0 D<400020C000606000C0300180 1803000C0600060C0003180001B00000E00000E00001B000031800060C000C0600180300 3001806000C0C0006040002013147A9320>2 D<03C00FF01FF83FFC7FFE7FFEFFFFFFFF FFFFFFFF7FFE7FFE3FFC1FF80FF003C010107E9115>15 D<400002C00006C00006C00006 C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006 C00006C00006C0000660000C60000C3000181C00700F01E003FF8000FE00171A7E981C> 91 D<003C00E001C0018003800380038003800380038003800380038003800380038003 80030007001C00F0001C0007000300038003800380038003800380038003800380038003 8003800380018001C000E0003C0E297D9E15>102 DI E /Fh 130[25 1[25 1[25 25 25 25 25 25 25 25 1[25 25 25 25 25 25 1[25 25 25 25 25 25 25 25 25 1[25 16[25 15[25 25 25 5[25 25 25 25 25 25 25 1[25 25 25 2[25 25 6[25 33[{}43 41.666668 /Courier rf /Fi 134[25 25 1[25 28 17 19 22 2[25 28 1[14 2[14 28 2[22 28 22 28 25 10[36 1[33 28 36 2[39 1[47 33 5[30 14[25 25 25 25 25 25 25 2[12 17 45[{}34 50.000000 /Times-Bold rf /Fj 134[29 29 1[29 32 19 23 3[29 32 48 3[16 32 1[19 26 1[26 32 29 10[42 1[39 32 5[55 39 2[23 2[36 3[39 14[29 29 29 3[19 45[{}28 58.333336 /Times-Bold rf /Fk 80[23 23 49[8 1[18 21 21 30 21 21 12 16 14 21 21 21 21 32 12 21 12 12 21 21 14 18 21 18 21 18 10[30 1[25 23 2[23 30 30 37 25 2[14 30 1[23 25 1[28 28 30 38 18 1[23 2[12 1[21 21 21 21 21 21 21 21 21 12 10 14 10 23 21 14 14 14 2[21 21 1[14 33[{}69 41.666668 /Times-Roman rf /Fl 134[25 2[25 25 14 19 17 1[25 25 25 39 14 25 14 14 25 1[17 22 25 22 25 22 7[36 2[36 36 30 28 5[44 1[36 1[17 1[36 3[33 33 1[46 6[25 2[25 2[25 1[25 2[12 1[12 44[{}39 50.000000 /Times-Roman rf /Fm 169[51 8[63 43 2[23 2[39 3[47 20[23 45[{}7 70.833336 /Times-Roman rf end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%EndSetup %%Page: 1 1 1 0 bop 833 482 a Fm(BLIF-MV)823 602 y Fl(Y)-6 b(uji)12 b(K)o(ukimoto)823 695 y(The)h(VIS)e(Group)637 754 y(Uni)o(v)o(ersity)h (of)g(California,)g(Berkele)o(y)727 812 y(vis@ic.eecs.berkele)o(y)m (.edu)839 908 y(May)g(31,)h(1996)324 1062 y Fk(BLIF-MV)i(is)g(a)h (language)f(designed)g(for)g(describing)f(hierarchical)h(sequential)g (systems)262 1112 y(with)c(non-determinism.)19 b(A)13 b(system)f(can)h(be)g(composed)f(of)g(interacting)f(sequential)h (systems,)262 1162 y(each)17 b(of)f(which)g(can)h(be)f(again)g (described)h(as)g(a)g(collection)e(of)h(communicating)f(sequential)262 1211 y(systems.)g(This)8 b(makes)h(it)f(possible)f(to)h(describe)h (systems)g(in)f(a)h(hierarchical)f(fashion.)14 b(Although)262 1261 y(BLIF)m(,)h(the)f(input)g(language)h(for)f(the)h(logic)f (optimization)f(system)j(SIS,)f(also)g(has)g(constructs)262 1311 y(for)e(describing)h(hierarchies,)i(the)o(y)f(are)g(automatically) e(\257attened)i(into)e(a)i(single-le)o(v)o(el)f(circuit)262 1361 y(once)k(the)o(y)g(are)h(read)g(in)f(because)i(the)e(internal)f (data)h(structure)g(of)g(SIS)g(does)h(not)e(support)262 1411 y(hierarchical)h(representations.)39 b(In)18 b(VIS,)h(ho)o(we)o(v) o(er)n(,)i(the)d(original)f(hierarchy)h(is)g(preserv)o(ed)262 1460 y(in)c(internal)h(data)h(structures)f(so)g(that)g(true)g (hierarchical)h(synthesis/v)o(eri\256cation)e(is)h(possible.)262 1510 y(Another)9 b(important)g(e)o(xtension)h(to)g(BLIF)g(is)g(that)g (BLIF-MV)g(can)h(describe)g(non-deterministic)262 1560 y(beha)o(viors.)30 b(This)16 b(is)f(done)g(by)h(allo)o(wing)d (non-deterministic)h(gates)i(in)f(descriptions.)29 b(Non-)262 1610 y(deterministic)9 b(gates)i(generate)g(an)h(output)c(arbitrarily)h (from)i(the)f(set)h(of)g(pre-speci\256ed)g(outputs.)262 1660 y(These)i(allo)o(w)e(us)h(to)g(model)g(non-deterministic)e (systems)j(in)e(the)h(VIS)g(en)n(vironment,)g(which)g(is)262 1709 y(crucial)i(in)f(formal)h(v)o(eri\256cation)g(since)h(designs)e (in)h(early)g(stages)h(are)g(likely)d(to)i(contain)g(non-)262 1759 y(determinism.)k(Lastly)11 b(BLIF-MV)g(supports)f(multi-v)o(alued) g(v)o(ariables,)i(which)f(can)h(be)g(used)f(to)262 1809 y(simplify)d(system)j(descriptions.)262 1949 y Fj(1)58 b(Syntax)262 2050 y Fi(1.1)50 b(Models)262 2128 y Fk(A)9 b(model)h(is)f(a)i(system)f(that)f(can)h(be)g(used)g(in)f(de\256ning)g (a)h(hierarchical)g(system.)15 b(An)o(y)10 b(BLIF-MV)262 2178 y(\256le)f(contains)h(one)f(or)h(more)g(model)g(de\256nitions.)j (If)d(there)g(is)f(more)h(than)g(one)f(model)h(de\256nition,)262 2228 y(one)e(model)g(is)g(speci\256ed)h(as)g(the)f(root)g(model)g(by)g (putting)e(the)i Fh(.root)g Fk(construct)f(in)h(the)g(ne)o(xt)g(line) 262 2278 y(of)h(the)g Fh(.model)g Fk(declaration.)14 b(An)9 b(entire)g(hierarchy)g(is)g(created)h(from)g(this)e(model)h (recursi)o(v)o(ely)m(.)262 2327 y(If)h(no)g(model)g(is)g(declared)h(as) g(the)f(root)g(model,)g(the)h(\256rst)f(model)g(serv)o(es)i(as)f(the)f (root)f(mode.)16 b(The)262 2377 y Fh(.root)10 b Fk(construct)h(can)h (optionally)d(ha)o(v)o(e)j(an)g(ar)o(gument,)g(which)f(speci\256es)h (the)f(instance)h(name)967 2574 y(1)p eop %%Page: 2 2 2 1 bop 262 307 a Fk(of)12 b(the)g(root)f(node.)21 b(If)12 b(no)g(ar)o(gument)g(is)h(used,)g(the)f(instance)h(name)g(is)f(the)g (same)i(as)f(the)f(model)262 357 y(name.)k(A)10 b(model)g(is)g (declared)h(as)g(follo)o(ws:)262 440 y Fh(.model)24 b()262 490 y(.inputs)g()262 540 y(.outputs)g()262 590 y()262 639 y(...)262 689 y()262 739 y(.end)324 822 y Fg(\017)c Ff(model-name)6 b Fk(is)g(a)g(string)g (gi)o(ving)g(the)g(name)g(of)g(the)g(model.)12 b(A)6 b(string)g(should)g(be)g(composed)365 872 y(of)11 b(lo)o(wer)o (-case/upper)o(-case)h(alphabetic)e(characters,)j(numbers,)e(or)f (symbols)g($,)h Fe(<)p Fk(,)h Fe(>)p Fk(,)p 1671 872 13 2 v 26 w(,)365 922 y(?,)f(|,)h(+,)f(*,)f(@.)16 b(An)o(y)10 b(string)f(used)h(in)g(BLIF-MV)g(has)h(to)f(satisfy)f(this)h (constraint.)324 1002 y Fg(\017)20 b Ff(input-list)9 b Fk(is)i(a)i(white-space)e(separated)i(list)d(of)i(strings)e (\(terminated)h(by)h(the)f(end)h(of)f(the)365 1051 y(line\))16 b(gi)o(ving)e(the)i(formal)g(input)f(terminals)h(for)f(the)h(model)g (being)g(declared.)34 b(If)16 b(this)365 1101 y(is)f(the)g(root)g (model,)h(then)f(signals)g(can)h(be)f(identi\256ed)f(as)i(the)f (primary)g(inputs)f(of)h(this)365 1151 y(system.)h Ff(input-list)7 b Fk(can)j(be)g(null,)f(in)g(which)h(case)h(the)f Fh(.inputs)f Fk(line)g(may)i(be)f(remo)o(v)o(ed)365 1201 y(altogether)n(.)33 b(Multiple)15 b Fh(.inputs)h Fk(lines)g(are)i(allo)o(wed,)g(and)e(the)h (lists)e(of)i(inputs)e(are)365 1251 y(concatenated.)324 1330 y Fg(\017)20 b Ff(output-list)12 b Fk(is)j(a)h(white-space)f (separated)h(list)e(of)h(strings)f(\(terminated)g(by)h(the)g(end)g(of) 365 1380 y(the)h(line\))e(gi)o(ving)g(the)h(formal)g(output)f (terminals)h(for)f(the)i(model)f(being)g(declared.)31 b(If)365 1430 y(this)14 b(is)h(the)g(root)f(model,)i(then)e(signals)h (can)g(be)g(identi\256ed)f(as)i(the)f(primary)f(output)f(of)365 1480 y(this)i(system.)33 b Ff(output-list)13 b Fk(can)k(be)f(null,)h (in)e(which)h(case)h(the)f Fh(.outputs)g Fk(line)f(may)365 1530 y(be)e(remo)o(v)o(ed)g(altogether)n(.)21 b(Multiple)10 b Fh(.outputs)i Fk(lines)g(are)h(allo)o(wed,)g(and)f(the)h(lists)e(of) 365 1579 y(outputs)e(are)i(concatenated.)324 1659 y Fg(\017)20 b Fk(Input)9 b(v)o(ariables)i(and)f(output)f(v)o(ariables)h(ha)o(v)o(e) i(to)e(be)g(disjoint,)f(i.e.)16 b(a)11 b(v)o(ariable)f(cannot)g(be)365 1709 y(both)f(an)i(input)e(and)h(an)h(output)d(in)i(a)h(model.)324 1789 y Fg(\017)20 b Ff(command)14 b Fk(is)g(one)g(of)f Fh(.mv)p Fk(,)i Fh(.table)p Fk(,)g Fh(.latch)p Fk(,)g Fh(.reset)e Fk(and)h Fh(.subckt)p Fk(,)h(which)365 1839 y(de\256nes)f(the)f(detailed)g(functionality)e(of)h(the)i(model.)24 b(All)12 b(the)h Fh(.mv)g Fk(declarations)g(must)365 1888 y(precede)f(the)e(others)g(in)f(a)i(model)f(declaration.)262 2006 y Fi(1.2)50 b(Multi-valued)9 b(V)-5 b(ariables)262 2084 y Fk(A)14 b(multi-v)o(alued)e(v)o(ariable)i(is)g(a)h(v)o(ariable)f (that)g(can)h(take)f(a)h(\256nite)e(number)i(of)f(v)o(alues.)27 b(There)262 2133 y(are)18 b(two)e(classes)i(of)f(multi-v)o(alued)f(v)o (ariables.)36 b(The)18 b(class)g(of)f Ff(enumer)o(ative)h(variables)f Fk(are)262 2183 y(v)o(ariables)10 b(whose)h(domain)g(is)g(the)f Fe(n)h Fk(inte)o(gers)g Fg(f)p Fk(0)p Fe(;)c(:)g(:)g(:)t(;)g(n)i Fg(\000)h Fk(1)p Fg(g)p Fk(.)17 b(Note)10 b(that)h(Boolean)f(v)o (ariables)262 2233 y(are)f(enumerati)o(v)o(e)h(v)o(ariables)f(where)h Fe(n)h Fd(=)h Fk(2.)j(Enumerati)o(v)o(e)9 b(v)o(ariables)g(are)h (declared)g(as)g(follo)o(ws.)262 2316 y Fh(.mv)24 b ()f()324 2399 y Fg(\017)d Ff(variable-name-list)8 b Fk(is)i(a)h(comma)g(separated)g (list)e(of)h(strings)f(\(terminated)g(by)h(the)g(end)g(of)365 2449 y(the)g(line\))g(gi)o(ving)e(the)i(names)i(of)e(v)o(ariables)g (being)g(declared.)967 2574 y(2)p eop %%Page: 3 3 3 2 bop 324 307 a Fg(\017)20 b Ff(number)o(-of-values)10 b Fk(is)g(a)h(natural)e(number)n(,)i(which)f(speci\256es)h(the)f (number)h(of)f(v)o(alues)g Fe(n)p Fk(.)324 390 y Fg(\017)20 b Fk(Example:)15 b Fh(.mv)25 b(x,y)g(3)p Fk(.)324 482 y(The)8 b(second)h(class,)g Ff(symbolic)f(variables)p Fk(,)g(is)g(more)h(general)f(than)f(the)h(\256rst)g(one.)14 b(A)8 b(symbolic)262 531 y(v)o(ariable)f(can)h(take)g(a)g(set)f(of)h (arbitrary)e(v)o(alues.)15 b(F)o(or)7 b(e)o(xample,)j(a)e(v)o(ariable)f (that)g(takes)h(three)g(v)o(alues)262 581 y(red,)h(green,)h(and)g(blue) e(is)h(a)h(symbolic)e(v)o(ariable.)15 b(Symbolic)8 b(v)o(ariables)h (are)h(declared)g(as)g(follo)o(ws.)262 672 y Fh(.mv)24 b()f()g()324 764 y Fg(\017)d Ff(variable-name-list)11 b Fk(and)i Ff(number)o (-of-values)f Fk(are)i(the)e(same)j(as)e(for)g(the)g(declaration)f(of) 365 814 y(enumerati)o(v)o(e)f(v)o(ariables.)324 897 y Fg(\017)20 b Ff(value-list)10 b Fk(is)h(a)h(white-space)g(separated)g (list)e(of)h(strings)f(\(terminated)h(by)g(the)g(end)g(of)g(the)365 946 y(line\))c(gi)o(ving)f(the)h(list)g(of)g(v)o(alues)h(the)f(v)o (ariable)h(can)g(take.)14 b(The)8 b(number)g(of)f(v)o(alues)h(declared) 365 996 y(and)j(the)f(range)g(size)h(should)e(match.)324 1079 y Fg(\017)20 b Fk(Example:)15 b Fh(.mv)25 b(x,y)g(3)f(red)h(green) g(blue)p Fk(.)324 1171 y(If)9 b(a)h(v)o(ariable)f(is)g(not)g(de\256ned) g(using)g Fh(.mv)g Fk(in)g(a)h(model,)g(then)f(the)g(v)o(ariable)g(is)g (assumed)i(to)d(be)262 1220 y(a)i(Boolean)g(v)o(ariable.)324 1270 y(T)m(wo)g(v)o(ariables)g(are)h(said)f(to)g(ha)o(v)o(e)h(the)f (same)i(type)e(if)313 1353 y(1.)21 b(the)10 b(v)o(ariables)h(are)g (enumerati)o(v)o(e)g(v)o(ariables)f(with)f(the)h(same)i(domain)e(size,) h(or)313 1436 y(2.)21 b(the)15 b(v)o(ariables)g(are)h(symbolic)e(v)o (ariables)h(with)f(the)h(same)i(domain)e(size)g(and)g(the)g(same)365 1486 y(symbolic)10 b(v)o(alues)g(de\256ned)h(in)f(the)g(same)h(order)f (in)g(the)g Fh(.mv)g Fk(construct.)262 1569 y(Consider)f(the)h(follo)o (wing)e(e)o(xample.)262 1652 y Fh(.mv)24 b(x)h(2)262 1702 y(.mv)f(y)h(2)g(red)f(blue)262 1785 y Fe(x)7 b Fk(and)g Fe(y)j Fk(are)e(not)e(of)h(the)h(same)g(type)f(because)i Fe(x)e Fk(is)h(an)f(enumerati)o(v)o(e)h(v)o(ariable)g(and)f Fe(y)i Fk(is)e(a)h(symbolic)262 1835 y(v)o(ariable)i(although)e(both)h (are)i(two-v)o(alued)e(v)o(ariables.)262 1918 y Fh(.mv)24 b(x)h(2)g(red)f(blue)262 1968 y(.mv)g(y)h(2)g(blue)f(red)262 2051 y Fe(x)13 b Fk(and)h Fe(y)h Fk(in)e(the)h(abo)o(v)o(e)h(e)o (xample)f(are)h(not)e(of)g(the)h(same)h(type)e(because)i(symbolic)e(v)o (alues)h(are)262 2100 y(de\256ned)c(in)g(dif)o(ferent)f(orders.)262 2219 y Fi(1.3)50 b(T)-5 b(ables)262 2297 y Fk(A)14 b(table)h(is)f(an)h (abstract)g(representation)f(of)g(a)h(physical)f(gate.)28 b(A)15 b(table)f(is)h(dri)o(v)o(en)f(by)g(inputs)262 2347 y(and)g(generates)h(outputs)e(follo)o(wing)f(its)h(functionality)m (.)25 b(Although)12 b(a)j(real)g(gate)f(generates)h(an)262 2397 y(output)d(deterministically)h(depending)h(on)g(what)h(inputs)e (are)i(supplied,)g(tables)g(in)f(BLIF-MV)262 2447 y(can)h(represent)h (non-deterministic)d(beha)o(viors)i(as)h(well.)29 b(The)16 b(functionality)c(of)j(the)g(table)g(is)967 2574 y(3)p eop %%Page: 4 4 4 3 bop 262 307 a Fk(described)13 b(as)h(a)f(symbolic)g(relation,)g (i.e.)25 b(the)13 b(table)g(enumerates)h(symbolically)e(all)h(the)g(v)o (alid)262 357 y(combination)h(of)h(v)o(alues)h(among)g(the)f(inputs)g (and)h(the)f(outputs.)30 b(Note)15 b(that)h(BLIF-MV)f(can)262 407 y(handle)e(multi-output)e(tables,)k(unlike)d(BLIF)m(,)i(where)g(e)o (v)o(ery)h(table)e(is)h(single-output.)23 b(A)14 b(table)262 457 y(without)9 b(input)h(represents)i(a)g(constant)f(generator)n(.)18 b(If)12 b(the)f(table)g(allo)o(ws)g(more)h(than)f(one)h(v)o(alue)262 506 y(for)h(its)h(output,)f(then)h(the)g(table)g(is)f(a)i Ff(nondeterministic)d Fk(constant)i(generator)n(,)h(which)f(we)h(call) 262 556 y Ff(pseudo)9 b(input)p Fk(.)14 b(T)m(ables)d(are)g(declared)g (in)f(the)g(follo)o(wing)e(way)m(.)262 646 y Fh(.table)24 b()g()h(...)f()h(->)f()h(...)e() 262 696 y()262 745 y(...)262 795 y()324 885 y Fg(\017)d Ff(in-1)p Fk(,)p Fe(:)7 b(:)g(:)e Fk(,)p Ff(in-n)14 b Fk(are)j(strings)d(gi)o(ving)f(the)i(names)h(of)f(the)g (inputs)f(to)h(the)g(table)g(being)g(de-)365 935 y(\256ned.)h(The)10 b(v)o(ariables)g(ha)o(v)o(e)h(to)e(be)i(de\256ned)f(using)f(the)h Fh(.mv)f Fk(construct)h(before)g(the)g(table.)365 984 y(Otherwise,)h(the)o(y)f(are)h(assumed)g(to)f(be)h(Boolean)e(v)o (ariables.)324 1067 y Fg(\017)20 b Ff(out-1)p Fk(,)p Fe(:)7 b(:)g(:)e Fk(,)p Ff(out-m)14 b Fk(are)i(strings)e(gi)o(ving)f (the)h(names)j(of)d(the)h(outputs)e(to)i(the)g(table)f(being)365 1116 y(de\256ned.)28 b(The)15 b(v)o(ariables)g(ha)o(v)o(e)g(to)f(be)h (de\256ned)g(using)e(the)h Fh(.mv)h Fk(construct)e(before)i(the)365 1166 y(table.)g(Otherwise,)9 b(the)o(y)f(are)h(assumed)g(to)f(be)h (Boolean)f(v)o(ariables.)14 b(An)o(y)8 b(table)h(must)f(ha)o(v)o(e)365 1216 y(at)j(least)f(one)g(output.)324 1298 y Fg(\017)20 b Fk(If)10 b(a)h(table)f(has)h(a)g(single)e(output,)g Fh(->)h Fk(is)g(optional.)324 1388 y(A)h Ff(r)n(elation)f Fk(is)g(a)i(white-space)f(separated)h(non-null)d(list)g(of)i Fe(n)f Fd(+)f Fe(m)j Fk(strings,)e(gi)o(ving)f(a)j(v)o(alid)262 1438 y(combination)c(of)i(v)o(alues)g(among)h(inputs)d(and)j(outputs.)i (The)e Fe(i)p Fk(-th)f(string)e(in)i(a)h(relation)e(speci\256es)262 1488 y(a)k(set)g(of)f(v)o(alues)h(for)f(the)g Fe(i)p Fk(-th)h(v)o(ariable)f(in)g(the)g(input/output)d(declaration)j(of)h Fh(.table)p Fk(.)22 b(Each)262 1537 y(relation)6 b(denotes)i(the)f (Cartesian)h(product)f(of)g(all)h(the)f(sets)h(of)g(v)o(alues.)14 b(The)9 b(input-outpu)o(t)c(relation)262 1587 y(of)12 b(a)h(table)f(is)g(de\256ned)h(as)g(the)f(union)g(of)g(all)g(the)g (relations.)21 b(A)13 b(set)f(of)g(v)o(alues)h(can)g(be)g(declared)262 1637 y(recursi)o(v)o(ely)d(in)f(the)h(follo)o(wing)e(form.)313 1726 y(1.)21 b(a)11 b(v)o(alue)f Fe(v)q Fk(,)i(or)313 1809 y(2.)21 b Fg(\000)p Fk(,)11 b(which)f(is)g(the)g(uni)o(v)o(erse,)h (or)313 1891 y(3.)21 b(a)11 b(range)g Fg(f)p Fe(v)538 1897 y Fc(1)563 1891 y Fg(\000)f Fe(v)625 1897 y Fc(2)642 1891 y Fg(g)p Fk(,)g(or)313 1973 y(4.)21 b(a)11 b(list)e Fd(\()p Fe(S)496 1979 y Fc(1)513 1973 y Fe(;)e(S)557 1979 y Fc(2)574 1973 y Fe(;)g(:)g(:)g(:)e(;)i(S)692 1979 y Fb(l)704 1973 y Fd(\))p Fk(,)k(where)g Fe(S)878 1979 y Fb(i)903 1973 y Fk(\()p Fe(i)g Fd(=)h Fk(1)p Fe(;)7 b(:)g(:)g(:)e(;)i(l)q Fk(\))j(is)g(a)g(set)h(of)f(v)o(alues,)h(or)313 2056 y(5.)21 b(!)p Fe(S)r Fk(,)12 b(which)e(is)g(a)g(complement)h(of)f (a)h(set)f(of)g(v)o(alues)h Fe(S)r Fk(.)324 2145 y(Let)e Fe(x)g Fk(be)g(an)g(enumerati)o(v)o(e)h(v)o(ariable)e(which)h(takes)f (4)h(v)o(alues.)15 b(The)9 b(follo)o(wing)e(are)i(e)o(xamples)262 2195 y(of)g(a)i(set)g(of)f(v)o(alues)g(for)g Fe(x)p Fk(.)324 2285 y Fg(\017)20 b Fk(1)324 2367 y Fg(\017)g(\000)324 2449 y(\017)g(f)p Fk(2)9 b Fg(\000)h Fk(3)p Fg(g)967 2574 y Fk(4)p eop %%Page: 5 5 5 4 bop 324 307 a Fg(\017)20 b Fd(\()p Fk(0)p Fe(;)7 b Fg(f)p Fk(2)h Fg(\000)i Fk(3)p Fg(g)p Fd(\))324 390 y Fg(\017)20 b Fk(!)p Fg(f)p Fk(2)9 b Fg(\000)g Fk(3)p Fg(g)324 482 y Fk(If)g(a)i(v)o(ariable)e(is)h(a)g(symbolic)f(v)o (ariable,)h(the)g(range)g(construct)f(in)g(the)g(abo)o(v)o(e)i(cannot)f (be)g(used)262 531 y(since)g Fg(f)p Fk(red-green)p Fg(g)p Fk(,)g(for)g(e)o(xample,)i(does)f(not)e(make)i(sense.)324 581 y(Let)f(us)h(consider)f(the)g(follo)o(wing)e(e)o(xample.)262 672 y Fh(.mv)24 b(x,y)h(4)262 722 y(.table)f(x)h(->)f(y)262 772 y(!2)g({1-3})262 822 y(-)g(0)262 872 y(2)g(\(0,3\))324 963 y Fk(The)13 b(relation)e(speci\256ed)i(in)f(this)f(table)h(is:)18 b Fd([\()p Fk(0)p Fe(;)7 b Fk(1)p Fe(;)g Fk(3)p Fd(\))i Fg(\002)h Fd(\()p Fk(1)p Fe(;)d Fk(2)p Fe(;)g Fk(3)p Fd(\)])i Fg([)h Fd([\()p Fk(0)p Fe(;)d Fk(1)p Fe(;)g Fk(2)p Fe(;)g Fk(3)p Fd(\))g Fg(\002)k Fd(\()p Fk(0)p Fd(\)])f Fg([)262 1013 y Fd([\()p Fk(2)p Fd(\))e Fg(\002)i Fd(\()p Fk(0)p Fe(;)d Fk(3)p Fd(\)])p Fk(.)262 1123 y Fa(1.3.1)41 b(=)10 b(Construct)262 1201 y Fk(One)j(can)h(also)f(use)h (the)f Ff(=)g(construct)g Fk(in)g(table)g(speci\256cations.)24 b(Assume)14 b(that)e(in)h(the)g(column)262 1251 y(corresponding)8 b(to)i(v)o(ariable)g Fe(y)q Fk(,)i(we)e(ha)o(v)o(e)i Fd(=)g Fe(x)e Fk(as)h(in)e(the)h(follo)o(wing)e(e)o(xample.)262 1342 y Fh(.table)24 b(x)h(->)f(y)262 1392 y(-)g(=x)324 1483 y Fk(The)11 b(interpretation)d(of)h(this)h(construct)f(is)h(that)g (the)g(v)o(alue)g(of)g Fe(y)i Fk(should)d(be)h(equal)g(to)g Fe(x)p Fk(.)15 b(This)262 1533 y(enables)10 b(us)h(to)e(describe)i(a)g (multi-v)o(alued)d(multiple)o(xor)h(compactly)h(\(see)h(belo)o(w\).)262 1616 y Fh(.mv)24 b(select)g(2)262 1666 y(.mv)g(data0,data1,output)f (256)262 1716 y(.table)h(select)g(data0)h(data1)f(->)h(output)262 1766 y(0)f(-)h(-)g(=data0)262 1816 y(1)f(-)h(-)g(=data1)262 1899 y Fk(Note)11 b(that)h(two)f(v)o(ariables)h(related)g(with)f(the)h (=)h(construct)f(should)e(be)j(of)f(the)g(same)h(type.)21 b(An)o(y)262 1948 y(v)o(ariable)10 b(referred)g(to)g(with)f(the)h(=)h (construct)f(must)g(be)g(an)h(input)e(of)h(the)g(table.)262 2059 y Fa(1.3.2)41 b(Default)10 b(Output)262 2137 y Fk(It)e(is)h (sometimes)h(con)n(v)o(enient)g(to)e(de\256ne)i(a)g(default)e(output)g (for)h(the)g(input)f(patterns)h(not)f(speci\256ed)262 2187 y(in)g(a)h(gi)o(v)o(en)g(relation.)14 b(The)9 b Fh(.default)g Fk(construct)f(is)h(used)g(for)f(this)g(purpose.)15 b(In)8 b(the)h(follo)o(wing)262 2236 y(e)o(xample,)i(no)e(relation)g (is)g(speci\256ed)i(for)e(the)g(case)j(where)e(either)f Fe(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 2286 y(a)f(default)f(statement)h(in)f(the)h(table,)g(output)e(00)h(is)h (related)g(for)f(those)h(unspeci\256ed)g(input)e(patterns.)262 2336 y(Therefore,)14 b(the)f(relation)f(of)h(this)f(table)g(is:)20 b Fd([\()p Fk(1)p Fd(\))10 b Fg(\002)h Fd(\()p Fk(1)p Fd(\))g Fg(\002)g Fd(\()p Fk(1)p Fd(\))g Fg(\002)g Fd(\()p Fk(1)p Fd(\)])f Fg([)h Fd([\()p Fk(0)p Fd(\))f Fg(\002)h Fd(\()p Fk(0)p Fd(\))g Fg(\002)g Fd(\()p Fk(0)p Fd(\))f Fg(\002)262 2386 y Fd(\()p Fk(0)p Fd(\)])f Fg([)g Fd([\()p Fk(0)p Fd(\))g Fg(\002)h Fd(\()p Fk(1)p Fd(\))g Fg(\002)g Fd(\()p Fk(0)p Fd(\))g Fg(\002)g Fd(\()p Fk(0)p Fd(\)])f Fg([)g Fd([\()p Fk(1)p Fd(\))h Fg(\002)g Fd(\()p Fk(0)p Fd(\))f Fg(\002)h Fd(\()p Fk(0)p Fd(\))g Fg(\002)g Fd(\()p Fk(0)p Fd(\)])p Fk(.)18 b(Each)12 b(table)f(can)h(ha)o(v)o(e)g(at)f (most)262 2436 y(one)f Fh(.default)f Fk(declaration.)967 2574 y(5)p eop %%Page: 6 6 6 5 bop 262 307 a Fh(.mv)24 b(x1,x2,y1,y2)g(2)262 357 y(.table)g(x1)h(x2)f(->)h(y1)g(y2)262 407 y(.default)f(0)g(0)262 457 y(1)g(1)h(1)g(1)324 548 y Fk(The)8 b Fh(.default)g Fk(construct)f(can)h(be)g(used)g(e)o(v)o(en)h(for)e(tables)h(without)e (inputs.)13 b(Ho)o(we)o(v)o(er)n(,)d(one)262 598 y(has)i(to)g(be)g (careful)g(about)g(the)g(semantics.)21 b(There)13 b(are)g(two)e (possible)g(cases.)23 b(One)12 b(case)i(is)d(that)262 648 y(a)g(table)f(has)h(a)g(default)f(declaration,)h(b)o(ut)f(has)h(no) f(relation)g(speci\256ed,)h(where)h(the)e(interpretation)262 697 y(of)i(the)g(table)h(is)f(that)g(it)g(always)g(takes)h(the)f (default.)21 b(The)14 b(other)e(case)i(is)e(that)g(a)h(table)g(has)g (both)262 747 y(a)f(default)g(declaration)g(and)g(a)h(non-null)e (relation)g(speci\256ed,)j(then)e(the)g(default)g(can)h(be)g(simply)262 797 y(ignored.)262 916 y Fi(1.4)50 b(Latches)12 b(and)g(Reset)g(T)-5 b(ables)262 994 y Fk(A)10 b(latch)g(is)g(a)h(storage)g(element)f(which) g(updates)h(its)e(stored)h(v)o(alue)h(at)f(e)o(v)o(ery)h(clock)g(tick.) k(A)10 b(latch)262 1043 y(has)h(an)g(input)f(and)h(an)g(output.)16 b(At)11 b(each)h(clock)f(tick)f(the)h(latch)g(output)e(is)i(set)g(to)g (the)f(latch)h(input)262 1093 y(v)o(alue)g(before)g(the)g(tick,)g(and)h (keep)f(the)g(v)o(alue)g(till)f(the)h(ne)o(xt)g(clock)h(tick.)17 b(Ev)o(ery)12 b(latch)f(has)h(to)e(be)262 1143 y(initialized)g (although)h(the)h(latch)g(is)g(allo)o(wed)g(to)g(ha)o(v)o(e)i(more)e (than)g(one)h(initial)d(v)o(alue,)j(in)f(which)262 1193 y(case)h(the)f(latch)g(takes)g(an)g(initial)e(v)o(alue)i (nondeterministically)e(from)h(the)h(speci\256ed)h(v)o(alues.)21 b(A)262 1243 y(latch)14 b(can)g(be)h(seen)g(as)g(a)g(multi-v)o(alued)d (\257ip-\257op)h(with)g(possibly)g(multiple)g(initial)f(states.)27 b(In)262 1293 y(BLIF-MV)-5 b(,)9 b(there)i(is)f(an)g(implicit)e (assumption)i(that)f(the)h(whole)g(system)g(is)g(clocked)g(by)g(a)g (single)262 1342 y(global)f(clock)h(although)f(the)h(clock)g(is)g(ne)o (v)o(er)h(declared)g(in)f(BLIF-MV)g(declarations.)324 1392 y(A)g(latch)g(is)g(declared)h(as)g(follo)o(ws.)262 1483 y Fh(.latch)24 b()g()324 1575 y Ff(latc)o(h)11 b(input)f Fk(and)h Ff(latc)o(h)g(output)f Fk(are)i(strings,)f(gi)o(ving)f(the)h(name)i(of)e(the)g(latch)g(input)f (and)i(the)262 1625 y(latch)h(output.)24 b(The)14 b(two)e(v)o(ariables) i(should)f(be)g(of)h(the)f(same)i(type.)25 b(A)14 b(latch)g(must)f(ha)o (v)o(e)i(one)262 1674 y(reset)d(table,)h(which)f(is)h(used)f(to)g (initialize)f(the)h(latch)g(output)f(at)h(the)g(be)o(ginning.)21 b(A)12 b(reset)h(table)262 1724 y(is)e(a)h(single)f(output)f(table)i (whose)g(only)e(output)g(is)i(the)f(output)f(of)i(a)g(latch.)19 b(Notice)12 b(that)f(we)h(use)262 1774 y Fh(.reset)c Fk(instead)h(of)g Fh(.table)g Fk(for)g(reset)g(tables.)15 b(If)9 b(a)h(latch)f(is)g(reset)g(to)g(a)h(constant)e(v)o(alue,)i(then) 262 1824 y(the)f(latch)h(table)g(has)g(no)g(input.)j(The)e(follo)o (wing)c(e)o(xample)k(is)f(for)g(the)f(latch)h Ff(latc)o(h)p 1459 1824 13 2 v 14 w(output)f Fk(whose)262 1874 y(reset)h(state)h(is)f (0.)262 1965 y Fh(.reset)24 b(latch_output)262 2015 y(0)324 2106 y Fk(One)15 b(can)g(specify)g(multiple)e(initial)g(states)i(by)f (specifying)g(more)h(than)f(one)h(v)o(alue)g(in)f(the)262 2156 y(latch)9 b(output.)14 b(Adding)8 b(one)i(more)h(line)e(to)g(the)h (abo)o(v)o(e)h(e)o(xample,)g(the)f(latch)g(has)g(no)o(w)g(two)f (initial)262 2206 y(states.)262 2297 y Fh(.reset)24 b(latch_output)262 2347 y(0)262 2397 y(1)967 2574 y Fk(6)p eop %%Page: 7 7 7 6 bop 324 307 a Fk(This)13 b(is)g(one)h(way)f(to)g(introduce)f (non-determinism)g(in)h(system)g(descriptions.)24 b(Also,)14 b(one)262 357 y(could)d(create)i(comple)o(x)g(reset)g(circuitry)e (sensiti)o(v)o(e)g(to)h(other)g(v)o(ariables)g(by)f(introducing)f (inputs)262 407 y(to)h(the)h(latch)f(table.)20 b(The)13 b(follo)o(wing)c Fh(.reset)j Fk(statement)g(initializes)e(the)i(latch)g (to)f(1)h(if)f Fe(x)h Fk(is)g(0)262 457 y(and)e(to)g(0)g(if)f Fe(x)h Fk(is)h(1.)262 548 y Fh(.reset)24 b(x)h(latch_output)262 598 y(0)f(1)262 648 y(1)g(0)262 766 y Fi(1.5)50 b(Subcir)o(cuits)262 844 y Fk(In)16 b(a)h(model,)h(another)e(model)g(can)h(be)g (instantiated)e(as)i(a)g(subcircuit)f(using)f(the)h Fh(.subckt)262 894 y Fk(construct.)262 985 y Fh(.subckt)24 b()g ()f()324 1077 y Fk(This)11 b(construct)f(instantiates)h(a)g(reference)i(model)e Ff(model-name)g Fk(as)h(an)f(instance)g Ff(instance-)262 1127 y(name)i Fk(in)f(the)h(current)g(model.)23 b Ff (formal-actual-list)9 b Fk(speci\256es)15 b(the)d(association)h (between)h(each)262 1176 y(formal)i(v)o(ariable)g(in)g Ff(model-name)g Fk(and)g(its)g(corresponding)f(actual)i(v)o(ariable)f (in)g(the)g(current)262 1226 y(model.)26 b(F)o(ormal)14 b(v)o(ariables)g(are)g(declared)h(in)e(the)h(reference)h(model,)g (while)f(actual)g(v)o(ariables)262 1276 y(are)e(v)o(ariables)g (declared)g(in)f(the)h(current)f(model.)20 b Ff(formal-actual-li)o(st)9 b Fk(is)i(a)i(list)d(of)i(assignments)262 1326 y(separated)f(by)f(a)g (white)g(space.)17 b(The)10 b(declaration)g(of)g Ff(formal-actual-li)o (st)d Fk(is)k(of)f(form:)262 1417 y Fh(formal-1)24 b(=)g(actual-1)h (formal-2)f(=)h(actual-2)f(...)g(formal-n)h(=)f(actual-n)324 1508 y Fk(The)11 b(order)f(of)g(formal)g(v)o(ariables)g(is)g (unimportant.)262 1627 y Fi(1.6)50 b(Miscellaneous)12 b(F)o(eatur)o(es)262 1705 y Fa(1.6.1)41 b(Comments)262 1783 y Fk(An)o(y)10 b(line)f(starting)g(from)h(#)h(is)f(a)g(comment.)16 b(It)10 b(is)g(ignored)f(by)h(the)g(parser)n(.)262 1893 y Fa(1.6.2)41 b(Including)10 b(Files)262 1971 y Fk(The)j Fh(.include)g Fk(construct)f(can)i(be)f(used)h(to)e(include)h(another)f (\256le)i(from)e(a)i(\256le)f(being)g(read.)262 2021 y(The)d(syntax)g(is)g Fh(.include)24 b(fileName)p Fk(.)262 2140 y Fi(1.7)50 b(Old)11 b(Syntax)262 2218 y Fk(Pre)o(viously)m(,)e (the)g(three)h(constructs)f Fh(.table)p Fk(,)g Fh(.default)p Fk(,)h Fh(.reset)f Fk(were)h(called)g Fh(.names)p Fk(,)262 2268 y Fh(.def)p Fk(,)17 b Fh(.r)f Fk(respecti)o(v)o(ely)m(.)33 b(The)17 b Fh(read)p 877 2268 13 2 v 15 w(blif)p 992 2268 V 14 w(mv)f Fk(command)h(in)f(VIS)g(supports)f(these)i(old)262 2317 y(constructs)9 b(as)i(well.)967 2574 y(7)p eop %%Page: 8 8 8 7 bop 262 307 a Fj(2)58 b(Semantics)262 400 y Fk(In)11 b(this)g(section)h(we)h(describe)f(the)g(semantics)h(of)f(BLIF-MV)-5 b(.)11 b(The)i(semantics)g(is)f(de\256ned)g(o)o(v)o(er)262 450 y(\257attened)f(networks)f(where)h(all)g(the)g Fh(.subckt)f Fk(constructs)h(are)h(substituted)d(recursi)o(v)o(ely)i(until)262 500 y(leaf)16 b(models.)34 b(Leaf)18 b(models)e(are)i(models)e(without) e(an)o(y)j Fh(.subckt)f Fk(declarations.)34 b(In)16 b(the)262 549 y(follo)o(wing,)8 b(a)i(\257attened)h(network)e(is)h(called)g(a)h Ff(system)p Fk(.)324 599 y(At)g(e)o(v)o(ery)g(time)g(point,)f(the)h (system)h(is)f(in)f(some)i(state,)g(where)g(each)g(latch)f(has)h(a)f(v) o(alue.)18 b(An)262 649 y(initial)9 b(state)k(of)e(the)h(system)g(is)g (a)h(state)f(where)g(e)o(v)o(ery)h(latch)e(is)h(set)g(to)g(an)g (initial)e(state)i(declared)262 699 y(using)f(the)i Fh(.reset)f Fk(constructs.)22 b(Notice)13 b(that)f(the)g(system)h(can)h(ha)o(v)o(e) g(more)f(than)f(one)h(initial)262 749 y(state)f(in)f(general.)20 b(At)11 b(e)o(v)o(ery)i(clock)f(tick,)g(all)f(the)h(latches)g(update)g (their)f(v)o(alues.)20 b(These)13 b(v)o(alues)262 798 y(then)f(propagate)h(through)e(tables)j(until)d(all)i(the)g(wires)g(ha) o(v)o(e)h(a)g(consistent)e(set)h(of)g(v)o(alues.)24 b(If)13 b(a)262 848 y(latch)f(is)g(encountered)g(during)e(the)i(propagation,)g (i.e.)h(an)f(output)f(of)h(a)g(table)g(is)g(an)h(input)e(of)g(an)262 898 y(latch,)f(the)g(propagation)f(process)i(is)f(stopped.)15 b(Note)10 b(that)g(because)i(of)e(nondeterminism,)g(gi)o(v)o(en)262 948 y(a)g(single)g(state,)h(there)f(may)h(be)g(se)o(v)o(eral)g (consistent)e(sets)i(of)f(v)o(alues.)324 998 y(The)18 b(semantics)g(can)f(be)h(seen)g(as)g(a)g(simple)f(e)o(xtension)f(of)h (the)g(standard)g(semantics)h(of)262 1048 y(synchronous)10 b(single-clocked)g(digital)g(circuits.)18 b(In)11 b(fact,)h(if)f(e)o(v) o(ery)h(table)f(is)g(deterministic)g(and)262 1097 y(e)o(v)o(ery)k (latch)f(has)h(a)g(single)f(initial)f(state,)j(the)e(two)g(semantics)h (are)h(e)o(xactly)e(equal.)29 b(The)15 b(only)262 1147 y(dif)o(ferences)8 b(are)i(in)d(the)i(interpretation)d(of)i (nondeterministic)e(tables)j(and)f(latches)h(with)e(multiple)262 1197 y(initial)h(states)i(as)h(described)g(in)e(the)i(abo)o(v)o(e.)262 1337 y Fj(3)58 b(The)14 b(VIS-v)h(Subset)g(of)g(BLIF-MV)262 1430 y Fk(VIS-v)f(can)h(only)f(work)g(on)g(a)i(strict)e(subset)g(of)h (BLIF-MV)f(although)f(an)o(y)j(synthesis-related)262 1480 y(commands)10 b(like)f Fh(read)p 625 1480 13 2 v 14 w(blif)g Fk(and)h Fh(write)p 943 1480 V 15 w(blif)p Fk(,)f(are)i(applicable)e(to)g(the)g(full-set)g(of)g(BLIF-)262 1529 y(MV)-5 b(.)10 b(If)g(the)g(user)g(generates)h(BLIF-MV)f(\256les)g (using)g(VL2MV)g(follo)o(wing)d(a)k(certain)f(restriction)262 1579 y(\(See)15 b(the)f(VIS)g(users')h(manual)f(for)g(details\),)h(the) f(\256les)h(are)g(guaranteed)f(to)g(be)h(in)e(the)h(subset.)262 1629 y(Ho)o(we)o(v)o(er)n(,)g(if)d(BLIF-MV)h(\256les)h(are)g(generated) g(manually)m(,)g(the)f(user)h(must)f(make)h(sure)f(that)g(the)262 1679 y(\256les)f(are)g(in)f(the)h(VIS-v)f(subset.)17 b(Otherwise,)11 b Fh(init)p 1045 1679 V 14 w(verify)f Fk(simply)g(fails,)h(thereby)f(making)262 1729 y(it)f(impossible)g(to)h (perform)g(the)g(v)o(eri\256cation.)324 1779 y(The)h(restriction)d(we)j (pose)g(is)f(as)h(follo)o(ws.)324 1862 y Fg(\017)20 b Fk(The)15 b(only)d(allo)o(wable)h(nondeterministic)f(tables)h(are)i Ff(pseudo-input)d(tables)p Fk(,)i(which)f(are)365 1911 y(no-input,)7 b(single-output)e(tables)j(which)f(generate)i(more)f (than)g(one)g(output)e(nondetermin-)365 1961 y(istically)m(.)262 2044 y(Note)k(that)h(one)g(can)h(always)f(transform)g(an)o(y)g(BLIF-MV) g(\256le)g(to)g(its)g(equi)o(v)o(alent)f(BLIF-MV)h(\256le)262 2094 y(in)c(the)h(VIS-v)g(subset)g(by)g(determinizing)f(all)h (intermediate)g(nondeterministic)f(tables)h(by)g(adding)262 2144 y(pseudo-inputs.)967 2574 y(8)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF