Formal verification of asynchronous data-path circuits

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.Science, Faculty ofComputer Science, Department ofGraduat