Verification of Building Blocks for Asynchronous Circuits

Freek Verbeek
(Open University of The Netherlands)
Julien Schmaltz
(Open University of The Netherlands)

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.

In Ruben Gamboa and Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2013), Laramie, Wyoming, USA , May 30-31, 2013, Electronic Proceedings in Theoretical Computer Science 114, pp. 70–84.
Published: 26th April 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.114.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org