Formal verification of hardware correctness: introduction and survey of current research
- 1 July 1988
- journal article
- research article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in Computer
- Vol. 21 (7) , 8-19
- https://doi.org/10.1109/2.65
Abstract
Formal verification techniques are analyzed, focusing on two key points: suitable representation systems and mechanizable proofs. Different approaches to hardware verification are first examined, and formal verification and automated synthesis are compared to show how they cooperate in producing zero-defect designs. The different techniques are evaluated. Cross fertilization with software verification techniques is discussed.Keywords
This publication has 17 references indexed in Scilit:
- Automatic Verification of Sequential Circuits Using Temporal LogicIEEE Transactions on Computers, 1986
- Specification and verification of digital systems using higher-order predicate logicIEE Proceedings E Computers and Digital Techniques, 1986
- Verification of Register Transfer Level Parallel Control SequencesIEEE Transactions on Computers, 1985
- Verify: A program for proving correctness of digital hardware designsArtificial Intelligence, 1984
- Circal: A calculus for circuit descriptionIntegration, 1983
- Equivalence of the Arbiter, the Synchronizer, the Latch, and the Inertial DelayIEEE Transactions on Computers, 1983
- An Abstract Model of Behavior for Hardware DescriptionsIEEE Transactions on Computers, 1983
- Temporal logic based hardware description and its verification with PrologNew Generation Computing, 1983
- Hardware Specification with Temporal Logic: An ExampleIEEE Transactions on Computers, 1982
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967