Abstract
This paper presents a technique for formally verifying synchronous circuits modelled at the Register Transfer Level of abstraction. The circuit's behavior, specification, and hypotheses on its clock sequencing are modelled using a special kind of predicate calculus formulas, named transfer formulas. The proof process consists in applying two general rules of the predicate calculus in a specific order. The automated verification process uses an acyclic graph for representing each transfer formula; in this way, the application of the rules is similar to the manipulation of boolean functions represented by acyclic graphs.
Chapter PDF
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
F. Anceau, "The Architecture of Microprocessors", Addison-Wesley, 1986.
M. R. Barbacci, "A Comparison of Register Transfer Languages for Describing Computers and Digital Systems", IEEE Trans. on Comp., Vol. C-24, No. 2, February 1975.
H. G. Barrow, "Verify: A Program for Proving Correctness of Digital Hardware Designs", Artificial Intelligence, Vol. 24, 1984.
A. Bartsch, H. Eveking, H.-J. Faerber, M. Kelelatchew, J. Pinder, U. Schellin, "LOVERT-A Logic Verifier of Register-Transfer Level Description", Proceedings of the IMEC IFIP International Workshop on "Applied Formal Methods for Correct VLSI Design", November 1989.
R. E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation", IEEE Trans. on Comp., Vol. C-35, No. 8, August 1986.
A. Camilleri, M. Gordon, T. Melham, "Hardware Verification Using Higher Order Logic", in From HDL Descriptions to Guaranteed Correct Circuit Designs, ed. D. Borrione, North-Holland, 1987.
P. Camurati, P. Prinetto, "Formal Verification of Hardware Correctness: Introduction and Survey of Current Research", Computer, July 1988.
A. Cohn, "A Proof of Correctness of the VIPER Microprocessor: the First Level", in VLSI Specification, Verification, and Synthesis, eds. G. Birtwistle and P. A. Subrahmanyam, Kluwer Academic Publishers, 1988.
C. Iseli, "WORP: A Watch Oriented RISC Processor", B. Sc. Thesis, Laboratoire de Systèmes Logiques, EPFL, December 1987.
J. Joyce, G. Birtwistle, M. Gordon, "Proving a Computer Correct in Higher Order Logic", Technical Report No. 100, Computer Laboratory, University of Cambridge, December 1986.
J. C. Madre, F. Anceau, M. Currat, J. P. Billon, "Formal Verification in an Industrial Design Environment", to appear in ‘The international Journal on Computer Aided VLSI Design'.
Z. Manna, "Mathematical Theory of Computation", McGraw-Hill, 1974.
T. F. Melham, "Abstraction Mechanisms for Hardware Verification", in VLSI Specification, Verification, and Synthesis, eds. G. Birtwistle and P. A. Subrahmanyam, Kluwer Academic Publishers, 1988.
W. Stallings, "Tutorial: Reduced Instruction Set Computers", IEEE Computer Society Press, Order Number 713, 1986.
R. Vemuri, "A Formal Model for Register Transfer Level Structures and Its Applications in Verification and Synthesis", Proceedings of the IMEC IFIP International Workshop on "Applied Formal Methods for Correct VLSI Design", November 1989.
"VTI User's Guide", VLSI Technology, Inc, 1988.
A. Bronstein, C. L. Talcott, "Formal Verification of Pipelines Based on String-Functional Semantics", Proceedings of the IMEC IFIP International Workshop on "Applied Formal Methods for Correct VLSI Design", November 1989.
L. Pierre, "The Formal Proof of Sequential Circuits Described in CASCADE Using the Boyer-Moore Theorem Prover", Proceedings of the IMEC IFIP International Workshop on "Applied Formal Methods for Correct VLSI Design", November 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Langevin, M. (1991). Automated RTL verification based on predicate calculus. In: Clarke, E.M., Kurshan, R.P. (eds) Computer-Aided Verification. CAV 1990. Lecture Notes in Computer Science, vol 531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023725
Download citation
DOI: https://doi.org/10.1007/BFb0023725
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54477-7
Online ISBN: 978-3-540-38394-9
eBook Packages: Springer Book Archive