B2M: A Semantic Based Tool for BLIF Hardware Descriptions

David Basin, Stefan Friedrich, and Sebastian Mödersheim

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


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.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:37
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems