Automatic verification of sequential circuits using temporal logic

M. Browne, E. Clarke, D. Dill, Bhubaneswar Mishra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. The system works in two steps: first, it builds a labeled state graph; second, it uses an efficient algorithm called a Model Checker to determine the truth of a temporal formula with respect to the state graph. We generate the state graphs by two different techniques. The first extracts the state graph directly from the circuit by simulation. The second complies an HDL specification into a state graph. As examples we verify an asynchronous queue element using the first technique and a traffic light controller using the second.

Original languageEnglish (US)
Title of host publicationUnknown Host Publication Title
EditorsCees-Jan Koomen, Tohru Moto-Oka
PublisherNorth-Holland
Pages98-113
Number of pages16
ISBN (Print)0444878262
StatePublished - 1985

Fingerprint

Sequential circuits
Temporal logic
Specifications
Telecommunication traffic
Controllers
Networks (circuits)

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Browne, M., Clarke, E., Dill, D., & Mishra, B. (1985). Automatic verification of sequential circuits using temporal logic. In C-J. Koomen, & T. Moto-Oka (Eds.), Unknown Host Publication Title (pp. 98-113). North-Holland.

Automatic verification of sequential circuits using temporal logic. / Browne, M.; Clarke, E.; Dill, D.; Mishra, Bhubaneswar.

Unknown Host Publication Title. ed. / Cees-Jan Koomen; Tohru Moto-Oka. North-Holland, 1985. p. 98-113.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Browne, M, Clarke, E, Dill, D & Mishra, B 1985, Automatic verification of sequential circuits using temporal logic. in C-J Koomen & T Moto-Oka (eds), Unknown Host Publication Title. North-Holland, pp. 98-113.
Browne M, Clarke E, Dill D, Mishra B. Automatic verification of sequential circuits using temporal logic. In Koomen C-J, Moto-Oka T, editors, Unknown Host Publication Title. North-Holland. 1985. p. 98-113
Browne, M. ; Clarke, E. ; Dill, D. ; Mishra, Bhubaneswar. / Automatic verification of sequential circuits using temporal logic. Unknown Host Publication Title. editor / Cees-Jan Koomen ; Tohru Moto-Oka. North-Holland, 1985. pp. 98-113
@inproceedings{ea4f20ec93764b1386d097ae771129ab,
title = "Automatic verification of sequential circuits using temporal logic",
abstract = "We describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. The system works in two steps: first, it builds a labeled state graph; second, it uses an efficient algorithm called a Model Checker to determine the truth of a temporal formula with respect to the state graph. We generate the state graphs by two different techniques. The first extracts the state graph directly from the circuit by simulation. The second complies an HDL specification into a state graph. As examples we verify an asynchronous queue element using the first technique and a traffic light controller using the second.",
author = "M. Browne and E. Clarke and D. Dill and Bhubaneswar Mishra",
year = "1985",
language = "English (US)",
isbn = "0444878262",
pages = "98--113",
editor = "Cees-Jan Koomen and Tohru Moto-Oka",
booktitle = "Unknown Host Publication Title",
publisher = "North-Holland",

}

TY - GEN

T1 - Automatic verification of sequential circuits using temporal logic

AU - Browne, M.

AU - Clarke, E.

AU - Dill, D.

AU - Mishra, Bhubaneswar

PY - 1985

Y1 - 1985

N2 - We describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. The system works in two steps: first, it builds a labeled state graph; second, it uses an efficient algorithm called a Model Checker to determine the truth of a temporal formula with respect to the state graph. We generate the state graphs by two different techniques. The first extracts the state graph directly from the circuit by simulation. The second complies an HDL specification into a state graph. As examples we verify an asynchronous queue element using the first technique and a traffic light controller using the second.

AB - We describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. The system works in two steps: first, it builds a labeled state graph; second, it uses an efficient algorithm called a Model Checker to determine the truth of a temporal formula with respect to the state graph. We generate the state graphs by two different techniques. The first extracts the state graph directly from the circuit by simulation. The second complies an HDL specification into a state graph. As examples we verify an asynchronous queue element using the first technique and a traffic light controller using the second.

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

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

M3 - Conference contribution

AN - SCOPUS:0022191522

SN - 0444878262

SP - 98

EP - 113

BT - Unknown Host Publication Title

A2 - Koomen, Cees-Jan

A2 - Moto-Oka, Tohru

PB - North-Holland

ER -