Clayton B. McDonald Carnegie Mellon University

Symbolic Functional and Timing Verification of Transistor-Level Circuits

This talk focuses on a new approach to timing and functional verification of full-custom transistor-level circuits. Current methodologies verify functionality and timing separately, resulting in higher efficiency and capacity. However, for many full-custom circuits, timing and functionality are tightly coupled, rendering current methods ineffective. Furthermore, the lack of functional information during timing analysis implies that heuristics must be used to determine timing constraints such as latch setups, pulse-width constraints, etc. These heuristics are often unable to handle the range of possible design styles used in full-custom methodologies. Our approach is based on symbolic simulation, where Boolean variables are applied to the circuit inputs rather than constant 0's or 1's. In this manner, we effectively perform a timing simulation for every possible input pattern concurrently. By verifying that the resultant Boolean functions on the output nodes are correct, we can show that all internal timing constraints must have been satisfied without using heuristics to explicitly identify them. While this methodology is substantially more compute-intensive than static timing analysis, it is surprisingly efficient and can be applied to a much more general class of circuits. One of the primary goals of this research is to integrate both methodologies such that symbolic timing simulation may be used only where necessary, and its results used in higher-level static analyses.

Bio
Clayton B. McDonald received the B.S. and M.S.E.E degrees in Electrical Engineering from the Georgia Institute of Technology in 1992 and 1993, respectively. From 1993 through 1997, he was a member of Hewlett Packard's Microprocessor Technology Lab, Fort Collins, CO, where he worked on chip-level timing analysis, power characterization, and circuit design. In 1998, he began work on the Ph.D. degree in Electrical Engineering at Carnegie Mellon University, Pittsburgh.