UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Formal verification of asynchronous data-path circuits Weih, David T.


Asynchronous designs are typically modelled with non-deterministic next-state relations. When a deterministic model is available, specialised verification techniques can be used to automatically verify relatively large designs. This thesis demonstrates that verification techniques developed for deterministic models can be applied to speed-independent self-timed circuits. We introduce local formulas, and show that the validity of a local formula is independent of the order in which the components of a speed-independent circuit perform their operations. Local formulas provide a natural way to specify the input/output behaviour of a circuit and are well-suited for specifying data-paths. We demonstrate the practicality of our approach by describing the verification of three designs: a FIFO, an adder, and a vector multiplier chip.

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.