00000cab a22000003a 4500 UP-99796217609500559 Buklod 20231007234342.0 m |o d | ta 101013s xx d | ||r ||||| || DENGII eng Kuehlmann, A. Robust Boolean reasoning for equivalence checking and functional property verification. pp. 1377-1394 Many tasks in computer-aided design (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., binary decision diagrams (BDDs), or structural satisfiability (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. The authors present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, an 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 developed for formal equivalence checking and property verification but can equally be used in other CAD applications. The authors' experiments demonstrate the effectiveness of the approach for a broad set of applications. Boolean reasoning. Binary decision diagram. Computer-aided design. Equivalence checking. False path analysis. Functional property verification. Logic synthesis. Orthogonal strength. Random simulation. Shared graph. Structural satisfiability. Structural transformation. IEEE Transactions on computer-aided design of integrated circuits and systems 21, 12 (2002). FO UPD DENG-II Article