Cuong Chau
ACL2 Seminar
Nov. 30, 2018

Title:

A Review of the Self-Timed Circuit Verification Framework

Abstract:

I will briefly review the ACL2 verification framework for self-timed
circuit designs that I presented in my last seminar talk.  I will
illustrate the framework through the following two examples, with the
emphasis on discussing single-step-update properties and multi-step
input-output relationships.

- a deterministic self-timed circuit: a FIFO queue of two links; and

- a non-deterministic self-timed circuit: a circuit performing
  arbitrated merges.