Document Type
Conference Proceeding
Publication Date
5-1996
Abstract
Ascertaining correctness of digital hardware designs through simulation does not scale-up for large designs because of the sheer combinatorics of the problem. Formal verification of hardware designs holds promise because its computational complexity is of the order of number of different types of components (and not number of components in the design). This approach requires the specification of the behavior and the design in a formal language, and reason with them using a theorem prover. In this paper we attempt to develop a methodology for writing and using these specifications for some important classes of hardware circuits. We examine digital hardware verification in the HOL-90 environment. (HOL-90 is a proof checker written in Standard ML which assists in mechanically checking a formal proof of hardware correctness.) In particular, we analyze proofs for a variety of circuits, and develop proof strategies for combinational circuits and restricted sequential circuits. Overall, this approach makes the theorem proving task less tedious and provides guidance to the user in carrying out proofs.
Repository Citation
Eastham, R.,
& Thirunarayan, K.
(1996). Proof Strategies for Hardware Verification. Proceedings of the IEEE 1996 National Aerospace and Electronics Conference, 2, 451-458.
https://corescholar.libraries.wright.edu/knoesis/887
DOI
10.1109/NAECON.1996.517689
Included in
Bioinformatics Commons, Communication Technology and New Media Commons, Databases and Information Systems Commons, OS and Networks Commons, Science and Technology Studies Commons
Comments
Presented at the IEEE National Aerospace and Electronics Conference, Dayton, OH, May 20-23, 1996.
Posted with permission from IEEE.