A methodology for hardware verification based on logic simulation
- 1 April 1991
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 38 (2) , 299-328
- https://doi.org/10.1145/103516.103519
Abstract
A logic simulator can prove the correctness of a digital circuit if it can be shown that only circuits fulfilling the system specification will produce a particular response to a sequence of simulation commands.This style of verification has advantages over the other proof methods in being readily automated and requiring less attention on the part of the user to the low-level details of the design. It has advantages over other approaches to simulation in providing more reliable results, often at a comparable cost. This paper presents the theoretical foundations of several related approaches to circuit verification based on logic simulation. These approaches exploit the three-valued modeling capability found in most logic simulators, where the third-value X indicates a signal with unknown digital value. Although the circuit verification problem is NP-hard as measured in the size of the circuit description, several techniques can reduce the simulation complexity to a manageable level for many practical circuits.Keywords
This publication has 13 references indexed in Scilit:
- An analysis of ternary simulation as a tool for race detection in digital MOS circuitsIntegration, 1986
- Automatic Verification of Sequential Circuits Using Temporal LogicIEEE Transactions on Computers, 1986
- Automatic verification of asynchronous circuits using temporal logicIEE Proceedings E Computers and Digital Techniques, 1986
- Verify: A program for proving correctness of digital hardware designsArtificial Intelligence, 1984
- A Switch-Level Model and Simulator for MOS Digital SystemsIEEE Transactions on Computers, 1984
- Circal: A calculus for circuit descriptionIntegration, 1983
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- A three-value computer design verification systemIBM Systems Journal, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967
- Representation of Events in Nerve Nets and Finite AutomataPublished by Walter de Gruyter GmbH ,1956