Automatic Verification of Sequential Circuits Using Temporal Logic
- 1 December 1986
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-35 (12) , 1035-1044
- https://doi.org/10.1109/tc.1986.1676711
Abstract
Verifying the correctness of sequential circuits has been an important problem for a long time. But lack of any formal and efficient method of verification has prevented the creation of practical design aids for this purpose. Since all the known techniques of simulation and prototype testing are time consuming and not very reliable, there is an acute need for such tools. In this paper we describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, our system does not require any user assistance and is quite fast—experimental results show that state machines with several hundred states can be checked for correctness in a matter of seconds!Keywords
This publication has 8 references indexed in Scilit:
- A hardware semantics based on temporal intervalsPublished by Springer Nature ,2005
- Automatic verification of asynchronous circuits using temporal logicIEE Proceedings E Computers and Digital Techniques, 1986
- A Switch-Level Model and Simulator for MOS Digital SystemsIEEE Transactions on Computers, 1984
- Automatic verification of asynchronous circuitsPublished by Springer Nature ,1984
- Automatic verification of finite state concurrent system using temporal logic specificationsPublished by Association for Computing Machinery (ACM) ,1983
- Hardware Specification with Temporal Logic: An ExampleIEEE Transactions on Computers, 1982
- The temporal logic of branching timePublished by Association for Computing Machinery (ACM) ,1981
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980