The Many Flavors of Equivalence Checking: Part 5, Summary of the Most Popular LEC and SLEC Use Cases
As I noted at the beginning of this series, the term “logic equivalence checking” (LEC) applies to a number of very different 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 the below summary drawn from this series for you to quickly reference when these need(s) arise. The common thread in all these flows: the employment of an automated, exhaustive formal analysis – without having to learn formal itself – so you can focus on the bigger picture.
———-
Task: RTL synthesis validation — exhaustively prove that the gate-level netlist exactly mimics the HDL circuit’s behavior
Tool(s): Mentor’s FormalPro Logic Equivalence Checking (LEC) tool
Detailed Post: Part 1 of this series: Synthesis Validation with LEC and SLEC (a/k/a the Most Popular Formal Apps Ever),
Reminder: 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 and signaling behaviors.
———-
Task: High-level synthesis validation — exhaustively prove the equivalence of the RTL generated by high-level synthesis tool to the original C/C++/SystemC code
Tool(s): Mentor SLEC-HLS
Detailed Post & Links: Part 1: Synthesis Validation with LEC and SLEC, Google case study, NVIDIA case study
Reminder: 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. 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 Sequential Logic Equivalence Checking (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.
———-
Task: RTL ECO and bug fix verification
Tool(s): Questa SLEC
Detailed Post & Links: Part 2: How SLEC Brings Automated, Exhaustive Formal Analysis to ECO/Bug Fix Verification
Reminder: The automated, exhaustive formal algorithms will find behavioral differences appearing at the outputs of the “unfixed” vs. the “fixed” designs. Unless your change is really small, a best practice here is to insert enabling logic ahead of the ECO where you run the analysis with the ECO disabled so you can check that backward compatibility between the old and new DUT is maintained – implicitly confirming you didn’t break anything when you slotted in the ECO/bug fix. Of course, there are also cases where an ECO is actually NOT supposed to change the DUT behavior at all – more aggressive clock gating, etc.
———-
Task: Verifying low power clock gating logic (e.g. verifying your “chicken bits” work)
Tool(s): Questa SLEC
Detailed Post & Links: Part 3: How SLEC Brings Automated, Exhaustive Formal Analysis to Low Power Clock Gating Verification, Erik Seligman, Tom Schubert, M V Achutha Kiran Kumar, Formal Verification, An Essential Toolkit for Modern VLSI Design. © 2015 Elsevier – MK, pp. 236-237
Reminder: A DUT without any chicken bit logic should perform identically to a DUT WITH chicken bit logic that is not activated. Hence, as with the logic synthesis validation flow, by definition any differences detected between the “Specification” and “Implementation” code are clearly a bad thing and need to be fixed ASAP.
———-
Task: Safety mechanism verification
Tool(s): Questa SLEC
Detailed Post & Links: Part 4: How SLEC Brings Automated, Exhaustive Formal Analysis to Safety Mechanism Verification
Reminder: If any difference in behavior is detected between the regular DUT and the safety mechanism logic with NO faults, and that same IP but WITH faults added, it means there is a flaw in the safety mechanism logic to mitigate the injected fault(s). The good news is that this analysis runs significantly faster than other approaches AND you don’t have to spend any time writing a testbench!
———-
Task: Verification of the recoding of VHDL design into to Verilog (or vice-versa)
Tool(s): Mentor’s FormalPro Logic Equivalence Checking (LEC) tool or Questa SLEC
Detailed Post & Links: Verification Horizons: “Using Questa® SLEC to Speed Up Verification of Multiple HDL Outputs”
Reminder: If the translated IP needs to strictly mimic the original IP in every way, use the LEC flow. But if it is OK for the timing of the output signals to be a little different in the “new” IP, the SLEC flow can be used.
———-
Task: Design Optimization – e.g. recoding a DUT for less latency, or reducing logic to save area
Tool(s): Questa SLEC
Detailed Post & Links: Verification Academy, SLEC for Design Optimization
Reminder: Truly this is a use case where a formal-based approach with SLEC really shines – you could spend weeks re-simulating the optimized design and get all the tests to pass, but you still might not find an unintended corner case introduced by the optimizations. SLEC will find all discrepancies right away.
———-
Summary
I trust this series of posts have helped you understand the many ways this automated, exhaustive technology can be applied to high-value verification challenges you have today; and has inspired you to invent your own flows!
Until next time, may your power consumption be low, and your throughput be high!
Joe Hupcey III,
for the Questa Formal team
Reference Links:
Part 2: How SLEC Brings Automated, Exhaustive Formal Analysis to ECO/Bug Fix Verification
Part 3: How SLEC Brings Automated, Exhaustive Formal Analysis to Low Power Clock Gating Verification
Part 4: How SLEC Brings Automated, Exhaustive Formal Analysis to Safety Mechanism Verification
