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.
