Jasper SEC App

Designed with high-productivity workflows, the Cadence^® Jasper^™ Sequential Equivalence Checking (SEC) App is a formal verification product that inputs two register-transfer level (RTL) models and verifies their sequential behavioral equivalence. The app delivers superior results for the equivalence problem when compared with other conventional formal tools.

There are many cases when you need to verify the sequential equivalency of two different RTL circuit descriptions. For example:

• Confirming that dynamic power optimizations (such as clock gating) were inserted correctly
• Verifying that an algorithmic change or performance optimization in the RTL didn't break the desired functionality
• Validating an engineering change order (ECO)

Simulation-based RTL equivalency checking approaches—where the results of "golden tests" are compared to the runs with the new circuit—assume the golden test suite exercises all functional corner cases. Of course, simulation is not exhaustive, so even the most carefully constructed RTL simulation regression suite will fall short at this task. The risk is exacerbated when the circuit(s) implement clock-gating schemes, since clock gating is notorious for its ability to conceal corner-case bugs and functional mismatches.

Unlike attempting to use simulation-based approaches or adapting regular formal tools for this type of verification, the Jasper SEC App provides a special formal engine optimized for exhaustively verifying SEC problems. The app also has a customized GUI specially structured to highlight functional differences discovered between the specification and implementation RTL.

Key Features

• Ability to prove that two designs expressed in RTL exhibit the exact same behavior at sequential design points
• Dedicated input wizard and debug GUI
• Special optimized engines for SEC that exhibit superior performance compared with other conventional formal tools