Verifying a self-timed division chip
Tarik Ono-Tesfaye · cIRcle (University of British Columbia) · 2009
The formal verification of asynchronous circuits is challenging, because they often have non-deterministic timing relations between circuit components. This thesis presents a formal proof strategy for verifying the correctness of a dual-rail, asynchronous divider chip. For that purpose, this thesis will extend timing verification techniques that were originally developed for combinational logic to apply to dual-rail, self-timed designs. The proof strategy is refinement based and employs four progressively more detailed models of the divider. Key safety properties are first established for the abstract models using model checking. These properties are then shown to hold for the more detailed models by verifying refinement between adjacent levels in the model hierarchy.