Large-Scale Equivalence Checking and Function Correction

Chih-Jen (Jacky) Hsu
2F, No.6-5, Du Sing Rd., Hsinchu, Taiwan

## I. INTRODUCTION

Efficient equivalence checking  and functional correction  on large-scale designs are crucial technologies for handling today’s demanding design cycles. Analyzing an entire design is not always practical for large-scale designs because of their size and complexity. It is well known that partitioning the design, based on two designs’ correspondence, can significantly reduce the complexity of the analysis. In this contest, we challenge contestants to insert cut points on large designs in an effort to reduce their equivalence checking and function change problems.

Equivalence checking (EC) and functional correction are both used to analyze the Boolean difference between a design specification and its logic implementation.

Equivalence Checking

Identifying corresponding cuts is an effective method of simplifying the equivalence checking problem caused by the Boolean complexity of large-scale designs. The corresponding cuts represent points of functional correspondence between the two designs, allowing you to partition the designs into smaller sub-problems. However, finding the equivalent correspondence can be difficult when the design has gone through ODC/SDC optimization. An algorithm that can effectively determine functional correspondence, can help improve the success of large-scale equivalence checking.

Functional Correction

Identifying corresponding cuts can also help simplify functional correction and help produce better function changes. In today’s design cycle where time-to-market is paramount, late changes (specification changes or bug fixes) are implemented using an Engineering Change Order (ECO) process where the changes are patched directly into the netlist instead of generating the netlist from scratch with the new function. This process not only saves time and cost, it can help improve the size and quality of the patch. However, it can be difficult to directly analyze and fix function changes for small patches on a large-scale design. Therefore, we have to locate and isolate the function changes to not only reduce the analysis complexity but to achieve a better patch.  Effectively locating the functional changes and isolating the function difference would help ensure the success of large-scale ECOs.

The EC and ECO processes both have two netlists. To start to solve the problems in both processes, we focus on one target---isolating large designs into corresponding smaller instances---but with two different objectives. EC divides the large instances into smaller equivalent ones and cannot tolerate any non-equivalent sub-instances; ECO isolates the large instance into root-cause of changes and minimizes the non-equivalent sub-instance. In this contest, we ask participants to design an algorithm that will identify the correspondence between the optimized netlists and isolated them as smaller instances for solving both problems. We would deliver two benchmark suites and a single criteria to seek the essential core engine for resolving the industrial problems: large-scale design isolation.

Several academic studies have addressed these issues. Khasidashvili et al.   used BDD to explore the equivalent cut for helping the EC. Huang et al.   extended the Boolean matching problem on non-exact multiple candidates and also demonstrated the effectiveness of applying functional isolation in ECO. Long et al.  proposed the high-level learning for correlating the correspondence through the high-level optimization. In this contest, we formulate our industrial needs and provide the common benchmark suites for evaluating the real powerful engine for resolving the practical problems.

## II. CONTEST OBJECTIVES

The objective of this contest is to inspire research in the area of partitioning large designs into corresponding designs that are smaller and easier to analyze. Having an effective algorithm can help addresses both the equivalence checking and functional correction problems in practice.  While there are existing studies that address each issue, and some provide solutions, we look forward to finding fresh ideas and research into the combined problem. In this contest, we provide benchmark cases representative of problems we encounter in practice that can facilitate academic research and hopefully lead to long-term advances.

## III. FORMAL PROBLEM DEFINITION AND INPUT/OUTPUT FORMAT

Given two corresponding, combinational gate-level netlists, participants must insert the corresponding cuts to isolate the function, whilst minimizing cost.

Without rewriting the netlists, participants will insert their cuts and then generate the analyzed netlists. We will evaluate cost using the size of the cone traversed from matched outputs and added cuts to inputs and added cuts. There are several detailed notes listed in following paragraphs.

Figure 1 illustrates the concept and request in this contest.

 Figure 1 Illustrates the contest requirements. Given two corresponding netlists, the program should analyze the circuit and insert cuts to isolate the function for minimizing the cost. Detailed Rules

1.     The given input netlists are the flattened, combinational netlists composed of only primitive gates. The I/O pins of the given corresponding netlists are matched by pin name. The matched input pairs are treated equivalent input and matched output pairs are treated as the compared set.

