Automatic verification of sequential circuits using temporal logic

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

Research output: Contribution to journalArticle

Abstract

An automatic verification system for sequential circuits is described in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, the system does not require 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; in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. Two different techniques that have been implemented for automatically generating the state-transition graphs are discussed.

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

Fingerprint

Automatic Verification
Sequential circuits
Temporal logic
Temporal Logic
State Transition
Graph in graph theory
Propositional Logic
State Machine
Specifications
Correctness
Efficient Algorithms
Specification
Experimental Results

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Cite this

Browne, M. C., Clarke, E. M., Dill, D. L., & Mishra, B. (1986). Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12), 1035-1044.

Automatic verification of sequential circuits using temporal logic. / Browne, Michael C.; Clarke, Edmund M.; Dill, David L.; Mishra, Bhubaneswar.

In: IEEE Transactions on Computers, Vol. C-35, No. 12, 12.1986, p. 1035-1044.

Research output: Contribution to journalArticle

Browne, MC, Clarke, EM, Dill, DL & Mishra, B 1986, 'Automatic verification of sequential circuits using temporal logic', IEEE Transactions on Computers, vol. C-35, no. 12, pp. 1035-1044.
Browne, Michael C. ; Clarke, Edmund M. ; Dill, David L. ; Mishra, Bhubaneswar. / Automatic verification of sequential circuits using temporal logic. In: IEEE Transactions on Computers. 1986 ; Vol. C-35, No. 12. pp. 1035-1044.
@article{19c59c04e9da455da227f3cea3f7284e,
title = "Automatic verification of sequential circuits using temporal logic",
abstract = "An automatic verification system for sequential circuits is described in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, the system does not require 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; in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. Two different techniques that have been implemented for automatically generating the state-transition graphs are discussed.",
author = "Browne, {Michael C.} and Clarke, {Edmund M.} and Dill, {David L.} and Bhubaneswar Mishra",
year = "1986",
month = "12",
language = "English (US)",
volume = "C-35",
pages = "1035--1044",
journal = "IEEE Transactions on Computers",
issn = "0018-9340",
publisher = "IEEE Computer Society",
number = "12",

}

TY - JOUR

T1 - Automatic verification of sequential circuits using temporal logic

AU - Browne, Michael C.

AU - Clarke, Edmund M.

AU - Dill, David L.

AU - Mishra, Bhubaneswar

PY - 1986/12

Y1 - 1986/12

N2 - An automatic verification system for sequential circuits is described in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, the system does not require 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; in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. Two different techniques that have been implemented for automatically generating the state-transition graphs are discussed.

AB - An automatic verification system for sequential circuits is described in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, the system does not require 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; in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. Two different techniques that have been implemented for automatically generating the state-transition graphs are discussed.

UR - http://www.scopus.com/inward/record.url?scp=0022890039&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0022890039&partnerID=8YFLogxK

M3 - Article

VL - C-35

SP - 1035

EP - 1044

JO - IEEE Transactions on Computers

JF - IEEE Transactions on Computers

SN - 0018-9340

IS - 12

ER -