A Framework for Asynchronous Circuit Modeling and Verification in ACL2

Cuong Chau
ACL2 Seminar
Oct. 20, 2017

Abstract:

This talk is the follow-up to my previous seminar talk about
asynchronous circuit modeling and verification using ACL2. In this
talk, I will briefly review our framework and then focus on
demonstrating this framework through case studies of self-timed
circuits that have no feedback loops. If time permits, I will briefly
describe our verification of a self-timed circuit with a feedback
loop, in particular, a 32-bit self-timed serial adder. The talk will
conclude with possible future work.