Symbolic Model Checking and Simulation with Temporal Assertions

Abstract

Assuring correctness of digital designs is one of the major tasks in the system design flow. In the last decade, traditional functional verification techniques like simulation with test benches and monitors have been augmented with formal techniques. Formal techniques can be divided into equivalence and property checking. Equivalence checking tools at the gate level are now part of most design flows. However, property checking is still subject to intensive research efforts due to the omnipresent state explosion problem.

Property checking is performed in two steps. First, a set of property specifications has to be written in an appropriate formalism. The system model is then checked against these properties. A property checking tool then either reports the absence of defects on the explored paths or generates a counter example trace.

In this work we show that formal property specifications can be reused in all phases of the verification process, including both functional and formal approaches. The properties provide the link between these usually rivaling techniques. First, we discuss current formalisms for specifying temporal properties. Then we present two automata based techniques for checking temporal properties given in the standardized Property Specification Language (PSL). The first approach checks the properties during SystemC simulation, whereas the second approach performs fully formal property checking of the temporal properties against a transition system employing a unique checking algorithm.

The results described in this article have been achieved in the course of the DFG project GRASP within the DFG Priority Programme 1064.