Abstract
This paper describes a mechanized approach to verifying that one concrete design is a refinement of another abstract design. A widely used notion of refinement is trace inclusion, which implies that each externally visible behavior of the concrete design can also be caused by the abstract design. In some cases this is too restrictive and the verification technique proposed here is based on a more liberal notion where information about the environment is exploited. A verification technique is presented for designs written in the design language Synchronized Transitions. The verification technique is supported by a prototype tool for mechanizing 1) the axiomatization of the design descriptions in the logic of an existing theorem prover, and 2) the generation of proof obligations. Based on the axiomatization of the design descriptions, the proof obligations can be discharged using the theorem prover.
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Martin Abadi and Leslie Lamport. The existence of refinement mappings. Technical Report 29, Digital Systems Research Center, 1988.
Randal E. Bryant. Can a simulator verify a circuit? In Formal Aspects of VLSI Design, pages 125–136. North-Holland, 1985.
Stephen J. Garland and John V. Guttag. A guide to LP, the Larch Prover. Technical Report 82, Digital Systems Research Center, 1991.
Mike Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal Aspects of VLSI Design, pages 153–177. North-Holland, 1985.
Bengt Jonsson. On decomposing and refining specifications of distributed systems. In Lecture Notes in Computer Science, 430, pages 361–385. Springer Verlag, 1990.
Jeffrey J. Joyce. Formal verification and implementation of a microprocessor. In Graham Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification and Synthesis, pages 129–157. Kluwer Academic Publishers, 1988.
Leslie Lamport. The temporal logic of actions. Technical Report 79, Digital Systems Research Center, 1991.
Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pages 137–151. ACM, 1987.
Thomas F. Melham. Abstraction mechanisms for hardware verification. In Graham Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification and Synthesis, pages 267–291. Kluwer Academic Publishers, 1988.
Niels Mellergaard. Mechanized Design Verification. PhD thesis, Department of Computer Science, Technical University of Denmark, 1994.
Jørgen Staunstrup. A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maxetti, N. (1995). Mechanized verification of refinement. In: Kumar, R., Kropf, T. (eds) Theorem Provers in Circuit Design. TPCD 1994. Lecture Notes in Computer Science, vol 901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59047-1_49
Download citation
DOI: https://doi.org/10.1007/3-540-59047-1_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59047-7
Online ISBN: 978-3-540-49177-4
eBook Packages: Springer Book Archive