The Many Flavors of Equivalence Checking: Part 1, Synthesis Validation with LEC and SLEC (a/k/a the Most Popular Formal Apps Ever)

In EDA, the word “simulation” is used everywhere: there is RTL and gate level simulation, analog simulation, RF simulation, and even simulators for the flow of materials across a factory floor. One term, accurately describing very different tools that are optimized for a plethora specific jobs. Similarly, “logic equivalence checking” (LEC) also applies to a number of tools that cover a wide variety of high-value verification tasks. Even experienced engineers can get tripped up in mapping equivalency checking requirements to the corresponding tool and work flow, hence this series of posts to enumerate what is out there. Let’s begin with the most popular, original use case of equivalence checking technology: logic synthesis validation.

RTL Logic Synthesis Validation

First, the earth cooled. Then the dinosaurs came. Then around the time ARPANET became the “World Wide Web”, logic designers were starting to trade schematic capture digital design creation work flows for programmatic synthesis of Hardware Description Languages (HDLs) like Verilog and VHDL. As impressive as this technology was, naturally engineers were concerned that their newfangled synthesis tools were faithfully re-creating their HDL designs into gate-level netlists (which, in-turn, were fed into the back-end implementation tools like they used to do themselves with their netlisted schematics.)

Initially, the comparison/validation of the “golden” HDL’s behavior vs. the synthesized gate-level circuitry was done by re-running the test bench created for the HDL DUT on the gate-level implementation. Unfortunately, as they say in the mathematics world, successful passage of all the tests is only a “necessary but not sufficient” criterion as the testbench is just not exhaustive. Plus, then-as-now, gate level simulations can take forever. Given the time constraints of most projects it is virtually impossible to run the full suite of HDL-level tests on the gate-level version of the design.

Consequently, these twin challenges inspired the creation of new class of tools that employ static, mathematical analysis techniques – i.e. automated formal verification – to exhaustively compare the behavior of the HDL and gate-level design descriptions for all inputs and all time, and do this significantly faster than brute-force comparison of simulation results.

Applying this to a synthesis validation flow gives rise to the following characteristics of any LEC tool: the tool shall report an error if the “Specification” (the HDL level DUT) and the “Implementation” (the synthesized gate-level DUT) (A) do not have the exact same logic behavior, and (B) have a different number of states (i.e. it’s still an error if the correct data appears just clock cycle earlier or later in the Implementation circuit’s outputs). If either these issues  are detected, it calls into question the effectiveness of the synthesis tool itself (but 99% of the time the unwanted differences are due to errors or ambiguities in the input constraints given to the synthesis tool by the designer.)

This might seem excessively strict, but recall that the goal of the RTL synthesis validation flow is to exhaustively prove that the gate-level netlist exactly mimics the HDL circuit’s behavior. Similarly, there are also times when engineers need to validate that one gate-level netlist behaves identically to another. For example, another popular application of LEC is to validate HDL language translations – e.g. the re-coding of a VHDL design into Verilog or vice –versa. As with the synthesis validation case, you want a perfect match of behaviors at the outputs between the two code bases. Mentor’s FormalPro-LEC tool is a high performance, scalable, mature solution for these use cases.

One important point of clarification here is that it is ok if the states in the interior of the designs being compared are ordered differently – flip-flops are ahead or behind clusters of combinatorial logic, the FSMs are encoded a little differently, etc. The critical criterion for a successful LEC run is that the two designs’ behaviors are perfectly the same at the outputs – i.e. measured at the perimeters they have exactly the same number of states.

In general, LEC is truly a verification-specific flow in that it is employed when your design is essentially finalized, and you really don’t want to see any behavioral mismatches between the golden Specification code and the Implementation code at all. As such, the language translation case is almost an exception that proves the rule, as LEC’s focus is mainly on validating the output of machine generated code from logic synthesis or routing.

High-Level Synthesis (HLS) Validation

In the more recent past, logic synthesis technology has advanced to the point where traditionally “pure software” languages like C and C++ — or their hardware-styled sub-sets like SystemC — can be synthesized directly into RTL code.  As with the RTL-to-gate-level synthesis work flow, HLS users (A) want to make sure the synthesis tool did its job perfectly, (B) also want to confirm they did their jobs perfectly by specifying the correct design constraints.

The twist in this use case is that a C/C++ Specification does not have any explicit clocks at all; and SystemC Specification code is often timed or clocked in a very basic manner separating threads/registers/states, with possibly no intra-circuit timing specified (because you don’t want to “write RTL in SystemC”). Hence, it is impossible to expect the more concrete RTL Implementation code created by the HLS tool to have exactly the same number of states as the Specification given the HLS algorithms will inevitably have to insert registers (i.e. extra states) to preserve data to meet clocking constraints imposed by the physical world. Consequently, the requirements for a LEC analysis must necessarily expand to accommodate the case where the number of states in the golden Specification and the Implementation are different, but in the end the Implementation code outputs the same data (potentially arriving a little earlier or later).

This is where Sequential Logic Equivalence Checking (SLEC) algorithms come into play. Like their LEC cousins, under-the-hood SLEC tools do an exhaustive mathematical comparison (i.e. an exhaustive formal analysis) of the C/C++/SystemC Specification and Verilog or VHDL Implementation. However, a SLEC analysis allows for the number of states to differ between the two, as long as the ultimate output data/signals are the same in the RTL as they were at the C-level. The Mentor SLEC-HLS tool is an exemplar of this technology; and when used in-tandem with the Catapult synthesizer it can make quick work of DSP-style circuits like video codecs, or can significantly pull-in the schedule of processor and GPU projects by enabling engineers to use faster C++ design and verification flows before going into a RTL implementation.

But Wait, There’s More …
Synthesis validation is but one application of this powerful formal-based technology. In Part 2 and beyond, I’ll describe how SLEC-based analysis can rapidly verify ECOs and bug fixes, low power clock gating control logic and other dynamic power optimizations, re-pipelining, a DUT’s resilience in the face of single-event upsets and faults, and more.

Until then, may the Equivalence be with you,

Joe Hupcey III,
for the Questa Formal team