Symbolic Simulation

  • 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