Automatic verification of sequential circuits using temporal logic

M. Browne, E. Clarke, D. Dill, B. 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 - Dec 1 1985

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Automatic verification of sequential circuits using temporal logic'. Together they form a unique fingerprint.

  • 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.