Robust Boolean reasoning for equivalence checking and functional property verification

Many tasks in CAD, such as equivalence checking, property checking, logic synthesis, and false paths analysis require efficient Boolean reasoning for problems derived from circuits. Traditionally, canonical representations, e.g., BDDs, or structural SAT methods, are used to solve different problem instances. Each of these techniques offer specific strengths that make them efficient for particular problem structures. However, neither structural techniques based on SAT, nor functional methods using BDDs offer an overall robust reasoning mechanism that works reliably for a broad set of applications. In this paper we present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, a SAT procedure, and random simulation natively working on a shared graph representation of the problem. The described intertwined integration of the four techniques results in a powerful summation of their orthogonal strengths. The presented reasoning technique was mainly deve...

• Type: Journal
• Year: 2002
• Where: TCAD
• Authors: Andreas Kuehlmann, Viresh Paruthi, Florian Krohm, Malay K. Ganai
• Keywords: Boolean Reasoning, Efficient Boolean Reasoning, Structural Sat Methods, TCAD 2002