Technical Reports

The ICICS/CS Reading Room

UBC CS TR-98-14 Summary

Verifying a Self-Timed Divider, March 30, 1998 Tarik Ono-Tesfaye, Christoph Kern and Mark Greenstreet, 13 pages

This paper presents an approach to verifying timed designs based on refinement: first, correctness is established for a speed-independent model; then, the timed design is shown to be a refinement of this model. Although this approach is less automatic than methods based on timed state space enumeration, it is tractable for larger designs. Our method is implemented using a proof checker with a built-in model checker for verifying properties of high-level models, a tautology checker for establishing refinement, and a graph-based timing verification procedure for showing timing properties of transistor level models. We demonstrate the method by proving the timing correctness of Williams' self-timed divider.

If you have any questions or comments regarding this page please send mail to