Advertisement

B2M: A Semantic Based Tool for BLIF Hardware Descriptions

  • David Basin
  • Stefan Friedrich
  • Sebastian Mödersheim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

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

Keywords

Decision Procedure Safety Property Abstract Syntax Sequential Circuit Hardware Description Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, 7 October 1985.Google Scholar
  2. [2]
    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
  3. [3]
    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
  4. [4]
    D. Basin and N. Klarlund. Automata based symbolic reasoning in hardware verification. The Journal of Formal Methods in Systems Design, 13(3):255–288, 1998.CrossRefGoogle Scholar
  5. [5]
    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
  6. [6]
    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
  7. [7]
    Y. Kukimoto. BLIF-MV. 1996. Availlable at http://www-cad.eecs.berkeley.edu/Respep/Research/vis/.
  8. [8]
    A. Meyer. Weak monadic second-order theory of one successor is not elementaryrecursive. In LOGCOLLOQ: Logic Colloquium. LNM 453, Springer, 1975.Google Scholar
  9. [9]
    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
  10. [11]
    J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57–81, 1967.CrossRefMathSciNetGoogle Scholar
  11. [12]
    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
  12. [13]
    VIS Group. VIS user’s manual. Availlable at http://www-cad.eecs.berkeley.edu/Respep/Research/vis/.
  13. [14]
    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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • David Basin
    • 1
  • Stefan Friedrich
    • 1
  • Sebastian Mödersheim
    • 1
  1. 1.Institute for Computer Science, University of FreiburgGermany

Personalised recommendations