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

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× the SAT-solver decisions by up to 5× the SAT-solver conflicts by up to 6× and accelerated the SAT checking by up to 7.6× for unsatisfiable formulas, and 136× for satisfiable ones.