Speaker:
Cuong K. Chau

Dissertation Title:
A Hierarchical Approach to Formal Modeling and
Verification of Asynchronous Circuits

Abstract:

The self-timed (or asynchronous) approach to circuit design has
demonstrated benefits in a number of different areas for its low
energy consumption, high operating speed, composability, and
modularity.  Nonetheless, the asynchronous paradigm exposes challenges
that are not found in the synchronous (or clock-driven) paradigm.  For
the verification task, a challenge emerges from the large number of
potential operational interleavings exhibited in the asynchronous
paradigm.  Simply exploring all interleavings is, in general,
intractable because the number of interleavings can grow
exponentially.

This dissertation focuses on developing scalable methods that are
capable of reasoning effectively about the interleaving problem
exhibited in self-timed systems.  We specify and verify
finite-state-machine representations of self-timed circuit designs
using the DE system, a formal hardware description language defined
using the ACL2 theorem-proving system.  We apply a link-joint paradigm
to model self-timed circuits as networks of channels that communicate
with each other locally via handshake protocols.  This link-joint
model has been shown to be a universal model for various self-timed
circuit families.  In addition, this model has a clean formalization
in the ACL2 logic and provides a protocol level that abstracts away
timing constraints at the circuit level.

Unlike many efforts for validating timing and communication properties
of self-timed systems, we are interested in verifying functional
properties.  Specifically, we verify the functional correctness of
self-timed systems in terms of relationships between their input and
output sequences.  To mitigate the consideration of all interleavings
simultaneously, we address the verification problem hierarchically and
avoid exploring the internal structures of verified submodules as well
as their operational interleavings.  The input-output relationship of
a verified submodule is determined based on the communication signals
at the submodule's input and output ports, while abstracting away all
execution paths internal to that submodule.