Open Collections

Formal verification of asynchronous data-path circuits

University of British Columbia

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.

Thesis/Dissertation

application/pdf

2009-02-11

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.

http://hdl.handle.net/2429/4469

Computer Science

University of British Columbia

UBCV

DSpace