Abstract Timing Verification for Synchronous Digital Systems

ATV, the Abstract Timing Verifier, is a program to perform static tim-ing analysis of dependency graphs derived from logic designs, analyzing representation of time and delays that enables a user to choose the represen-tation 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 in to 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 A TV 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 pro-gram 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. Report Documentation Page Form ApprovedOMB No. 0704-0188 Public reporting burden for the collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources, gathering and maintaining the data needed, and completing and reviewing the collection of information. Send comments regarding this burden estimate or any other aspect of this collection of information