Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
- 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.
References
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.
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.
Albert John Camilleri. Executing Behavioural Definitions in Higher Order Logic. PhD thesis, University of Cambridge, 1988.
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.
1994 Francisco Cantu, Edinburgh DAI. Personal Communication.
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.
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.
A. Gupta and Allen L. Fisher. Tradeoffs in canonical sequential function representations. In Proceedings of the IEEE International Conference on Computer Design, October 1994.
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.
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.
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.
Warren Hunt. Microprocessor design verification. Journal of Automated Reasoning, 5(4):429–460, 1989.
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.
M. Morris Mano. Digital logic and computer design. Prentice-Hall, Inc., 1979.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D.A., Klarlund, N. (1995). Hardware verification using monadic second-order logic. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_38
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive