Abstract
There are several approaches of using automated theorem provers and assistants in hardware verification. It has been shown, that hardware behavior can be modelled and verified using theorem proving tools. But the task of generating a proof remains difficult and often needs a big amount of interaction. Therefore, the methods of our hardware verification system VERENA are based on term rewriting. It is shown how we use the expressive power of type theory to model circuit behavior. The crucial point in implementing a term rewriting system is to guarantee that the term rewriting rules used have specific properties like correctness, confluence, completeness, etc. It is demonstrated how we use the HOL prove assistant to prove the correctness of term rewriting rules.
Chapter PDF
Similar content being viewed by others
Keywords
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
P. Amblard, P. Caspi, N. Halbwachs: “Use of time functions to describe and explain circuit behavior,” IEE Proceedings, Vol. 133, Pt.E, No.5, 1986, pp. 271–275.
R. Boyer, J. Moore: “A Computational Logic,” Academic Press, New York, 1979.
D.Borrione, J.-L.Paillet, L.Pierre: “Formal Verification of CASCADE descriptions,” The Fusion of Hardware Design and Verification, G.J.Milne (ed.), Elsevier Science Publishers B.V. (North-Holland), 1988, pp. 185–210
A.Bronstein, C.L.Talcott: “Formal Verification of Pipelines based on String-Functional Semantics,” Proc. of the IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, L.J.M.Claesen (ed.), Houlthalen Belgium, Nov., 1989, pp. 347–364
M.Browne, E.Clarke, D.Dill, B.Mishra: “Automatic Verification of Sequential Circuits using Temporal Logic,” CHDLs and their Applications, C.J.Koomen and T.Moto-oka (eds.), North-Holland, 1985, S.98–113
A.Eveking: “Formal Verification of Synchronous Systems,” Formal Aspects of VLSI Design, G.J.Milne and P.A.Subrahmanyam (eds.), Elsevier Science Publishers B.V. (North-Holland), 1986, pp. 137–151
M. Fujita, S. Kono, H. Tanaka, T. Moto-oka: “Aid to hierarchical and structural logic design using temporal logic and Prolog,” IEE PROCEEDINGS, Vol. 133, Pt.E, No.5, Sept. 1986, S 283–294.
M.Gordon: “HOL — A Machine Oriented Formulation of Higher Order Logic,” University of Cambridge, Computer Laboratory, Technical Report no. 68, 1985
W.Grass: “VERENA — A CAD tool for designing guaranteed correct logic circuits,” Proceedings of the 2nd ABAKUS workshop, Innsbruck-Igls, Austria, Sept.1988, pp. 41–56
F.K.Hanna, N.Daeche: “Specification and Verification using Higher-Order Logic,” Proc. CHDL, Kommen and Moto-oka (eds.), North Holland, 1985
M.Gordon: “The HOL Reference Manual,” “The HOL Description,” and “The HOL Tutorial,” Documentation of the HOL88 System, Cambridge, 1988
T.Larsson: “Hardware Verification based on Algebraic Manipulation and Partial Evolution,” The Fusion of Hardware Design and Verification, G.J.Milne (ed.), Elsevier Science Publishers B.V. (North-Holland), 1988, pp. 231–252
M.Mutz: “Formal verification of sequential circuits with VERENA: a case study,” Proc. of the Advanced Research Workshop on Correct Hardware Design Methodologies, Turin, Italy, June 1991, P.Prinetto and P.Camurati (eds.), Elsevier Science Publishers B.V. (North-Holland)
J.-L.Paillet: “Descriptions and Specifications of Digital Devices,” From HDL to Guaranteed Correct Designs, IFIP, pp. 21–42
L.Pierre: “The Formal Proof of the Min-Max sequential benchmark described in CASCADE using the Boyer-Moore Theorem Prover,” Proc. of the IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, L.J.M.Claesen (ed.), Houlthalen Belgium, Nov., 1989, pp. 129–148
S.R.Ramirez Chavez: “Formal proof of the cascading properties of a parallel sorting circuit,” Proc. of the IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, L.J.M.Claesen (ed.), Houlthalen Belgium, Nov. 1989, 338–346
B. Zeigler: “Theory of Modelling and Simulation”, John Wiley & Sons, New York, Chichester, Brisbane, Toronto, 1976.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mutz, M. (1992). Using the HOL prove assistant for proving the correctness of term rewriting rules reducing terms of sequential behavior. In: Larsen, K.G., Skou, A. (eds) Computer Aided Verification. CAV 1991. Lecture Notes in Computer Science, vol 575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55179-4_27
Download citation
DOI: https://doi.org/10.1007/3-540-55179-4_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55179-9
Online ISBN: 978-3-540-46763-2
eBook Packages: Springer Book Archive