Modeling and Verifying Asynchronous Circuits Using the DE System

Cuong Chau
ACL2 Seminar
Mar. 23, 2018

Abstract:

The asynchronous (or self-timed) approach to circuit design has
demonstrated benefits in a number of different areas, including low
power consumption, high operating speed, and better composability and
modularity for large systems.  Nonetheless, the asynchronous paradigm
exposes great challenges in both design and verification that are not
found in the synchronous (or clock-driven) paradigm.  In the
verification task, the challenge emerges from non-deterministic
circuit behavior exhibited in the asynchronous paradigm.  Reasoning
with highly non-deterministic systems, especially ones with feedback
loops in their data flows, can become formidable.

The proposed dissertation focuses on developing scalable methods for
reasoning about the functional correctness of self-timed circuits and
systems using the ACL2 theorem-proving system.  Our framework uses the
DE system, a formal hardware description language built using ACL2, 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 channels that communicate with each other
locally via handshake protocols.  We develop a hierarchical
verification method that scales well by abstracting away the internal
structures of verified subsystems as well as their operational
interleavings.  In this proposal, I will demonstrate our framework by
modeling and verifying the functional correctness of several
self-timed circuit designs.