Hardware verification using monadic second-order logic

  • David A. Basin
  • Nils Klarlund
Session 2: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


We show how the second-order monadic theory of strings can be used to specify hardware components and their behavior. This logic admits a decision procedure and counter-model generator based on canonical automata for formulas. We have used a system implementing these concepts to verify, or find errors in, a number of circuits proposed in the literature. The techniques we use make it easier to identify regularity in circuits, including those that are parameterized or have parameterized behavioral specifications. Our proofs are semantic and do not require lemmas or induction as would be needed when employing a conventional theory of strings as a recursive data type.


Decision Procedure Regular Language Arithmetic Logic Unit Combinational Logic Circuit Parameterized Hardware 
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.


  1. 1.
    David Basin and Peter DelVecchio. Verification of combinational logic in Nuprl. In Hardware Specification, Verification ana Synthesis: Mathematical Aspects, Ithaca, New York, 1989. Springer-Verlag.Google Scholar
  2. 2.
    Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 43–67. Elsevier Science Publishers B. V. (North-Holland), 1987.Google Scholar
  3. 3.
    Albert John Camilleri. Executing Behavioural Definitions in Higher Order Logic. PhD thesis, University of Cambridge, 1988.Google Scholar
  4. 4.
    Cyrluk D., S. Rajan, N. Shankar, and M.K. Srivas. Effective theorem proving for hardware verification. In Second International Conference On Theorem Proving In Circuit Deisgn: Theory, Practice and Experience, Bad Herrenalb, Germany, September 1994.Google Scholar
  5. 5.
    1994 Francisco Cantu, Edinburgh DAI. Personal Communication.Google Scholar
  6. 6.
    Michael J. 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
  7. 7.
    A. Gupta and Allen L. Fisher. Parametric circuit representation using inductive boolean functions. In C. Courcoubetis, editor, Computer Aided Verification, CAV' 93, LNCS 697, pages 15–26. Springer Verlag, 1993.Google Scholar
  8. 8.
    A. Gupta and Allen L. Fisher. Tradeoffs in canonical sequential function representations. In Proceedings of the IEEE International Conference on Computer Design, October 1994.Google Scholar
  9. 9.
    F.K. Hanna and N. Daeche. Specification and verification using higher-order logic: a case study. In G.J. Milne and P.A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 179–213. Elsevier Science Publishers B.V., 1986.Google Scholar
  10. 10.
    J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. Technical Report RS-95-21, BRICS, Department of Computer Science, University of Aarhus, 1995.Google Scholar
  11. 11.
    Hardi Hungar. Combining model checking and theorem proving to verify parallel processes. In C. Courcoubetis, editor, Computer Aided Verification, CAV' 93, LNCS 697, pages 154–165. Springer Verlag, 1993.Google Scholar
  12. 12.
    Warren Hunt. Microprocessor design verification. Journal of Automated Reasoning, 5(4):429–460, 1989.Google Scholar
  13. 13.
    Warren J. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 89–129. Elsevier Science Publishers B. V. (North-Holland), 1987.Google Scholar
  14. 14.
    M. Morris Mano. Digital logic and computer design. Prentice-Hall, Inc., 1979.Google Scholar
  15. 15.
    T. F. Melham. Using recursive types of reasoning about hardware in higher order logic. In International Working Conference on The fusion of Hardware Design and Verification, pages 26–49, July 1988.Google Scholar
  16. 16.
    J.-K. Rho. and F. Somenzi. Automatic generation of network invariants for the verification of iterative sequential networks. In C. Courcoubetis, editor, Computer Aided Verification, CAV' 93, LNCS 697, pages 123–137. Springer Verlag, 1993.Google Scholar
  17. 17.
    W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. MIT Press/Elsevier, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • David A. Basin
    • 1
  • Nils Klarlund
    • 2
    • 3
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany
  2. 2.Department of Computer Science University of AarhusBRICSAarhus CDenmark
  3. 3.Basic Research in Computer ScienceCentre of the Danish National Research FoundationDenmark

Personalised recommendations