ComputingComputer EngineeringComputer ScienceComputer ArchitectureFormal MethodsLogicFinite State Machine ModelingModel CheckingTemporal LogicVerificationFinite State Machine VerificationPropositional Temporal LogicState MachinesSystem VerificationTemporal Logic SpecificationTemporal Logic VerificationTemporal Verification
Verifying sequential circuits has long been a critical problem, yet the lack of formal, efficient methods and the time‑consuming, unreliable nature of simulation and prototype testing underscore the urgent need for practical verification tools. The paper presents an automatic verification system for sequential circuits that uses propositional temporal logic specifications. The system automatically verifies sequential circuits by evaluating specifications expressed in propositional temporal logic. Experimental results show the system can verify state machines with several hundred states in seconds without user assistance, outperforming most mechanical verification systems.
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!
6
The temporal logic of branching time
Mordechai Ben‐Ari, Zohar Manna, Amir Pnueli · 1981 · 216 citations · Full text