Paper Info
Title
Symbolic verification of timed asynchronous hardware protocols
Abstract
Correct interaction of asynchronous protocols requires verification. Timed asynchronous protocols add another layer of complexity to the verification challenge. A methodology and automated tool flow have been developed for verifying systems of timed asynchronous circuits through compositional model checking of formal models with symbolic methods. The approach uses relative timing constraints to model timing in asynchronous hardware protocols - a novel mapping of timing into the verification flow. Relative timing constraints are enforced at the interface external to the protocol component. SAT based and BDD based methods are explored employing both interleaving and simultaneous compositions. We present our representation of relative timing constraints, its mapping to a formal model, and results obtained using NuSMV on several moderate sized asynchronous protocol examples. The results show that the capability of previous methods is enhanced to enable the hierarchical verification of substantially larger timed systems.
Year
DOI
Venue
2013
10.1109/ISVLSI.2013.6654650
ISVLSI
Keywords
Field
DocType
asynchronous circuits,binary decision diagrams,computability,formal verification,logic CAD,protocols,BDD based methods,CAD tool flow,NuSMV,SAT based method,automated tool flow,compositional model checking,formal models,hierarchical verification,relative timing constraints,symbolic methods,symbolic verification,timed asynchronous circuits,timed asynchronous hardware protocols,timing mapping,verification flow
Asynchronous communication,Functional verification,Model checking,Computer science,Intelligent verification,Computability,Computer hardware,High-level verification,Interleaving,Formal verification
Conference
ISSN
Citations 
PageRank 
2159-3469
4
0.46
References 
Authors
6
3
Name
Order
Citations
PageRank
Krishnaji Desai140.46
Kenneth S. Stevens218525.65
John O'Leary351.62