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: