@InProceedings{	  basin.ea:b2m:2000,
  author	= {David Basin and Stefan Friedrich and Sebastian
		  M{\"o}dersheim},
  title		= {{B2M}: A {S}emantic {B}ased {T}ool for {BLIF} {H}ardware
		  {D}escriptions},
  editor	= {Warren A. Hunt and Steven D. Johnson},
  language	= {USenglish},
  booktitle	= {Formal Methods in Computer-Aided Design, Third
		  International Conference, FMCAD 2000},
  year		= 2000,
  series	= {Lecture Notes in Computer Science},
  volume	= 1954,
  pages		= {91--107},
  address	= {Austin, Tx, USA},
  month		= nov,
  publisher	= {Springer-Verlag},
  abstract	= {BLIF is a hardware description language designed for the
		  hierarchical description of sequential circuits. We give a
		  denotational semantics for BLIF-MV, a popular dialect of
		  BLIF, that interprets hardware descriptions in WS1S, the
		  weak monadic second-order logic of one successor. We show
		  how, using a decision procedure for WS1S, our semantics
		  provides a simple but effective basis for diverse kinds of
		  symbolic reasoning about circuit descriptions, including
		  simulation, equivalence testing, and the automatic
		  verification of general safety properties. We illustrate
		  these ideas with the B2M tool, which compiles circuit
		  descriptions down to WS1S formulae and analyzes them using
		  the MONA system.},
  keywords	= {formal methods, computer-aided design, systems design,
		  hardware design, design automation, systems verification,
		  formal specification, system design tools, model checking,
		  program analysis },
  ps		= {papers/2000/BFMfmcad2000.ps.gz},
  pdf		= {papers/2000/BFMfmcad2000.pdf}
}