Model Reductions and a Case Study

Jin Hou, Eduard Cerny

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


In this paper, we present a model reduction algorithm for property checking. For the property to be verified, we first construct a property dependency graph. Beginning from the set of state variables appearing in the property, we search through the property dependency graph and add a noncorrelated set of state variables to the current set of state variables to construct a more detailed model at each reduction iteration step. The final reduced model is the one which is constructed by using all state variables that can be reached in the graph. The final reduced model preserves the property strongly, while the intermediate reduced models preserve the property weakly. Our reduction algorithm is completely automatic. Since there is no preimage operation in MDG due to the presence of abstract state variables, all backward reduction algorithms cannot be used in MDG. Our method is suitable for MDG and has been implemented in this tool, however, it can be used in other tools as well. We then discuss a quite common circuit structure which appears in telecommunication and data processing circuits. We use three verification tools MDG, FormalCheck and SMV to verify this circuit. The experimental results show that our reduction algorithm is more efficient on these typical structures.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Start Conference Manager
Conference Systems