Data-Loop-Free Self-Timed Circuit Verification
| Autor: | Warren A. Hunt, Marly Roncken, Matt Kaufmann, Cuong K. Chau, Ivan E. Sutherland |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Correctness
LOOP (programming language) Computer science Computation Hardware description language 020207 software engineering 02 engineering and technology ACL2 Computer engineering Asynchronous communication Scalability 0202 electrical engineering electronic engineering information engineering computer Electronic circuit computer.programming_language |
| Zdroj: | ASYNC |
| DOI: | 10.1109/async.2018.00023 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|