Abstract
The verification of digital circuits at higher levels of abstraction still suffers from complex and unstructured proofs. In this paper, we present a class of circuits that can be used for the implementation of arbitrary processes without shared memory. These processes communicate with each other according to a handshake protocol. We have proven general theorems to automatically derive correctness theorems for composed handshake circuits. The contribution of this paper is therefore a new design style based on handshake circuits and a highly automated approach to verification at the system level based on functional abstraction.
This work has been partly financed by a german national grant, project Automated System Design, SFB No.358.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. Composing specifications. Technical Report 66, System Research Center, 1990.
S.M. Burns and A.J. Martin. A synthesis method for self-timed VLSI circuits. In Proceedings of the International Conference on Computer Design, 1987.
European Design and Test Conference. IEEE Computer Society Press, March 1994.
C.A.R. Hoare. An axiomatic approach to computer programming. Communications ACM, 12:576–580, 1969.
C.A.R. Hoare. Communicating sequential processes. Communications ACM, pages 666–677, 1978.
HOL User's Group Workshop, number 780 in Lecture Notes in Computer Sciences, Vancouver, Canada, August 1993. Springer Verlag.
F. Kröger. Temporal Logic of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1987.
A.J. Martin. Synthesis of asynchronous VLSI circuits. In J. Staunstrup, editor, Formal Methods for VLSI Design, 1990.
T.F. Melham. Abstraction mechanisms for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1988.
K. Schneider, R. Kumar, and Th. Kropf. The FAUST prover. In D. Kapur, editor, 11th Conference on Automated Deduction, number 607 in Lecture Notes in Computer Science, pages 766–770. Springer Verlag, Albany, New York,1992.
K. Schneider, R. Kumar, and Th. Kropf. Hardware verification with firstorder BDD's. In Conference on Computer Hardware Description Languages, 1993.
K. Schneider, R. Kumar, and Th. Kropf. Alternative proof procedures for finite-state machines in a higher-order environment. In International Workshop on Higher-Order Logic Theorem Proving and its Applications, Vancouver, Canada, 1993.
K. Schneider, T. Kropf, and R. Kumar. Control-path oriented verification of sequential generic circuits with control and data path. In [EDAC94].
W. Wong. Modelling bit vectors in HOL: the word library. In [HUG93].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schneider, K., Kumar, R., Kropf, T. (1994). Automating verification by functional abstraction at the system level. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_56
Download citation
DOI: https://doi.org/10.1007/3-540-58450-1_56
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58450-6
Online ISBN: 978-3-540-48803-3
eBook Packages: Springer Book Archive