ICCAD 2015 Contest
LargeScale Equivalence Checking and Function
Correction
ChihJen (Jacky) Hsu
Cadence Taiwan, Inc.
2F, No.65, Du Sing Rd., Hsinchu, Taiwan
Efficient
equivalence checking [1] and
functional correction [2] on largescale
designs are crucial technologies for handling today¡¦s demanding design
cycles. Analyzing an entire design is not always practical for largescale
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 largescale designs. The
corresponding cuts represent points of functional correspondence between the
two designs, allowing you to partition the designs into smaller subproblems.
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 largescale 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 timetomarket
is paramount, late changes (specification changes or bug fixes) are implemented
using an Engineering Change Order (ECO)[2] 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 largescale 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 largescale ECOs.
The EC and ECO processes both have two netlists. To start to solve the
problems in both processes, we focus on one targetisolating large designs
into corresponding smaller instancesbut with two different objectives. EC
divides the large instances into smaller equivalent ones and cannot tolerate
any nonequivalent subinstances; ECO isolates the large instance into
rootcause of changes and minimizes the nonequivalent subinstance. 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: largescale design isolation.
Several academic studies have addressed these issues. Khasidashvili et al. [3] used BDD to explore the
equivalent cut for helping the EC. Huang et al. [4] extended the Boolean matching problem on
nonexact multiple candidates and also demonstrated the effectiveness of
applying functional isolation in ECO. Long et al. [5] proposed the
highlevel learning for correlating the correspondence through the highlevel
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.
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 longterm advances.
Given
two corresponding, combinational gatelevel 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 invertedequivalence. Therefore, the added cuts
would be grouped in a set as the equivalent groups with phase consideration.
3. We treat
the matched inputpairs 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 nonequivalent.
4.
We rank the results using the following
objective function:
a. Generated
netlists without nonequivalent compared sets rank higher than those with
nonequivalent sets.
b. The
cost of the result without
nonequivalent 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 nonequivalent
sets is the summation of the cone size from the points in the nonequivalent
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
nonequivalent 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 inversedequivalence 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>
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 inversephase.
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 nonequivalent. Therefore,
this output would be treated as nonequivalent with the cost of nonequivalent
cones. The cost would be 2 + 2, summation from the gates in nonequivalent
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.
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.
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 badcut for nonequivalent 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 nonequivalence is random simulation. The more robust
way is to use a formal engine, including ABC [6] ,
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 nonequivalence with
higher reliability.
l In
the end, try to tackle SDC/ODC and diagnose the rootcause of nonequivalence.
If you can find the structure correlation, you can figure out more creative
idea for resolving this problem.Have fun.
[1]
A. Kuehlmann and F. Krohm.
¡§Equivalence checking using cuts and heaps.¡¨ DAC 1997
[2]
C.C. Lin,
K.C. Chen, S.C. Chang, M. MarekSadowska, and K.T.
Cheng. ¡§Logic synthesis for engineering change.¡¨ DAC 1995
[3]
Z. Khasidashvili, J. Moondanos, D. Kaiss, and Z. Hanna. ¡§An Enhanced Cutpoints Algorithm in
Formal Equivalence Verification¡¨. HLDVT 2001.
[4]
S.L.
Huang, W.H. Lin, and C.Y. (Ric) Huang.
¡§Match and replace: a functional ECO engine for multierror circuit
rectification.¡¨ ICCAD 2011
[5]
J. Long,
R.K. Brayton, and M.L.
Case, ¡§LEC: Learning Driven
Datapath Equivalence Checking.¡¨ DIFTS @FMCAD. 2013.
[6]
ABC: A
system for sequential synthesis and verification.
l Unit6.tgz (Remove Unit6.tgz)
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)
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 
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 nonequivalent, and you may use randompattern 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 nonequivalent 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
fanin? for example, if Team C add a cut on f , you
will check "cutset 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 cutset.
So if Team C add a cut on f ,
we will check "cutset f" using cut d,e
10.
If 2 compared primary outputs are nonequivalent. 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 noneq 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 nonequivalent 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 miniSAT 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 ¡K.. 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 subpath of
your program env, please submit it to Beta test.
1.
You say: ¡§C. The cost of the result with
nonequivalent sets is the summation of the cone size from the points in the
nonequivalent 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.