Cuong Chau
ACL2 Seminar
Apr. 13, 2018

Abstract:

In this talk, I will illustrate our self-timed modeling and
verification methodology by walking through the ACL2 source code of a
circuit example, namely, a self-timed FIFO queue of two links.  If
time permits, I will show another example of specifying and verifying
a self-timed circuit that contains a feedback loop in its data flow,
namely, a circuit computing the greatest common divisor of two natural
numbers.