Automatic verification of sequential circuits using temporal logic

Michael C. Browne, Edmund M. Clarke, David L. Dill, Bud Mishra

Research output: Contribution to journalArticle

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! The verification system uses a simple and efficient algorithm, called a model checker. The algorithm works in two steps: in the first step, it builds a labeled state-transition graph; and in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. We discuss two different techniques that we have implemented for automatically generating the state-transition graphs: The first involves extracting the state graph directly from the circuit by exhaustive simulation. The second obtains the state graph by compilation from an HDL specification of the original circuit.

Original languageEnglish (US)
Pages (from-to)1035-1044
Number of pages10
JournalIEEE Transactions on Computers
VolumeC-35
Issue number12
DOIs
StatePublished - Dec 1986

    Fingerprint

Keywords

  • Asynchronous circuits
  • hardware verification
  • sequential circuit verification
  • temporal logic
  • temporal logic model checking

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computational Theory and Mathematics

Cite this