B2M: A Semantic Based Tool for BLIF Hardware Descriptions
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 e.ective basis for diverse kinds of symbolic reasoning about circuit descriptions, including simulation, equivalence testing, and the automatic veri.cation 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.
KeywordsDecision Procedure Safety Property Abstract Syntax Sequential Circuit Hardware Description Language
Unable to display preview. Download preview PDF.
- B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, 7 October 1985.Google Scholar
- A. Ayari and D. Basin. Bounded model construction for monadic second-order logics. In 12th International Conference on Computer-Aided Verification (CAV’00), number 1855 in Lecture Notes in Computer Science, pages 99–113, Chicago, USA, July 2000. Springer-Verlag.Google Scholar
- D. Basin and S. Friedrich. Combining WS1S and HOL. In D.M. Gabbay and M. de Rijke, editors, Frontiers of Combining Systems 2, pages 39–56. Research Studies Press/Wiley, 2000.Google Scholar
- M. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design. North-Holland, 1986.Google Scholar
- J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In TACAS’ 95, LNCS 1019, 1996.Google Scholar
- Y. Kukimoto. BLIF-MV. 1996. Availlable at http://www-cad.eecs.berkeley.edu/Respep/Research/vis/.
- A. Meyer. Weak monadic second-order theory of one successor is not elementaryrecursive. In LOGCOLLOQ: Logic Colloquium. LNM 453, Springer, 1975.Google Scholar
- F. Morawietz and T. Cornell. On the recognizibility of relations over a tree definable in a monadic second-order tree description language. Research Report SFB 340-Report 85, 1997.Google Scholar
- W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 4. MIT Press/ Elsevier, 1990.Google Scholar
- VIS Group. VIS user’s manual. Availlable at http://www-cad.eecs.berkeley.edu/Respep/Research/vis/.
- VIS Group. VIS: A system for Verification and Synthesis. In R. Alur and T. Henzinger, editors, Proceedings of CAV’ 96, LNCS 1102, pages 428–432. Springer, 1996.Google Scholar