  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.
