- Equivalence checking between RTL and circuit schematics is difficult
for some circuits (e.g., custom arrays
- Critical timing and self-timed control logic components
- Large number of bit-cells
- Inherently complex sequential logic blocks
- Dynamic Logic
- Traditional tools fail on such circuits
- Very large state space and too many initial state/input
sequence combinations for simulation-based tools
- Boolean equivalence tools can only check static cones of logic,
and do not capture dynamic behavior
|