Model Reductions and a Case Study

  • Jin Hou
  • Eduard Cerny
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


In this paper, we present a model reduction algorithm for property checking. For the property to be verified, we first construct a property de- pendencygraph which represents the function dependency of the property on variables. 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 de- tailedmodel 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 in- termediatereduced models preserve the property weakly. Our reduction algo- rithmis completely automatic. Since there is no preimage operation in MDG (Multiway Decision Graph) model checker 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, how- ever,it can be used in other tools as well. We then discuss a quite common circuit structure which appears in telecommunication and data processing cir- cuits.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.


Model Check Temporal Logic Clock Cycle Model Reduction Transition Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    F. Corella, Z. Zhou, X. Song, M. Langevin, E. Cerny. Multiway Decision Graphs for Automated Hardware Verification. In Formal Methods in System Design, 10(1),1997.Google Scholar
  2. [2]
    Z. Zhou, X. Song, F. Corella, E. Cerny, M. Langevin. Description and Verification of RTL Design Using Multiway Decision Graphs.Technical Report RC19822,IB T.J.Watson Research Center, November 1994.Google Scholar
  3. [3]
    Y. Xu. Model Checking for a First-order Temporal Logic Using Multiway Decision Graphs. Ph.D thesis, University of Montreal, 1999.Google Scholar
  4. [4]
    Y. Xu, E. Cerny, X. Song, F. Corella, O. Mohamed. Model Checking for a First-Order Temporal Logic using Multiway Decision Graphs. In Proceedings of Conference on Computer Aided Verification (CAV 98), July 1998.Google Scholar
  5. [5]
    Y. Xu, E. Cerny, A. Silburt, A. Coady, Y. Liu, P. Pownall. Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors. Charme 1999.Google Scholar
  6. [6]
    E. Allen Emerson. Temporal and Modal Logic, 16th chapter of Hand book of Theoretical Computer Science, edited by ed]J. van Leeuwen. Elsevier Science Publishers B.V 1990.Google Scholar
  7. [7]
    R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers, 35(8), Auguest 1986.Google Scholar
  8. [8]
    J.R. Brurch, E.M. Clarke, D.E. Long, K.L. McMillan, D.L. Dill. Symbolic Model Checking for Sequencial Circuit Verification. In IEEE Transactions on Computer-Aided Design, 13(4), April 1994.Google Scholar
  9. [9]
    K.L. McMillan. Symbolic model checking-an approach to the state explosion problem. Ph.D thesis, SCS, Carnegie Mellon University, 1992.Google Scholar
  10. [10]
    J.R. Brurch, E.M. Clarke, K.L. McMillan. Symbolic Model Checking: 1020 States and Beyond. In proceeding of LICS 1990.Google Scholar
  11. [11]
    E. Clarke, O. Grumberg, and D. Long. Verification tools for Finite-State Concurrent Systems, Lecture Notes in Computer Science 803, 1994.Google Scholar
  12. [12]
    E. Clarke, O. Grumberg, and D. Long. Model Checking and Abstraction. In ACM-TOPLAS, Vol 16, No.5, September 1994.Google Scholar
  13. [13]
    E.M. Clarke, T. Filkorn, S. Jha. Exploiting Symmetry in Temporal Logic Model Checking. In Formal Mrthods in System Design, Vol 9, 1996.Google Scholar
  14. [14]
    C. Norris Ip, David Dill. Better Verification Through Symmetry. In Formal Methods in System Designs, Vol 9, Auguest 1996.Google Scholar
  15. [15]
    H.J. Touati, R.K. Brayton, R. Kurshan. Testing Language Containment for w-Automata Using BDDs. in Information and Computation 118, 1995.Google Scholar
  16. [16]
    R.P. Kurshan. Reducibility in Analysis of Coordination. In Lecture Notes in Control and Information Sciences. Vol 103, 1987.Google Scholar
  17. [17]
    R.P. Kurshan. Analysis of Discrete Event Coordination. In Lecture Notes in Compute Science. Vol 430, 1990.Google Scholar
  18. [18]
    M. Sela, F. Limor, I. Haifa. Input Elimination and Abstraction in Model Checking. FMCAD98, Nov 3-6, 1998.Google Scholar
  19. [19]
    G. Cabodi, P. Camurati, S. Quer. Improved Reachability Analysis of Large Finite State Machines. ICCAD 96, Nov 10-14, 1996.Google Scholar
  20. [20]
    C. Norris Ip, David Dill. State Reduction Using Reversible Rules. In 33rd Design Automation conference, Las Vegas, June 1996.Google Scholar
  21. [21]
    H. Higuchi, Y. Matsunaga. A Fast State Reduction Algorithm for Incompletely Spec ified Finite State Machines. In 33rd Design Automation Conference, Las Vegas, June 1996.Google Scholar
  22. [22]
    E.A. Emerson, A.P. Sistla. Symmmetry and Model Checking. In CAV93, June 1993.Google Scholar
  23. [23]
    Dennis Rene Dams. Abstract Interpretation and Partition Refinement for Model Checking. Ph.D thesis, Eindhoven University of Technology, 1996.Google Scholar
  24. [24]
    Dennis Dams, Orna Grumberg, Rob Gerth. Generation of Reduced models for Checking Fragments of CTL. In CAV93, June 1993.Google Scholar
  25. [25]
    David Lee, Mihalis Yannakakis. Online Minimization of Transition Systems. 24th Annual ACM STOC 1992.Google Scholar
  26. [26]
    K. Fisler, Moshe Y. Vardi. Bisimulation Minimization in an Automata-Theoretic Verification Framework. FMCAD98, Nov 3-6, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Jin Hou
    • 1
  • Eduard Cerny
    • 1
  1. 1.Dépt.IROUniversité de MontréalQCCanada

Personalised recommendations