Adaptive variable reordering for symbolic model checking

被引：4
|
作者：
Kamhi, G [1 ]
Fix, L [1 ]
机构：
[1] Intel Israel Ltd, Future CAD Technol, Haifa, Israel
来源：
1998 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN: DIGEST OF TECHNICAL PAPERS | 1998年
关键词：
binary decision diagram; variable reordering; symbolic model checking;
D O I：
10.1109/ICCAD.1998.742897
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this paper, we present an adaptive dynamic variable ordering paradigm which is application-dependent and intended for symbolic model checking applications. The impact of the adaptive variable reordering approach is demonstrated on circuits from Intel's next-generation micro-processors. On large circuits, in particular, our algorithms make verification tasks that would never end finish successfully in a reasonable amount of time. Our approach, to the best of our knowledge, pioneers in applying successfully ROBDD-independent and application-specific heuristics to the domain of dynamic variable reordering.
引用
收藏
页码：359 / 365
页数：7
相关论文
共 50 条
  • [1] Increasing efficiency of symbolic model checking by accelerating dynamic variable reordering
    Meinel, C
    Stangier, C
    DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION 1999, PROCEEDINGS, 1999, : 760 - 761
  • [2] Model-based variable and transition orderings for efficient symbolic model checking
    Johnston, Wendy
    Winter, Kirsten
    van den Berg, Lionel
    Strooper, Paul
    Robinson, Peter
    FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 524 - 540
  • [3] Symbolic model checking
    McMillan, KL
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
  • [4] Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Buchi automata
    Klein, Joachim
    Baier, Christel
    Chrszon, Philipp
    Daum, Marcus
    Dubslaff, Clemens
    Kluppelholz, Sascha
    Maercker, Steffen
    Mueller, David
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2018, 20 (02) : 179 - 194
  • [5] Interpolants and symbolic model checking
    McMillan, K. L.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2007, 4349 : 89 - 90
  • [6] Symbolic model checking APSL
    Liu, Wanwei
    Wang, Ji
    Chen, Huowang
    Ma, Xiaodong
    Wang, Zhaofei
    FRONTIERS OF COMPUTER SCIENCE IN CHINA, 2009, 3 (01): : 130 - 141
  • [7] On partitioning and symbolic model checking
    Iyer, S
    Sahoo, D
    Emerson, EA
    Jain, J
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2005, 25 (05) : 780 - 788
  • [8] Symbolic model checking APSL
    Liu, Wanwei
    Wang, Ji
    Chen, Huowang
    Ma, Xiaodong
    TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 39 - 46
  • [9] On partitioning and symbolic model checking
    Iyer, S
    Sahoo, D
    Emerson, EA
    Jain, J
    FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 497 - 511
  • [10] Lazy symbolic model checking
    Yang, J
    Tiemeyer, A
    37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 35 - 38
12345