B2M: A semantic based tool for BLIF hardware descriptions

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 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.