2.     The added cuts should be grouped as the correlative sets and treated as the new equivalent inputs set and new equivalent compared sets for further analysis. Therefore, we request that participants embed corresponding set information as the instance name of the added cuts. Corresponding groups can accept inverted-equivalence. Therefore, the added cuts would be grouped in a set as the equivalent groups with phase consideration.

3.     We treat the matched input-pairs and grouped cuts as an equivalent boundary. Two points are equivalent when they have the same Boolean function with respect to their cone. For each compared set, including output pairs and added cut sets, it is equivalent if and only if any point in the set is equivalent to any others. Note that, if the cut set contains 1 cut point only, we treat it as non-equivalent.

4.     We rank the results using the following objective function:

a.     Generated netlists without non-equivalent compared sets rank higher than those with non-equivalent sets.

b.     The cost of the result without non-equivalent sets is compared using the cone size of gates from the compared sets (compared largest to smallest). For example, if three teams have cone sizes A: (10,8,3,3) B: (10,8,5) C: (12,1), we consider A better than B, and B better than C.

c.     The cost of the result with non-equivalent sets is the summation of the cone size from the points in the non-equivalent compared sets.

Rule a is used to avoid adding the wrong cuts while performing EC; rule b simulates the complexity for EC; rule c uses the cone size to estimate the patch size while ECO analyzes on the non-equivalent sets only.  We analyze the quality using this objective function on the generated netlists. The team with the minimal cost wins the case. Note that cuts are included when calculating the size of the cone.

Input Format

The input of each case contains two combinational flattened netlists in Verilog format, and the netlist is composed of primitive gates only. The I/O pins of these two designs are matched together by name only.

Output Format

l  The output is the processed netlists with the added cuts.

l  The single input is the module of the cut, and the single output is the cell named as “_cut”.

l  The instance name of the cut is in “cut_n_i” or “cut_n_bar_j” where:

u  n is an integer that represents the equivalent set

u  the name with “bar” postfix is the inversed-equivalence in that set

u  i and j are any sequence number

Acceptable Changes

The netlist cannot be rewritten, including the optimization, instance type, and instance name.

The only acceptable change is to reconnect the cut with gates.

In other words, if the cut is treated as a buffer, the original and revised designs should be isomorphic (including their instance names).

Program Requirements

The requested program accepts four arguments: the first two arguments are the input Verilog files, followed by the two output generated cut netlists. For example:

<program> <in_1.v> <in_2.v> <out1.v> <out2.v>

## IV. EXAMPLE

In this example, we illustrate the problem description, cost, and ranking. The inputs are shown in Figure 2. There are two netlists in Verilog format composed by primitive gates only. The I/O of these two designs are matched entirely by name.

Contestants are requested to insert the corresponding cuts and generate them in Verilog format with any rewrite.

In this example, we provide four sample outputs and illustrate the objective function and team ranking.

Input

 Design A Design B module top (a,b,c,o); input a,b,c; output o; wire d,e,f,g; and  (d,a,b); xor  (e,a,b); xor  (f,d,e); nand (g,b,c); xor  (o,f,g); `endmodule `` `` ` `module top (a,b,c,o);` input a,b,c; output o; wire d,e,f,g; and (d,a,b); xor (e,a,b); or  (f,d,e); and (g,b,c); xnor(o,f,g); `endmodule `` `` `

Figure 2. Example corresponding input files.

Team A

Team A inserts two cuts in Design A, two cuts in Design B, and one cut in Design B is in inverse-phase.

There are three compared sets, including cut_1, cut_2, and output pairs;  these three sets are equivalent. Therefore, the cost of team A would be (4,4,2,2,1,1). The maximum cone size is 4, traversed from cut_2_1 in both Design A and Design B. The cone size from o is 1, containing one gate only; we do not include the matched input/cut while calculating cone size.

 Design A Design B module top (a,b,c,o); input a,b,c; output o; wire d,e,f,g; wire gg,ff; and (d,a,b); xor (e,a,b); xor (f,d,e); _cut cut_2_1(ff,f); nand (g,b,c); _cut cut_1_1(gg,g); xor (o,ff,gg); endmodule ` ` `module top (a,b,c,o);` input a,b,c; output o; wire d,e,f,g; wire gg,ff; and (d,a,b); xor (e,a,b); or (f,d,e); _cut cut_2_1(ff,f); and (g,b,c); _cut cut_1_bar_1(gg,g); xnor (o,ff,gg); `endmodule`` `

