Language emptiness checking using MDGs

ABSTRACT

Multiway Decision Graphs (MDGs) are efficient diagrams suitable for the modeling and automatic verification of register transfer level designs. The MDG tools provide a first-order branching time model checking, sequential equivalence checking, and combinational verification. In this paper, we present a new model checking algorithm based on language emptiness checking using MDGs. The proposed procedure makes use of the Wring tool from UC Berkeley to generate the property automaton. Language emptiness is checked on the product of this latter and the design automaton represented in terms of MDGs. Compared with the existing MDG model checking, our algorithm shows superior performance. We also conducted experimental comparison between our tool, VIS from UC Berkeley and Cadence FormalCheck.

REFERENCES

• 1: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 2: F. Corella , Z. Zhou , X. Song , M. Langevin , E. Cerny, Multiway Decision Graphs for Automated Hardware Verification, Formal Methods in System Design, v.10 n.1, p.7-46, February 1997 [doi>10.1023/A:1008663530211 ]
• 3: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 4: K. Fisler and S. Johnson. Integrating design and verification environments through a logic supporting hardware diagrams. In IFIP Conference on Hardware Description Language and their Applications, Chiba, Japan, 1995.
• 5: Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999 [doi>10.1145/307988.307989]
• 6: P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, 1994.
• 7: Fabio Somenzi , Roderick Bloem, Efficient Büchi Automata from LTL Formulae, Proceedings of the 12th International Conference on Computer Aided Verification, p.248-263, July 15-19, 2000
• 8: Moshe Y. Vardi, An automata-theoretic approach to linear temporal logic, Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata, p.238-266, April 1996, Banff, Canada
• 9: Ying Xu , Eduard Cerny , Xiaoyu Song , Francisco Corella , Otmane Aït Mohamed, Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs, Proceedings of the 10th International Conference on Computer Aided Verification, p.219-231, June 28-July 02, 1998
• 10: Z. Zhou and N. Boulerice. MDG Tools (V1.0) User's Manual. D'IRO, University of Montreal, 1996.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Verification

General Terms:
Verification

Keywords:
MDGs (multiway decision graphs), ROBDDs (reduced ordered binary decision diagrams), büchi automata, formal hardware verification, language emptiness checking, model checking