Sequential equivalence checking between RTL design revisions
During a typical development process, there are many occasions where a change needs to be made to a block, which must then be retested to ensure functional equivalence. For example, once a block has been proven to operate correctly, a designer may wish to optimize some section, maybe to improve the coding style, reduce the gate count or streamline operation. Today, an engineer must execute an entire simulation regression run to verify each change. This often requires a lot of time and may also need additional stimulus, with no possibility that an exhaustive functional check will be performed.
OneSpin 360 EC-RTL is an easy to use Sequential Equivalency Checking tool that ensures functional equivalence between RTL design revisions.
Sequential Equivalence Checking with EC-RTL
A fast comparison of two RTL blocks ensures that they represent the same functionality, which has many useful purposes. For example, optimizing code for power, or re-encoding a finite state machine for functional safety should not change the design functionality. To verify such changes, 360 EC-RTL uses the full formal platform to examine the functionality of a set of registers and logic regardless of the different relationship between the elements between two design representations.
Why is it different than Combinational EC?
Equivalency Checking is already used to test RTL versus gate representations of a design for sign-off purposes, and it seems a natural fit to use the same basic technique for RTL to RTL checking. However, there is an issue at this level, which typically does not occur in ASIC synthesis, and that is the changing of clocked register elements and the movement of functional sections of a design versus these registers.
For ASIC synthesis, in general the synthesis tool converts register elements to flips flops and the combinational logic between these register elements is maintained as gates. EC tools that compare pre and post synthesis representations create a mapping between register elements and flips flops, and then compares the combinational logic functionality in between. This method breaks down if the registers are changed between the representations, or moved relative to the combinational logic functional units.
In contrast, 360 EC-RTL’s sequential equivalence checking examines the functionality of a set of registers and logic regardless of the different relationship between the elements between two design representations. By comparing the overall functional relationship, the technology is able to exhaustively compare two descriptions for common functionality, pinpointing differences if they occur.
360 EC-RTL is a comprehensive RTL to RTL Equivalence Checking tool that efficiently compares designs and either formally proves that they operate the same under all conditions, or demonstrates issues where the functionality is different. In the latter case, the differences are revealed in a waveform and text display with a generated witness to show the behavior of the two designs.
With OneSpin 360 EC-RTL, designers are now able to perform fast comparisons of designs that they modify or optimize and avoid long repetitious simulation runs. This can save hours of verification time often at crucial moments in the development process. This also provides an exhaustive proof of equivalence that is impossible to achieve with simulation.