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

%!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 D<FEFEC0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0C0
C0C0C0C0C0C0FEFE07297C9E0C>91 D<FEFE060606060606060606060606060606060606
06060606060606060606060606060606060606FEFE0729809E0C>93
D E /Fe 12 122 df<60F0F06004047C830C>58 D<60F0F0701010101020204080040C7C
830C>I<0000038000000F0000003C000000F0000003C000000F0000003C000000F00000
03C000000F0000003C000000F0000000F00000003C0000000F00000003C0000000F00000
003C0000000F00000003C0000000F00000003C0000000F000000038019187D9520>I<E0
000000780000001E0000000780000001E0000000780000001E0000000780000001E00000
00780000001E00000007800000078000001E00000078000001E00000078000001E000000
78000001E00000078000001E00000078000000E000000019187D9520>62
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 df<FFFFFF80FFFFFF8019027D8A20>0 D<400020C000606000C0300180
1803000C0600060C0003180001B00000E00000E00001B000031800060C000C0600180300
3001806000C0C0006040002013147A9320>2 D<03C00FF01FF83FFC7FFE7FFEFFFFFFFF
FFFFFFFF7FFE7FFE3FFC1FF80FF003C010107E9115>15 D<400002C00006C00006C00006
C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006
C00006C00006C0000660000C60000C3000181C00700F01E003FF8000FE00171A7E981C>
91 D<003C00E001C0018003800380038003800380038003800380038003800380038003
80030007001C00F0001C0007000300038003800380038003800380038003800380038003
8003800380018001C000E0003C0E297D9E15>102 D<F0001C0007000300038003800380
0380038003800380038003800380038003800380018001C000E0003C00E001C001800380
038003800380038003800380038003800380038003800380030007001C00F0000E297D9E
15>I 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(<model-name>)262
490 y(.inputs)g(<input-list>)262 540 y(.outputs)g(<output-list>)262
590 y(<command>)262 639 y(...)262 689 y(<command>)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
(<variable-name-list>)f(<number-of-values>)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(<variable-name-list>)f(<number-of-values>)g(<value-list>)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(<in-1>)g(<in-2>)h(...)f(<in-n>)h(->)f(<out-1>)h(<out-2>...)e(<out-m>)
262 696 y(<relation>)262 745 y(...)262 795 y(<relation>)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(<latch-input>)g(<latch-output>)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(<model-name>)g
(<instance-name>)f(<formal-actual-list>)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