Automatic Verification of Sequential Circuits Using Temporal Logic

摘要: Verifying the correctness of sequential circuits has been an important problem for a long time. But lack any formal and efficient method verification prevented creation practical design aids this purpose. Since all known techniques simulation prototype testing are time consuming not very reliable, there is acute need such tools. In paper we describe automatic system in which specifications expressed propositional temporal logic. contrast to most other mechanical systems, our does require user assistance quite fast—experimental results show that state machines with several hundred states can be checked matter seconds!