Designed with high productivity workflows, the JasperGold® Sequential Equivalency Checking (SEC) App is a formal verification product that inputs two register-transfer level (RTL) files and verifies their sequential behavioral equivalence. The app delivers up to 10X faster runtimes compared to using regular formal tools.
There are many cases when you’ll need to verify the sequential equivalency of two different RTL circuit descriptions. For example:
Confirming that low-power optimizations 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 by definition, 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 / functional mismatches.
Unlike attempting to use simulation-based approaches or adapting regular formal tools for this type of verification, JasperGold Sequential Equivalence Checking 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 determine, with mathematical certainty, that two designs expressed in RTL exhibit the exact same behavior at sequential design points
Dedicated input wizard and debug GUI
Special optimized engine for sequential equivalence checking that runs 2-10X faster vs. regular formal tools
Ability to handle prickly multi-value logic cases, such as non-resettable flops, Verilog ‘X’ values, dangling signals, etc.