{"id":14407,"date":"2020-07-13T10:16:38","date_gmt":"2020-07-13T17:16:38","guid":{"rendered":"https:\/\/blogs.mentor.com\/verificationhorizons\/?p=14407"},"modified":"2026-03-27T08:48:37","modified_gmt":"2026-03-27T12:48:37","slug":"the-many-flavors-of-equivalence-checking-part-5-summary-of-the-most-popular-lec-and-slec-use-cases","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2020\/07\/13\/the-many-flavors-of-equivalence-checking-part-5-summary-of-the-most-popular-lec-and-slec-use-cases\/","title":{"rendered":"The Many Flavors of Equivalence Checking: Part 5, Summary of the Most Popular LEC and SLEC Use Cases"},"content":{"rendered":"

\"\"<\/a>As I noted at the beginning of this series, the term \u201clogic equivalence checking\u201d (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 \u2013 without having to learn formal itself \u2013 so you can focus on the bigger picture.<\/p>\n

———-<\/p>\n

Task:<\/strong> RTL synthesis validation — exhaustively prove that the gate-level netlist exactly<\/u> mimics the HDL circuit\u2019s behavior<\/p>\n

Tool(s):<\/strong> Mentor’s FormalPro Logic Equivalence Checking (LEC) tool<\/a><\/p>\n

Detailed Post:<\/strong> Part 1 of this series: Synthesis Validation with LEC and SLEC (a\/k\/a the Most Popular Formal Apps Ever)<\/a>,<\/p>\n

Reminder<\/strong>: The critical criterion for a successful LEC run is that the two designs\u2019 behaviors are perfectly the same at the outputs \u2013 i.e. measured at the perimeters they have exactly the same number of states and signaling behaviors.<\/p>\n

———-<\/p>\n

Task:<\/strong> High-level synthesis validation — exhaustively prove the equivalence of the RTL generated by high-level synthesis tool to the original C\/C++\/SystemC code<\/p>\n

Tool(s):<\/strong> Mentor SLEC-HLS<\/a><\/p>\n

Detailed Post & Links: <\/strong>Part 1: Synthesis Validation with LEC and SLEC<\/a>, Google case study<\/a>, NVIDIA case study<\/a><\/p>\n

Reminder<\/strong>: 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<\/u> 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.<\/p>\n

———-<\/p>\n

Task:<\/strong> RTL ECO and bug fix verification<\/p>\n

Tool(s):<\/strong> Questa SLEC<\/a><\/p>\n

Detailed Post & Links:<\/strong> Part 2: How SLEC Brings Automated, Exhaustive Formal Analysis to ECO\/Bug Fix Verification<\/a><\/p>\n

Reminder<\/strong>: The automated, exhaustive formal algorithms will find behavioral differences appearing at the outputs of the \u201cunfixed\u201d vs. the \u201cfixed\u201d 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 \u2013 implicitly confirming you didn\u2019t 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 \u2013 more aggressive clock gating, etc.<\/p>\n

———-<\/p>\n

Task:<\/strong> Verifying low power clock gating logic (e.g. verifying your \u201cchicken bits\u201d work)<\/p>\n

Tool(s): <\/strong>Questa SLEC<\/a><\/p>\n

Detailed Post & Links:<\/strong> Part 3: How SLEC Brings Automated, Exhaustive Formal Analysis to Low Power Clock Gating Verification<\/a>, Erik Seligman, Tom Schubert, M V Achutha Kiran Kumar, Formal Verification, An Essential Toolkit for Modern VLSI Design<\/em>. \u00a9 2015 Elsevier \u2013 MK, pp. 236-237<\/a><\/p>\n

Reminder:<\/strong> 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 \u201cSpecification\u201d and \u201cImplementation\u201d code are clearly a bad thing and need to be fixed ASAP.<\/p>\n

———-<\/p>\n

Task:<\/strong> Safety mechanism verification<\/p>\n

Tool(s): <\/strong>Questa SLEC<\/a><\/p>\n

Detailed Post & Links:<\/strong> Part 4: How SLEC Brings Automated, Exhaustive Formal Analysis to Safety Mechanism Verification<\/a><\/p>\n

Reminder:<\/strong> 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\u2019t have to spend any time writing a testbench!<\/p>\n

———-<\/p>\n

Task:<\/strong> Verification of the recoding of VHDL design into to Verilog (or vice-versa)<\/p>\n

Tool(s):<\/strong> Mentor’s FormalPro Logic Equivalence Checking (LEC) tool<\/a> or Questa SLEC<\/a><\/p>\n

Detailed Post & Links:<\/strong> Verification Horizons: \u201cUsing Questa\u00ae SLEC to Speed Up Verification of Multiple HDL Outputs<\/em>\u201d<\/a><\/p>\n

Reminder<\/strong>: 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 \u201cnew\u201d IP, the SLEC flow can be used.<\/p>\n

———-<\/p>\n

Task:<\/strong> Design Optimization \u2013 e.g. recoding a DUT for less latency, or reducing logic to save area<\/p>\n

Tool(s):<\/strong> Questa SLEC<\/a><\/p>\n

Detailed Post & Links:<\/strong> Verification Academy, SLEC for Design Optimization<\/a><\/p>\n

Reminder<\/strong>: Truly this is a use case where a formal-based approach with SLEC really shines \u2013 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.<\/p>\n

———-<\/p>\n

Summary<\/strong><\/p>\n

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!<\/p>\n

Until next time, may your power consumption be low, and your throughput be high!<\/p>\n

Joe Hupcey III,
\nfor the Questa Formal team<\/p>\n

Reference Links:<\/strong><\/p>\n

Part 1 of this series: Synthesis Validation with LEC and SLEC<\/strong> (a\/k\/a the Most Popular Formal Apps Ever)<\/a><\/p>\n

Part 2: How SLEC Brings Automated, Exhaustive Formal Analysis to ECO\/Bug Fix Verification<\/strong><\/a><\/p>\n

Part 3: How SLEC Brings Automated, Exhaustive Formal Analysis to Low Power Clock Gating Verification<\/strong><\/a><\/p>\n

Part 4: How SLEC Brings Automated, Exhaustive Formal Analysis to Safety Mechanism Verification<\/strong><\/a><\/p>\n","protected":false},"excerpt":{"rendered":"

As I noted at the beginning of this series, the term \u201clogic equivalence checking\u201d (LEC) applies to a number of…<\/p>\n","protected":false},"author":71594,"featured_media":15373,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"spanish_translation":"","french_translation":"","german_translation":"","italian_translation":"","polish_translation":"","japanese_translation":"","chinese_translation":"","footnotes":""},"categories":[1001,1,10],"tags":[465,486,488,495,574,670,710,720],"industry":[],"product":[],"coauthors":[931],"class_list":["post-14407","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-equivalence-checking","category-news","category-tips-tricks","tag-equivalence-checking","tag-formal","tag-formal-apps","tag-formalpro","tag-lec","tag-questa-slec","tag-sequential-logic-equivalency-checking","tag-slec"],"featured_image_url":"https:\/\/blogs.sw.siemens.com\/wp-content\/uploads\/sites\/54\/2020\/07\/apples-to-apples.jpg","_links":{"self":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14407","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/users\/71594"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/comments?post=14407"}],"version-history":[{"count":5,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14407\/revisions"}],"predecessor-version":[{"id":16937,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14407\/revisions\/16937"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media\/15373"}],"wp:attachment":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media?parent=14407"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/categories?post=14407"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/tags?post=14407"},{"taxonomy":"industry","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/industry?post=14407"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/product?post=14407"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/coauthors?post=14407"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}