Verification of speed-independent data-path circuits
D. Weih, Mark R. Greenstreet · IEE Proceedings - Computers and Digital Techniques · 1996
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.