Formal equivalence verifiers for combinational circuits rely heavily on BDD algorithms. However, building monolithic BDDs is often not feasible for today's complex circuits. Thus, to increase the effectiveness of BDD-based comparisons, divide-and-conquer strategies based on cut-points are applied. Unfortunately, these algorithms may produce false negatives. Significant effort must then be spent for determining whether the failures are indeed real. In particular, if the design is actually incorrect, many cut-point based algorithms perform very poorly. In this paper we present a new algorithm that completely removes the problem of false negatives by introducing normalized functions instead of free variables at cut points. In addition, this approach handles the propagation of input assumptions to cut-points, is significantly more accurate in finding cut-points, and leads to more efficient counter-example generation for incorrect circuits. Although, naively, our algorithm would appear to be more expensive than traditional cut-point techniques, the empirical data on more than 900 complex signals from a recent microprocessor design, shows rather the opposite.
展开▼
