A Framework for Asynchronous Circuit Modeling and Verification in ACL2 Cuong Chau ACL2 Seminar Sep. 22, 2017 Abstract: The asynchronous (or self-timed) approach to circuit design has demonstrated benefits in a number of different areas, including low power consumption, high operating speed, and better composability and modularity for large systems. Nonetheless, the asynchronous paradigm exposes great challenges in both design and verification that are not found in the synchronous (or clock-driven) paradigm. In the verification task, the challenge emerges from non-deterministic circuit behavior exhibited in the asynchronous paradigm. Reasoning with highly non-deterministic systems, especially circuits with feedback loops, can become formidable. In this talk, I will present a framework for specifying and verifying the functional correctness of self-timed circuit designs using ACL2. Our framework applies a link-joint paradigm to model self-timed circuits as networks of channels that communicate with each other locally via handshake protocols. Our approach exploits hierarchical reasoning, compositional reasoning, and induction to support scalability. I will demonstrate our framework through several case studies.