Title :
Verification of speed-independent data-path circuits
Author :
Weih, D.T. ; Greenstreet, M.R.
Author_Institution :
Dept. of Comput. Sci., British Columbia Univ., Vancouver, BC, Canada
fDate :
9/1/1996 12:00:00 AM
Abstract :
The paper demonstrates that verification techniques developed for relatively large, synchronous circuits can be applied to speed-independent, self-timed circuits. Local formulas are introduced which provide a natural way to specify the input/output behaviour of data-path circuits. The validity of a local formula is independent of the order in which the operations occur in a speed-independent circuit. The approach is demonstrated with the verification of a FIFO and a vector multiplier chip
Keywords :
formal verification; hardware description languages; logic design; logic testing; multiplying circuits; timing; FIFO chip; VHDL; input output behaviour specification; large synchronous circuits; local formula; speed-independent data-path circuit verification; speed-independent self-timed circuits; vector multiplier chip;
Journal_Title :
Computers and Digital Techniques, IEE Proceedings -
DOI :
10.1049/ip-cdt:19960703
