A DE Verification Framework for Asynchronous Circuit Verification

Cuong Chau
ACL2 Seminar
Jan. 27, 2017

Abstract:

Formal verification in asynchronous circuits is known to be
challenging due to highly non-deterministic behavior exhibited in
these systems. One of the main challenges is that it is very hard to
come up with a systematic approach to establishing invariance
properties, which are crucial in proving the correctness of circuit
behavior. Non-determinism also results in asynchronous circuits having a
large state space, and hence makes the verification task much more
difficult than in synchronous circuits. To ease the verification task
by reducing non-determinism, and consequently reducing the state
space, we impose extra sequential dependencies among operations in
asynchronous circuits. These constraints enable our DE verification
framework to be able to compute invariants and consequently verify the
correctness of asynchronous circuit designs. Our framework applies a
hierarchical verification approach similar to the FM9001
microprocessor verification, which was originally created by Bishop
Brock and Warren Hunt in the DUAL-EVAL verification system - the
precursor of DE that was developed in the NQTHM theorem-proving
system. In this talk, I will demonstrate our framework by modeling and
proving the correctness of a 32-bit asynchronous sequential serial
adder.