Figure 3. Example output of Team A.

Team B

Team B does not insert any cuts and generates the same result. Therefore, the result is still equivalent with the cost (5, 5)

 Design A Design B module top (a,b,c,o); input a,b,c; output o; wire d,e,f,g; and  (d,a,b); xor  (e,a,b); xor  (f,d,e); nand (g,b,c); xor  (o,f,g); endmodule `module top (a,b,c,o);` input a,b,c; output o; wire d,e,f,g; and (d,a,b); xor (e,a,b); or  (f,d,e); and (g,b,c); xnor(o,f,g); `endmodule `` `` `

Team C

Team C inserts three corresponding cut sets, and those cut sets are equivalent. However, the output pair (o, o) are non-equivalent. Therefore, this output would be treated as non-equivalent with the cost of non-equivalent cones. The cost would be 2 + 2, summation from the gates in non-equivalent compared sets.

 Design A Design B module top (a,b,c,o); input a,b,c; output o; wire d,e,f,g; wire dd,ee,gg; and (d,a,b); _cut cut_1_1 (dd,d); xor (e,a,b); _cut cut_2_1 (ee,e); xor (f,dd,ee); nand (g,b,c); _cut cut_3_bar_1 (gg,g); xor (o,f,gg); endmodule module top (a,b,c,o); input a,b,c; output o; wire d,e,f,g; wire dd,ee,gg; and (d,a,b); _cut cut_1_1 (dd,d); xor (e,a,b); _cut cut_2_1 (ee,e); or (f,dd,ee); and (g,b,c); _cut cut_3_1 (gg,g); xnor (o,f,gg); endmodule Team D

Team D inserts two corresponding cut sets. The cut_1 contains two cuts in Design A and two cuts in Design B. However, the cut_1 set is nonequivalent. The cut_2 set is also nonequivalent, since cut_2 contains only one cut. Therefore, the cost of this output would be 2+2+2+2+2+2+3 = 15 from five cuts in nonequivalent and 2 nonequivalent output pairs.

 Design A Design B module top (a,b,c,o); input a,b,c; output o; wire d,e,f,g; wire dd,ee,gg; and (d,a,b); _cut cut_1_1 (dd,d); xor (e,a,b); //_cut cut_1_1(ee,e); conflict name _cut cut_1_2 (ee,e); //inst name should not conflict xor (f,dd,ee); nand (g,b,c); _cut cut_2_1 (gg,g); xor (o,f,gg); endmodule module top (a,b,c,o); input a,b,c; output o; wire d,e,f,g; wire dd,ee; and (d,a,b); _cut cut_1_1 (dd,d); xor (e,a,b); //_cut cut_1_1(ee,e); _cut cut_1_2 (ee,e); or (f,dd,ee); and (g,b,c); xnor (o,f,g); endmodule Team Ranking

1.     Team A

2.     Team B

3.     Team C

4.     Team D

Team A is ranked as the highest team. Although team A and B are equivalent, team B has a higher cost. Team C has less cost than Team D. We will use the rank in each testcase to score the teams.

## V. EVALUATION METHODOLOGY

We evaluate the results by checking the equivalence of compared sets and calculating its cost using the objective function. Half the cases will address the ECO problem; the other half will address the EC problem. For each case, we evaluate the cost of the result and rank the teams from 1 to 7 to get the point from (10, 7, 5, 4, 3, 2, 1). The team with the most points wins.

With regards to the cost of each case, we evaluate the statement in problem formulation. When the cost ties, we compare their rank by runtime.

The hard limit of the results are:

1.     The format of generated netlist should be correct, otherwise the score would be 0. Furthermore, logic rewriting and renaming is forbidden.

2.     If the runtime of analysis is larger than 1800, there is no score.

## VI. PROBLEM GUIDANCE

Although we encourage participants to use creative thinking when solving this problem, we have included some tips to help guide the problem solving:

l  To read the netlist, you will need a simple parser.

l  The result is valid if you can further generate the same output netlist.

l  Boolean equivalence is vital, especially in the following situations:

u  Removing a bad-cut for non-equivalent cuts

