Original URL: https://www.linkedin.com/pulse/navigating-abort-points-logic-equivalence-checking-heidi-zheng-9fq2c

Abort points are frequently encountered in Logic Equivalence Checking. LEC tools, which may run for extended periods, might eventually cease operation, leading to an unsuccessful result. Considering the months invested in the IC design flow, the question arises: should the process restart, resulting in the loss of all previous efforts, or should alternative methods be explored to address the issue?

Addressing the issue provides several viable options.

The initial approach involves leveraging random simulation. The detailed process entails extracting the aborted logic cone from the netlist and saving it as a Verilog netlist file. In cases involving RTL to netlist, the associated RTL portion is extracted and saved as a Verilog RTL file. Subsequently, a test bench is created to instantiate both small modules, and numerous random simulations are executed to compare the output of the two modules. After thousands of successful comparisons, increased confidence in the equivalence of the aborts is achieved.
The second method advocates running Logic Equivalence Checking on the two modules extracted as described above. LEC tools tend to exhibit better performance when dealing with smaller-sized designs.

A third option involves replacing the logic cone associated with the abort points or the module containing the abort points. In this scenario, a new synthesis is conducted on the module with the abort points, with verification set as a high priority. For example, in Design Compiler, the synthesis in the module at issue can be configured with the verification priority set to high (Command: set_verification_priority -high)

Centering on the third option outlined earlier, GOF ECO offers two approaches for replacing abort points. The initial method involves furnishing APIs to substitute the entire newly synthesized module, a process elaborated on in this LinkedIn article.

The second approach involves replacing all the abort points. As illustrated in Figure 3, the logic cone steering the abort flops can be substituted with another newly synthesized logic cone, which proves to be more amenable to Logic Equivalence Checking.

Below is the script for performing the replacement of abort points.

read_library("tsmc.lib");
read_design("-ref", "new_syn.gv");
read_design('-imp', "original_netlist.gv");
set_top("spi2gram");
set_top_ref("spi2gram");
fix_logic("beat_cnt_reg_0_/D", "beat_cnt_reg_1_/D", "beat_cnt_reg_2_/D", "-force");
report_eco;
set_top('the_top_module');
write_verilog("eco_netlist.gv");  

As the two methodologies offered by GOF—module replacement and abort points replacement—are localized rather than global replacements, there is a potential risk that certain boundary optimization information may not be captured. This could result in LEC failures on the new ECO netlist. The debugging process is simplified through GOF's provided debug method, detailed in the article on Non-Equivalence Debug Through Pattern Back-Annotation available on LinkedIn.

GOF platform integrates four functional components: ECO, Formal, LEC and Debug. To access detailed information about GOF, please visit the website https://nandigits.com