ATV: an abstract timing verifier

A discussion is presented of implementation and extensions of an abstract timing verifier, and in particular, several novel operations and a novel algorithm for analyzing critical paths that extend through transparent latches and stretch over multiple machine cycles. By placing events in different reference frames that can be translated relative to one another, the program can be used either to check a design for timing errors when the clock schedule is fixed and known, or to derive spacing constraints between clock edges when only the relative ordering of the clock edges is known. All algorithms are designed to operate on a wide variety of representation of time and delay.<>