Circuit-based Boolean Reasoning
Andreas Kuehlmann, Malay Ganai, Viresh Paruthi · 2001
Many tasks in CAD, such as equivalence checking, property checking, logic synthesis, and false paths analysis require efficient Boolean reasoning for problems derived from circuit structures. Traditionally, canonical representations, e. g., BDDs, or SAT- based search methods are used to solve a particular class of problems. In this paper we present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, and a SAT procedure natively working on a shared graph representation of the problem. The described intertwined integration of the three techniques results in a robust summation of their orthogonal strengths. Our experiments demonstrate the effectiveness of the approach.