Name
Abstract | ||
|---|---|---|
This paper presents a methodology for formally verifying the functional correctness of self-timed circuits whose data flows are free of feedback loops. In particular, we formalize the relationship between their input and output sequences. We use the DE system, a formal hardware description language built using the ACL2 theorem-proving system, to specify and verify finite-state-machine representations of self-timed circuit designs. We apply a link-joint paradigm to model self-timed circuits as networks of computations that communicate with each other with protocols. Our approach exploits hierarchical reasoning and induction to support scalability. We demonstrate our methodology by modeling and verifying several data-loop-free self-timed circuits. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1109/ASYNC.2018.00023 | 2018 24th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC) |
Keywords | Field | DocType |
asynchronous circuit modeling,asynchronous circuit verification,hierarchical verification,non deterministic behavior,link joint model,mechanical theorem proving,data loop free | Computer science,Correctness,Exploit,Input/output,ACL2,Electronic circuit,Computer engineering,Scalability,Hardware description language,Computation | Conference |
ISSN | ISBN | Citations |
1522-8681 | 978-1-5386-5884-0 | 1 |
PageRank | References | Authors |
0.37 | 6 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| cuong chau | 1 | 31 | 2.53 |
| Warren A. Hunt, Jr. | 2 | 520 | 59.18 |
| Matt Kaufmann | 3 | 22 | 5.07 |
| Marly Roncken | 4 | 298 | 63.79 |
| I. E. Sutherland | 5 | 1520 | 2067.03 |