TY - JOUR
T1 - Hierarchical verification of asynchronous circuits using temporal logic
AU - Mishra, B.
AU - Clarke, E.
N1 - Funding Information:
by NSF under Grant No. MCS-82-16706.
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
AN - SCOPUS:0021899094
SN - 0304-3975
VL - 38
SP - 269
EP - 291
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - C
ER -