Verification of Building Blocks for Asynchronous Circuits
The work
| Authors | Freek Verbeek; Julien Schmaltz |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2013 |
| Citekey | verbeek2013verification |
Where it appeared
| Published in | Proceedings of the 11th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2013) |
|---|---|
| Series | Electronic Proceedings in Theoretical Computer Science |
| Volume | 114 |
Identifiers
| arXiv | 1304.7859 from its landing_page_url |
|---|---|
| DOI | 10.4204/eptcs.114.6 |
Access
| Landing page | https://arxiv.org/abs/1304.7859 |
|---|
Related
| Distinct from | kurze2026nocout |
|---|---|
| Distinct from | vangastel2013formalisation |
From bibtex.
Abstract
Scalable formal verification constitutes an important challenge for the design of asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We present our approach to using ACL2 to verify necessary and sufficient conditions over asynchronous delay-insensitive primitives. These conditions are used to derive SAT/SMT instances from circuits built out of these primitives. These SAT/SMT instances help in establishing absence of deadlocks. Our verification effort consists of building an executable checker in the ACL2 logic tailored for our purpose. We prove that this checker is correct. This approach enables us to prove ACL2 theorems involving defun-sk constructs and free variables fully automatically.
Cite it as
@inproceedings{verbeek2013verification,
title = {Verification of Building Blocks for Asynchronous Circuits},
author = {Freek Verbeek and Julien Schmaltz},
year = {2013},
booktitle = {Proceedings of the 11th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2013)},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {114},
doi = {10.4204/eptcs.114.6},
}
This record lives at https://refs.drheap.org/verbeek2013verification/ and will keep doing so.