Sciweavers

Share
TCAD
2002

Robust Boolean reasoning for equivalence checking and functional property verification

9 years 11 months ago
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...
Andreas Kuehlmann, Viresh Paruthi, Florian Krohm,
Added 23 Dec 2010
Updated 23 Dec 2010
Type Journal
Year 2002
Where TCAD
Authors Andreas Kuehlmann, Viresh Paruthi, Florian Krohm, Malay K. Ganai
Comments (0)
books