Equivalence Checking

  • Most common technique of formal verification used in industry today
  • Typically, the gate-level implementation is compared with the representation at a higher level (RTL)
  • A canonical representation allows easy comparison of two functions
    • representation should be efficient in memory and time
    • problem of checking Boolean Equivalence is NP-complete
  • Commercial tools available from most tool vendors
  • Limitation is that some functions (such as multipliers) require exponential space for the representation