High-Level Model Checking Using Wu's Method

As the size and functional complexity of integrated circuits increase, design verification becomes a more and more important aspect of the design flow. Classical simulation method cannot meet with the tremendous verification demand of complex IC designs. Because of this, formal verification receives more and more attentions from academic circles as an important assistant.As one of important formal verification techniques, model checking is widely used in the industrial practice because of the trait of high degree of automation and strong ability. Existing model checking methods are mostly based on bit-level techniques such as BDD or SAT, which mainly aim at low level control dominated designs. However, current chips emphasis the abilities of signal processing, data communication, picture/multimedia processing and operation. A variety of communication units, ranging from arithmetic operation modules to data paths are embedded on a signal chip. Existing model checking techniques are hard to satisfy the verification requirement of high level data dominated designs.In this paper, a novel model checking approach for the high level design verification is proposed. We conduct the research from two aspects: the expression model and the verification algorithm. In the approach, functions of circuit components are represented by polynomial equations, and high level temporal logic formulae are directly applied to this representation. Wu's method for mechanical theorem proving is then applied in the framework of model checking. Firstly, circuit is unrolled over timeframes to obtain a set of polynomial equations. Secondly, temporal logic formula which describes the property is translated to another set of polynomial equations according to bounded semantics. Let the first set of polynomial equations be the hypothesis and the second set of polynomial equations be the conclusion, then the original model checking problem is reduced to the task of theorem proving which can be solved by Wu's method efficiently.A series of experiments have been done in order to validate the proposed approach. Experimental results demonstrate that the new approach achieves the expectation effect.