Automatic verification of asynchronous circuits

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

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)
Title of host publicationLogics of Programs - Workshop
PublisherSpringer-Verlag
Pages101-115
Number of pages15
ISBN (Print)9783540128960
DOIs
StatePublished - Jan 1 1984
EventWorkshop on Logics of Programs, 1983 - Pittsburgh, United States
Duration: Jun 6 1983Jun 8 1983

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume164 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherWorkshop on Logics of Programs, 1983
CountryUnited States
CityPittsburgh
Period6/6/836/8/83

Fingerprint

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Clarke, E., & Mishra, B. (1984). Automatic verification of asynchronous circuits. In Logics of Programs - Workshop (pp. 101-115). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 164 LNCS). Springer-Verlag. https://doi.org/10.1007/3-540-12896-4_358

Automatic verification of asynchronous circuits. / Clarke, E.; Mishra, Bhubaneswar.

Logics of Programs - Workshop. Springer-Verlag, 1984. p. 101-115 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 164 LNCS).

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

Clarke, E & Mishra, B 1984, Automatic verification of asynchronous circuits. in Logics of Programs - Workshop. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 164 LNCS, Springer-Verlag, pp. 101-115, Workshop on Logics of Programs, 1983, Pittsburgh, United States, 6/6/83. https://doi.org/10.1007/3-540-12896-4_358
Clarke E, Mishra B. Automatic verification of asynchronous circuits. In Logics of Programs - Workshop. Springer-Verlag. 1984. p. 101-115. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-12896-4_358
Clarke, E. ; Mishra, Bhubaneswar. / Automatic verification of asynchronous circuits. Logics of Programs - Workshop. Springer-Verlag, 1984. pp. 101-115 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a45c791a21154daeb11a83a2b754f61c,
title = "Automatic verification of asynchronous circuits",
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 = "E. Clarke and Bhubaneswar Mishra",
year = "1984",
month = "1",
day = "1",
doi = "10.1007/3-540-12896-4_358",
language = "English (US)",
isbn = "9783540128960",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "101--115",
booktitle = "Logics of Programs - Workshop",

}

TY - GEN

T1 - Automatic verification of asynchronous circuits

AU - Clarke, E.

AU - Mishra, Bhubaneswar

PY - 1984/1/1

Y1 - 1984/1/1

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=85034592351&partnerID=8YFLogxK

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

U2 - 10.1007/3-540-12896-4_358

DO - 10.1007/3-540-12896-4_358

M3 - Conference contribution

SN - 9783540128960

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 101

EP - 115

BT - Logics of Programs - Workshop

PB - Springer-Verlag

ER -