Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
复制标题
DOI：
10.1109/tc.2010.74
复制
发表时间：
2010-07-01
影响因子：
3.7
通讯作者：
Benedetti, Marco
中科院分区：
文献类型：
--
作者：
Mangassarian, Hratch;Veneris, Andreas;Benedetti, Marco
正式的CAD工具在描述VLSI设计的顺序行为的数学模型上运行。随着现代数字硬件设计的规模和状态空间的不断增长，这种数学模型的简洁性对于扩展这些工具的可扩展性至关重要，只要压缩不是以降低性能为代价。量化的布尔公式满意度（QBF）是对布尔可满足性（SAT）的有力概括。它也属于与处理顺序电路的许多CAD问题相同的复杂性类别，这使其成为编码此类问题的自然候选人。这项工作提出了用于建模顺序电路行为的简洁QBF编码。编码是参数化的，并使用时间框架窗口实现进一步的压缩。全面的硬件结构用于说明所提出的编码。将三个值得注意的CAD问题，即界限模型检查，设计调试和顺序测试模式生成，被编码为QBF实例，以证明所提出的方法的鲁棒性和实用性。与最先进的SAT技术相比，对Opencore电路的广泛实验显示了90％的记忆降低，并显示出竞争性的跑步时间。此外，解决实例的数量增加了16％。诚然，这项工作鼓励进一步研究QBF在CAD中用于VLSI。
Formal CAD tools operate on mathematical models describing the sequential behavior of a VLSI design. With the growing size and state-space of modern digital hardware designs, the conciseness of this mathematical model is of paramount importance in extending the scalability of those tools, provided that the compression does not come at the cost of reduced performance. Quantified Boolean Formula satisfiability (QBF) is a powerful generalization of Boolean satisfiability (SAT). It also belongs to the same complexity class as many CAD problems dealing with sequential circuits, which makes it a natural candidate for encoding such problems. This work proposes a succinct QBF encoding for modeling sequential circuit behavior. The encoding is parametrized and further compression is achieved using time-frame windowing. Comprehensive hardware constructions are used to illustrate the proposed encodings. Three notable CAD problems, namely bounded model checking, design debugging and sequential test pattern generation, are encoded as QBF instances to demonstrate the robustness and practicality of the proposed approach. Extensive experiments on OpenCore circuits show memory reductions in the order of 90 percent and demonstrate competitive runtimes compared to state-of-the-art SAT techniques. Furthermore, the number of solved instances is increased by 16 percent. Admittedly, this work encourages further research in the use of QBF in CAD for VLSI.