ATV, the Abstract Timing Verifier, is a program to perform static timing analysis of dependency graphs derived from logic designs, analyzing worst-case paths. Unlike other timing verifiers, ATV uses an abstract representation of time and delays that enables a user to choose the representation of time and delays most suitable to a particular analysis. Such representations include single numbers, ranges [min-max], and statistical descriptions (mean and standard deviation), or asymmetric rise/fall versions of all of these. The sophisticated user may develop new models and plug them into the program.
This technical report consists of the main body of my dissertation of the same title. It describes the background of the Abstract Timing Model that ATV uses, several different timing models, implementation of the principle algorithm for clock phase length analysis of transparent latch designs, and results of using the program. Detailed information about how to use the program is available in the companion technical report, User's Guide to ATV, an Abstract Timing Verifier, which also appeared as the appendix to my dissertation.