@InProceedings{b2m,
  author = {Basin, David and Friedrich, Stefan and M{\"o}dersheim,
Sebastian},
  title = {{B2M}: A {S}emantic {B}ased {T}ool for {BLIF} {H}ardware
{D}escriptions},
  booktitle = {Formal Methods in Computer-Aided Design, Third
International Conference (FMCAD 2000)},
  pages = {91--107},
  year = 2000,
  volume = 1954,
  series = {Lecture Notes in Computer Science},
  address = {Austin, Texas, USA},
  month = {November},
  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.} }