Modeling Asynchronous Circuits in ACL2 Using the Link-Joint Interface

Cuong Chau
ACL2 Seminar
Apr. 19, 2016

Abstract:

The asynchronous approach in circuit design has demonstrated
advantages in a number of different areas, including low power
consumption, high operating speed, better composability and
modularity. Unlike the synchronous approach, there is no global clock
signal distributed in asynchronous systems. In such systems, the
communication between components is performed via local handshake
protocols. It is interesting that handshake interfaces can be
established and generalized easily under the link-joint point of view
described in Roncken et al.'s paper - Naturalized Communication and
Testing. In this talk, I will briefly describe the link and joint
concepts introduced in Roncken et al.'s paper and how to establish a
handshake channel in terms of the link-joint interface. I will also
present our formalization of these concepts using our new version of
DE - a hardware description language written in ACL2. By applying the
link-joint interface, I will then illustrate how to build a simple
while-loop circuit in an asynchronous manner and prove certain
properties of this circuit in ACL2.