A New Approach to Formal Design Verification

Verification of a chip now involves over 50% of the design effort, and this percentage is expected to worsen in the future. Simulation is the primary approach in industry for design verification, but the probability of detecting subtle bugs decreases as designs increase in complexity, On the other hand, formal techniques for verification are limited in the sizes of designs they can handle.

This talk will give a brief overview of formal approaches to functional design verification. It will then describe a novel approach for formally verifying both safety and liveness properties of designs using tools originally developed for automatic test pattern generation (ATPG)
for faults in manufactured chips. The properties to be verified are automatically mapped into a monitor circuit with a target fault so that finding a test (a sequence of inputs) for the fault corresponds to formally establishing the property. The mapping of the properties to the monitor circuit will be described in detail and the process will be shown to be sound and complete. The fundamental benefits of an ATPG-based search over conventional satisfiability (SAT) based search will be discussed. Experimental results show that the ATPG-based approach requires orders of magnitude less time and scales much better than current tools for formal property checking.
Jacob A. Abraham is a Professor in the departments of Electrical and Computer Engineering and Computer Sciences at the University of Texas at Austin. He is also director of the Computer Engineering Research Center and holds a Cockrell Family Regents Chair in Engineering. He received a Ph.D. in Electrical Engineering with minor in Computer
Science from Stanford University in 1974. He has published extensively, has supervised more than 50 Ph.D. dissertations, and has been elected Fellow of both the IEEE and the ACM. His current research involves hierarchical techniques to develop highly effective
manufacturing tests for digital and analog integrated circuits, as well as new approaches to verifying the correctness of complex integrated circuits. He is also working with local industry in developing a new Master's program in Electrical and Computer Engineering focusing on Digital and Mixed-Signal Circuit Design.