UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Verifying a self-timed division chip Ono-Tesfaye, Tarik


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.

Item Media

Item Citations and Data


For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.