Hierarchical verification of asynchronous circuits using temporal logic

B. Mishra, E. Clarke

Research output: Contribution to journalArticle

Abstract

Establishing the correctness of complicated asynchronous circuit is in general quite difficult because of the high degree of nondeterminism that is inherent in such devices. Nevertheless, it is also very important in view of the cost involved in design and testing of circuits. We show how to give specifications for circuits in a branching time temporal logic and how to mechanically verify them using a simple and efficient model checker. We also show how to tackle a large and complex circuit by verifying it hierarchically.

Original languageEnglish (US)
Pages (from-to)269-291
Number of pages23
JournalTheoretical Computer Science
Volume38
Issue numberC
DOIs
StatePublished - 1985

Fingerprint

Asynchronous Circuits
Temporal logic
Temporal Logic
Networks (circuits)
Nondeterminism
Branching
Correctness
Specification
Verify
Testing
Costs
Specifications
Model

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Hierarchical verification of asynchronous circuits using temporal logic. / Mishra, B.; Clarke, E.

In: Theoretical Computer Science, Vol. 38, No. C, 1985, p. 269-291.

Research output: Contribution to journalArticle

@article{1b73f3c3761f40bc8bb1fe74b4e4fd29,
title = "Hierarchical verification of asynchronous circuits using temporal logic",
abstract = "Establishing the correctness of complicated asynchronous circuit is in general quite difficult because of the high degree of nondeterminism that is inherent in such devices. Nevertheless, it is also very important in view of the cost involved in design and testing of circuits. We show how to give specifications for circuits in a branching time temporal logic and how to mechanically verify them using a simple and efficient model checker. We also show how to tackle a large and complex circuit by verifying it hierarchically.",
author = "B. Mishra and E. Clarke",
year = "1985",
doi = "10.1016/0304-3975(85)90223-3",
language = "English (US)",
volume = "38",
pages = "269--291",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "C",

}

TY - JOUR

T1 - Hierarchical verification of asynchronous circuits using temporal logic

AU - Mishra, B.

AU - Clarke, E.

PY - 1985

Y1 - 1985

N2 - Establishing the correctness of complicated asynchronous circuit is in general quite difficult because of the high degree of nondeterminism that is inherent in such devices. Nevertheless, it is also very important in view of the cost involved in design and testing of circuits. We show how to give specifications for circuits in a branching time temporal logic and how to mechanically verify them using a simple and efficient model checker. We also show how to tackle a large and complex circuit by verifying it hierarchically.

AB - Establishing the correctness of complicated asynchronous circuit is in general quite difficult because of the high degree of nondeterminism that is inherent in such devices. Nevertheless, it is also very important in view of the cost involved in design and testing of circuits. We show how to give specifications for circuits in a branching time temporal logic and how to mechanically verify them using a simple and efficient model checker. We also show how to tackle a large and complex circuit by verifying it hierarchically.

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

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

U2 - 10.1016/0304-3975(85)90223-3

DO - 10.1016/0304-3975(85)90223-3

M3 - Article

VL - 38

SP - 269

EP - 291

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - C

ER -