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