u  Determining whether two inputs are equivalent

u  Inserting cuts into the  equivalence net

u  Checking the equivalence of two combinational cones

l  The simplest way to determine non-equivalence is random simulation. The more robust way is to use a formal engine, including ABC  , to check the logic equivalence. However, a complete engine is not always necessary, especially when you need to save time for analysis. Therefore, one task may be to find/write an engine that quickly validates non-equivalence with higher reliability.

l  In the end, try to tackle SDC/ODC and diagnose the root-cause of non-equivalence. If you can find the structure correlation, you can figure out more creative idea for resolving this problem.Have fun.

## VII. REFERENCE

    A. Kuehlmann and F. Krohm. “Equivalence checking using cuts and heaps.” DAC 1997

    C.-C. Lin, K.-C. Chen, S.-C. Chang, M. Marek-Sadowska, and K.-T. Cheng. “Logic synthesis for engineering change.” DAC 1995

    Z. Khasidashvili, J. Moondanos, D. Kaiss, and Z. Hanna. “An Enhanced Cut-points Algorithm in Formal Equivalence Verification”. HLDVT 2001.

    S.-L. Huang, W.-H. Lin, and C.-Y. (Ric) Huang. “Match and replace: a functional ECO engine for multi-error circuit rectification.” ICCAD 2011

    J. Long, R.K. Brayton,  and M.L. Case,  “LEC: Learning Driven Data-path Equivalence Checking.” DIFTS @FMCAD. 2013.

## VIII. BENCHMARK

l

l

l

l

l

l  Unit6.tgz (Remove Unit6.tgz)

l

l

l

l

l

l

l

l

l

l

l

l  Unit18.tgz(Hidden Case)

l  Unit19.tgz(Hidden Case)

l  Unit20.tgz(Hidden Case)

l  Unit21.tgz(Hidden Case)

l  Unit22.tgz(Hidden Case)

l  Unit23.tgz(Hidden Case)

Evaluation Results

l  Extra evaluation(Top 4)

 TOP unit1 unit2 unit3 unit4 unit5 unit7 unit8 unit9 unit10 unit11 unit12 unit13 unit14 unit15 unit16 unit17 score 1 EQ 4 NE 4 EQ 4 NE 4 EQ 4 EQ 5 NE 2 NE 3 EQ 7 NE 7 EQ 7 NE 4 EQ 10 NE 7 EQ 7 NE 10 89 2 EQ 10 NE 7 EQ 7 NE 7 EQ 10 TO 0 NE 4 NE 5 EQ 10 IV 0 EQ 10 TO 0 NE 7 TO 0 EQ 10 TO 0 87 3 NE 0 NE 1 EQ 2 NE 3 EQ 2 NE 2 NE 5 NE 2 NE 4 NE 10 NE 4 NE 7 NE 4 NE 10 NE 4 NE 7 67 4 EQ 5 NE 5 EQ 5 NE 5 EQ 7 EQ 10 NE 7 NE 4 TO 0 NE 4 TO 0 NE 10 TO 0 TO 0 TO 0 TO 0 62

## FAQ

1.     Q1: _cut cut_1_1 (dd,d);

Can dd be replaced with any name?

Must it be named dd?

ANS: Yes, you can change the wire name, but cannot the topology of netlist.

Q2:In figure 2 design B. There is not a space between xnor and (o,f,g). Is it legal?

ANS: Legal.

Q3: What is the maximal number of inputs of gates?

ANS: 32768

Q4: What does j mean in cut_i_j? In the example, all of cuts named cut_i_1.

Is there any situation that j is not 1?

ANS: Yes, when there is multiple equivalent cuts in a single design, you should name them with different j in integer.

Q5: Should we find equivalent cuts in one design? e.g. Team D

Or, can we identify equivalent cuts in only one design?

ANS: You can identify multiple equivalent cuts in a single design. For example, cut_1 group has 3 cuts in design A but 0 in design, and cut_2 group has 2 cuts in design A and 2 in design B.

2.     2 * 7 +3 = 17 not 15

the right answer should be 2 +2 +2 +2 +2 +2 +3 = 15 ? ANS: The result is wrong, thanks for you help

3.     If we have cut_1_1 and cut_1_2 in design A, but no cut in design B, then how the cost will be calculate?  equivalent or non_equivalent ?

