Formal Verification Research

Computer Engineering Research Center
The University of Texas at Austin

In recent years, significant gains have been made in formally verifying systems using symbolic model checking and related research. However, there still exists a gap between what can be efficiently verified in the research community and what needs to be formally verified in industry. Our view is that the key problem is one of finding useful abstractions which will reduce the complexity of verifying large designs. Research has shown that significant reductions are possible when verifying systems structured symmetrically or whose datapaths can be removed logically. The difficulty is that these methods are still not strong enough to deal with industrial designs. We are exploring new and powerful abstractions, with the designer as an active participant in the process. This is being done by viewing designs at multiple levels in the design hierarchy to further reduce the computational complexity. The goal of this research is to introduce new techniques in building decompositions of systems from high-level descriptions of designs into abstract representations which are complete with respect to a property of interest.

We have recently developed a novel approach for formally verifying both safety and liveness properties of designs using sequential ATPG tools. The properties are automatically mapped into a monitor circuit with a target fault so that finding a test for the fault corresponds to formally establishing the property. The mapping of the properties to the monitor circuit is described in detail and the process is shown to be sound and complete. Experimental results show that the ATPG-based approach performs better than existing verification techniques, especially for large designs.

Research projects include:

New techniques for Boolean Verification

Verifying the equivalence of two Boolean functions is a the heart of all verification. Since even this problem is very complex in general, we have developed a variety of solutions to verifying large functions. These include probabilistic verification, indexed Binary Decision Diagrams, functional partitioning and the use of multiple filters.

Techniques for Verifying Large Sequential Circuits

This work explores abstractions which will ameliorate the state space explosion when dealing with large designs.
A paper describing our recent work, Verifying Properties Using Sequential ATPG, will be presented at the 2002 International Test Conference.

Verification of Analog and Mixed-Signal circuits

Techniques for verifying the correctness of analog circuits and interfacing these results with digital verification to address mixed-signal circuits are explored.

Back to: