Abstract
Formal Hardware Verification has gained a lot of attention recently as a viable alternative to simulation. Several notable achievements have been reported, such as Hunt [4], Birtwistle et. al. [1]. In this document we describe one aspect of an ongoing project aimed at developing an integrated environment for hardware description, simulation, and verification. We report here on the current efforts toward developing tools for formal verification of hardware and how these tools interact with other parts of the IVW workstation being developed at General Electric Research and Development Center (GE CRD). This is of necessity a preliminary document, as our work in developing an environment for highly automatic verification of hardware is at an early stage.
Work partially supported by Contract F33615-85-C-1862, AFWAL, Wright-Patterson Air Force Base, Ohio.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Birtwistle, G., Joyce, J., Liblong, B., Melham, T., and Schediwy, R. (1985). Specification and VLSI design. Research Report No. 85/220/33, Dept. of Computer Science, University of Calgary, Calgary, Alberta, Canada.
Boyer, R. and Moore, J.S. (1985). Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Technical Report ICSCA-CMP-44, Institute for Computing Science, University of Texas at Austin.
Gordon, M. (1985). Why Higher-Order Logic is a good formalism for specifying and verifying hardware. Technical Report 77, Computer Laboratory, University of Cambridge, Cambridge, U.K.
Hunt, WA, Jr. (1985). FM8501: A Verified Microprocessor. Technical Report 47, Institute for Computing Science, Univ. of Texas at Austin.
Kapur, D. and Musser, D.R. (1984). Proof by Consistency. To appear in Artificial Intelligence.
Kapur, D. and Narendran, P. (1985). An Equational Approach to Predicate Calculus. In: Proceedings of IJCAI-85, Los Angeles.
Kapur, D., Sivakumar, G., and Zhang, H. (1986). RRL: A Rewrite Rule Laboratory. In: Proceedings of 8th Conference on Automated Deduction (CADE-86), Oxford, U.K.
Knuth, D.E. and Bendix, P.B. (1970). Simple Word Problems in Universal Algebras, in Computational Problems in Abstract Algebras (ed. J. Leech), Pergamon Press, 263–297.
Moszkowski, B. (1985). A Temporal Logic for Multilevel Reasoning about Hardware.IEEE Computer.
Musser, D.R. (1980). Proving Inductive Properties of Abstract Data Types. In: Proc. of 7th Principles of Programming Languages Conf., Las Vegas, Nevada.
Musser, D.R., and Cyrluk, DA. (1985). Affirm-85 Installation Guide and Reference Manual Update. GE Corporate R&D Center, Schenectady, NY 12345.
Musser, D.R., Narendran, P. and Premerlani, W. (1987). BIDS: A Method for Specifying and Verifying Bidirectional Hardware Devices. Appears elsewhere in this volume.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1988 Kluwer Academic Publishers, Boston
About this chapter
Cite this chapter
Narendran, P., Stillman, J. (1988). Hardware Verification in the Interactive VHDL Workstation. In: Birtwistle, G., Subrahmanyam, P.A. (eds) VLSI Specification, Verification and Synthesis. The Kluwer International Series in Engineering and Computer Science, vol 35. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-2007-4_7
Download citation
DOI: https://doi.org/10.1007/978-1-4613-2007-4_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-9197-8
Online ISBN: 978-1-4613-2007-4
eBook Packages: Springer Book Archive