ANS: If cut_1_1 and cut_1_2 in design A are equivalent, that is equivalent.

4.     Is the naming of the following situation legal or not? There is an AND gate which has the input A,B and has a cut "cut_1_1" in the output.

Can we name the cut "cut_1_bar_2" at the output of other NAND gate which has the same input. Both AND gate and NAND gate are in design A.

ANS: Yes, that’s legal and should be considered in your algorithm to optimize to cuts.

5.     Must design A and B be equivalent?

(b)If not, could we know which testcases are equivalent before running our program?

ANS: (a)Around half of cases are non-equivalent, and you may use random-pattern simulation to check the “design equivalence”.

However, if you would like to check the output equivalence in detail, we would suggest you to write the approach to check the non-equivalent more accurately, (and quickly).

(b)No, there is no corner case that needs high effort to check the design equivalence. (We will deliver the testcase soon).

6.     In example for problem B graphs of netlists are isomorphic, but some gates are different. Do exist cases with different graphs of netlists?

ANS: Yes. You can expect all the cases are not isomorphic, as in our benchmark cases.

7.     Can we use power of ABC and BOOST in our source?

ANS: You can do that. Please make sure you can build the code correctly in our environment.

8.     "If the runtime of analysis is larger than 1800, there is no score." Do you mean in seconds?

ANS: Right, 1800 seconds.

9.     In given example, what if Team C adds cut on "f"? do cut d, e need to be delete to prevent false negative? In other words, my question is, cut set equivalence is checked based on primary input? or based on cut in its transitive fan-in? for example, if Team C add a cut on f , you will check "cut-set f" using primary input a,b ? or using cut d,e?

ANS: The equivalence would consider the pi and cut set. If you add the “f” without removing d and e, f would be treated as noneq cut-set.

So if Team C add a cut on f , we will check "cut-set f" using cut d,e

10.  If 2 compared primary outputs are non-equivalent. But it's caused by some error occur at middle position. That is, the function is correct near primary input and primary output. But it isn't correct at the position between them, is it meaningful to tag the cut near primary output?

ANS: If it cannot reduce the size of non-eq compared set, that is not helpful. In general cases for the noneq problem, just isolate the noneq part would be the good way to get the good result.

11.  Can we insert a cut on output pin? Or output pin has already been considered as a cut? What if the design A and B are not equivalent, will we always have the non-equivalent cost on the output?

ANS: Output already be the compared set, if you add the cut at output, there will be extra cost but still okay. About the design A and B are not eq, output compared set may become EQ if you add the some cut set. This is also the main purpose of this topic.

12. Given 2 cuts, A and B,if they share some logic gates, what the cost will be? Will the intersection part be computed twice individually in computations of A and B?

ANS: The cone size computation is individually computed by each cut or po.

13. Given 2 cuts in the same group, what if they are in transitive path to each other? Is this condition legal? e.g., we add a cut before and after a buffer/not gate.

ANS: They may become noneq in most of cases. For example, PI->cut1->buf->cut2->po.  The function of cut1 is PI but the function of cut2 is cut1.

14. Can we use mini-SAT tool (http://minisat.se/) in our source code?

ANS: Sure, you can use any package or tools, but just make sure your program could run without any problem in our evaluation machine.

15. If I did not submit files in alpha test, may I still submit files for beta test?

ANS: Yes. You are encouraged to submit files for beta test and final test.

16. For problem B, are we allowed to output temporary text files during the execution of our program? We will read information from the temporary text file to execute our program. Is it possible that numerous programs will be executed at the same time, or the temporary file will be deleted while our program is still running, and we will fail to access the temporary file?

ANS: We would create the independent directories to evaluate your binary for every cases. More clearly, if there are 3 cases, 3 teams, we would create teamA.case1 teamA.case2 ….. teamC.case3:  9 directories for evaluating your binaries without any collision on temp files. Therefore, output temporary file would be okay if it is reasonable and the path is relative to the sub-path of your program env, please submit it to Beta test.

1.     You say: “C. The cost of the result with non-equivalent sets is the summation of the cone size from the points in the non-equivalent compared sets.​​​” But suppose that two cones include common gate.​ Will be this gate calculated twice?

ANS: Yes, count the cone separately, so the common gates would be computed multiple times.