Sequential logic equivalence checking (SLEC) is effective in finding bugs in new logic required to reduce dynamic power consumption, validating last minute ECOs, or verifying that design optimizations aren’t too aggressive. It is also very efficient in verifying safety mechanisms used in ISO 26262 and other fault mitigating designs. SLEC’s effectiveness comes from using exhaustive formal verification algorithms, which do not require a testbench; and indeed are completely automated so the user does not need to know about formal technology themselves. Given the formal-based nature of the analysis, SLEC can prove functional equivalence of the two designs for all inputs and all time, or identify any differences between the two designs. In contrast, simulation-based approaches cannot prove sequential equivalence. Indeed, even with well-written constrained-random testbenches, simulation may find functional differences depending on the quality of the testbenches but such analysis could still miss critical corner cases. As such, SLEC can save a lot of resimulation time after small modifications of the design.
In this course, you will be introduced to the concept of sequential logic equivalence checking and its common applications. You will also learn how to start with Questa® SLEC to verify design optimization, bug fix/ECOs, low power clock gating logic, and safety mechanisms.
