Questa SLEC

The Questa SLEC app uses formal analysis to exhaustively compare two blocks of RTL code, identifying any differences in the output behavior of the two designs for all inputs, and for all time.

Automated and exhaustive formal analysis

Quite a few high-value verification tasks involve the comparison of a circuit to a close equivalent that’s been modified in a small, yet operationally critical way. For example, sometimes new logic is required to reduce dynamic power consumption, an ECO is needed at the last minute, or the impact of stuck-at or transient faults must be evaluated. While each of these tasks can be addressed with RTL simulation, doing so can take weeks — even months — of testbench development and simulation debug. Even worse, the results from even the most well-designed constrained-random simulation environment will not be exhaustive, leaving the door open for functional bugs that were unintentionally created by the added logic.

The asynchronous reset domain crossings (RDC) that arise create metastability and signal reconvergence issues in the reset signaling networks — similar to the failures seen in asynchronous clock domain crossings (CDC). Just as with CDC phenomena, the metastability
induced by these asynchronous RDCs cannot be modeled or exhaustively covered by digital simulation, leaving designers open to the considerable risk of unpredictable chip behavior when samples come back from the fab, or worse, in the field.

Automated sequential logic equivalence checking

A sequential logical equivalence check (SLEC) formally verifies that two sequentially different designs are functionally equivalent. The Questa® SLEC app performs an exhaustive, formal-based analysis of two RTL designs in only a few hours — even minutes — depending on the design sizes and parameters. This frees the user from having to manually create and maintain
testbenches and re-run massive, time and resource intensive simulation regression suites.