Thesis Defense - Pardo

During the last few years, the complexity and size of the digital systems has increased so drastically, that almost every stage in the design flow has changed significantly. In that flow, simulation used to be the most used technique to guarantee the correctness of a digital system.

Formal verification provides a different approach to validate a system. It allows to reason formally about its behavior. The implementation of a system is checked against the specification of the properties to be satisfied. The most common paradigms are based on theorem proving, model checking and language containment. Typically, a digital system is modeled as a collection of interacting sub-systems. As new sub-systems are added the number of states may grow exponentially. This is known as the "state explosion" problem.

Abstract interpretation is one approach to alleviate the state explosion problem. The main idea is to interpret the behavior of a system in a different abstracted (and therefore simplified) system with fewer states.

The main challenge for these techniques is the degree of automation provided to the designer. So far, automatic abstraction mechanisms have been applied in very specific examples, and they usually require the intervention of the designer to guide the process.

This dissertation proposes an automatic abstraction paradigm to verify generic digital systems. First, an abstraction theory in the context of model checking of the mu-calculus logic is presented. Necessary conditions are given for an abstraction to provide a conservative answer to the verification problem.

Second, a practical implementation of the concepts developed in the theory is presented. The algorithm is based in an initial verification of the formula with an approximation, and a posterior refinement stage in which the abstraction is gradually modified to achieve verification. The algorithm has been integrated in VIS (Verification Interacting with Synthesis) a tool for the verification of digital systems.

To show its applicability, the tool has been successfully applied to the verification of some real life examples. A system controlling a metal processing plant, as well as a model of the Ethernet protocol have been successfully verified applying the abstraction techniques discussed in this dissertation.