An Update on Self-Timed Circuit Verification

Cuong Chau
ACL2 Seminar
Sep. 21, 2018

Abstract:

This talk is divided into three parts:

1. review the progress of my work on developing a hierarchical method
   for self-timed circuit modeling and verification;

2. present the main steps in my verification flow; and

3. discuss my strategy for verifying a well-known type of self-timed
   circuit that produces non-deterministic output sequences, that is,
   circuits allocating mutually exclusive access to shared resources.
   This work has involved developing a library that supports reasoning
   about the membership relation and the interleaving operation.