Efficient translation of Boolean formulas to CNF in formal verification of microprocessors

扫码查看

原文链接

NETL

外文摘要：We present a method for translating Boolean formulas to CNF by identifying gates with fanout count of 1， and merging them with their fanout gate to generate a single set of equivalent CNF clauses。 This eliminates the intermediate CNF variable for the output of the first gate， and reduces the number of CNF clauses， compared to the conventional translation to CNF， where each gate is assigned an output variable and is represented with a separate set of CNF clauses。 Chains of nested ITE operators， where each ITE is used only as else-argument of the next ITE， are similarly merged and represented with a single set of clauses without intermediate variables。 This method was applied to Boolean formulas from formal verification of microprocessors。 The formulas require up to hundreds of thousands of variables and millions of clauses， when translated to CNF with the conventional approach。 The best translation reduced the CNF variables by up to 2/spl times/ the SAT-solver decisions by up to 5/spl times/ the SAT-solver conflicts by up to 6/spl times/ and accelerated the SAT checking by up to 7。6/spl times/ for unsatisfiable formulas， and 136/spl times/ for satisfiable ones。

外文关键词：

formal verificationlogic CADmicroprocessor chipsBoolean functionslogic gatesBoolean formulasformal verificationequivalent CNF clausesnested ITE operatorsSAT-solver

作者：

M.N. Velev

展开 >

作者单位：

Dept. of Electr. & Comput. Eng., Carnegie Mellon Univ., Pittsburgh, PA, USA

会议母体文献：

Design Automation Conference, 2004. Proceedings of the ASP-DAC 2004. Asia and South Pacific

页码：

p.310-315

出版时间：

2004