Date of Award
Fall 2023
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Department
Computer Science
First Advisor
Manohar, Rajit
Abstract
While software bugs can be addressed through patches, hardware bugs require design changes, making their resolution more time consuming and expensive. Formal methods offer the ability to prove the absence of bugs in hardware systems, and their application has been prominent in the hardware industry. However, despite the adoption of formal methods, hardware bugs are still prevalent in commercial hardware. Many existing formal methods applied in Very Large-Scale Integration (VLSI) design flows are partial or only verify specific properties rather than ensuring overall functional correctness. The dissertation tackles the verification challenge specifically for asynchronous circuits, which adopts a self-timed approach and employs explicit signaling between components. In this dissertation, we propose the formal verification techniques for three phases in asynchronous VLSI: microarchitecture designs, logic designs, and circuit designs. First, we utilize stepwise refinements design methodology and present a translation validator, enabling the validation of correctness for microarchitectural optimizations. Then, we employ theorem proving and model checking to verify the correctness of logic and circuit designs. By integrating these contributions with commercially-available verification techniques that check chip layouts against circuit designs, a verified asynchronous circuit design flow from high-level specification to chip layout is completed.
Recommended Citation
Wu, Xiang, "Formal Verification of Asynchronous VLSI Design Flow" (2023). Yale Graduate School of Arts and Sciences Dissertations. 1168.
https://elischolar.library.yale.edu/gsas_dissertations/1168
