Cuong Chau
ACL2 Seminar
March 10, 2017

Modeling and Verifying Self-Timed Circuits Using an Asynchronous
Extension of the DE System

Abstract:

In this talk, I will present in more detail our framework for
asynchronous circuit modeling and verification. I demonstrate our
framework by modeling and verifying the functional correctness of a
32-bit self-timed serial adder. I will also show my attempt to state
theorems for all modules in a way that enables compositional
(hierarchical) reasoning in our framework.