Equivalence Checking

            Equivalence Checking RTL vs RTL) would be the use of equivalence checkers which were traditionally oriented towards combinational equivalence checking but have some sequential capabilities. The advantage is that these tools are well known to designers and are fairly mature. However, the tools are still primarily oriented towards verifying the output of a synthesis tool. These tools are able to deal with some changes in state encoding, allowing a synthesis tool to perform some retiming operations. However, the debug environment is not ideally suited to RTL designers: The user is presented with a schematic displaying gate-level differences between the two designs, without benefit of a waveform or stimulus.

It is common to divide formal verification into equivalence checking and property checking. The latter category includes both assertion-based verification and automated formal solutions such as apps. A simple way to conceptually unify these two categories is to think of equivalence checking as ABV on a model containing both designs to be compared as well as a set of assertions specifying that the outputs of the two designs must match. This does not necessarily represent how actual tools are build, but it may help in understanding.

Nothing can replace formal analysis. Simulation acceleration uses hardware to run faster, so it will execute more tests in a given time, but it still exercises very little design behavior. In-circuit emulation (ICE) and prototypes built using FPGAs are typically designed to be plugged into the end system in lieu of the actual chip under design. They may run even faster than acceleration and will exercise different aspects of the design. While ICE and prototypes are valuable for hardware-software co-verification, they are in no way a substitute for the exhaustive nature of formal verification.

It is no longer sufficient for FPGA designers to defer verification to the bring-up lab. Modern FPGAs are complex system-on-chip (SoC) devices with all the complexity of their ASIC counterparts. The difficulty of lab debug and long reprogramming cycles mandate that FPGA teams adopt ASIC-like verification processes. Formal verification tools work equally well on both technologies and have been adopted on many FPGA projects.

Equivalence checking is arguably even more important for FPGAs than for ASICs. The FPGA synthesis and place-and-route processes often make significant changes to the design structure, including moving logic across register stages, in order to maximize use of the underlying chip technology. These manipulations present some risk of altering design functionality. Formal equivalence checking can catch any such problems, but sequential equivalence checking is required since there is no 1-to-1 mapping between state elements in the RTL source and the optimized netlist.

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.