ECO Flow for Fixing Datapath Bugs
Abstract
This paper is presented to discuss the ECO methodology and flow for fixing datapath bugs. Compared to the control logic, datapath is much more complex, and fixing datapath bugs is more difficult than fixing control logic bugs. In this paper, an ECO flow is presented for fixing datapath bugs. The topics to be covered include:
● Difficulty in fixing datapath bugs by ECO
● ECO Flow for datapath bug fixing
● Fix datapath bugs at algorithm level
● Formal verification: great help for fixing datapath bugs
● Formal verification: indispensable for the datapath verification
1. Introduction
Engineering Change Order or ECO has been becoming more and more popular in current complex ASIC designs. The reasons for its prevalence can be split into two categories, saving money and saving time. First, ECOs on the first silicon using spare cells make changes only on the metal masks so that much money for re-making the full set of masks can be saved. Second, ECOs can save much time for re-running the entire design flow to make changes on design. There have been several literatures [1,2,3] addressing the ECO methodology and flow, especially Steve Golson’s SNUG paper [3] covers almost all general aspects of ECO and gives out a very good flow based on that many ECOs can be completed. However, fixing bugs by ECO has been mainly focused on small changes like control logic bugs. No effort has been specially made on the complex datapath logic.
Compared to control logic, its datapath counterpart is much more complex and hard to design, so Synopsys has a dedicated tool, Module Compiler, for the description and synthesis of datapth. The datapath discussed here is modeled in Module Compiler Language (MCL). It is composed of not only simple logic gates but also arithmetic units like adders and multipliers. These arithmetic units are usually unavailable in the spare cells, which are composed of almost simple logic gates. All these lead to the great difficulty in fixing datapath bugs.
Challenges for fixing datapath bugs
1) The operations of datapath are mainly Multiply and Add/Minus, which can be realized with different structures provided by MC. For an example of 8-bit adder, it is modeled in MCL as below:
module adder8 ( A, B, C );
input signed [8] A, B;
output signed [9] C;
directive (group=”adder”, delay=2000, fatype=”cla”,);
C = A + B;
endmodule
Synthesize the adder8 in TSMC .18um process and set the delay to 2ns, the synthesis results of adder8 using different final adder type are shown in Table 1.

It’s clear that, the synthesis results are much different from each other with different final adder types, in terms of area, timing and cell used. The synthesized logic can be more complicated when the constraints like period and area change, especially when the pipeline and retime are enabled. MC’s such great flexibility provides us a platform to find out a relatively optimized implementation of datapath under specific area and delay requirements. But it also brings us great difficulties in debugging and fixing datapath bugs.
2) Because of the complexity of the synthesized datapath logic, it’s very difficult to find the point(s) causing the bug(s) in the gate netlist.
3) Datapath changes are often related to arithmetic units, but such units are unavailable in the spare cells.
4) Datapath design is often area critical, so very few spare cells have been put in the old netlist.
5) Datapath is often timing critical, limiting the changes to be small.
6) Complete verification of the ECO netlist is very hard to fulfill by traditional simulation, because the bugs depend on the input vectors. It’s impossible for the stimulus to cover tens of thousands of possible input vector combinations.
Because of the challenges mentioned above, a good methodology and complete ECO flow are vital to the success of the ECO on datapath. In this paper, a flow is presented for functional datapath ECO of fully hierarchy design with ECO routing only.
2. Methodology
It’s well known that the same algorithm can be realized in different ways by doing some mathematic operation and transforms. Also due to the carry-in of add operation, the errors in the LSB also cause the higher bits to fail. Based on these observations, we get a methodology for fixing datapath bugs.
1) Fix bugs at algorithm level. It’s possible to find alternatives to realize the same algorithm. Some of the alternatives may be implemented easily in the old netlist.
2) If failed to find a simple alternative, compare the old and new gate netlists by formal verification tool to find out all the falling points, which usually compose a bus.
3) Select the lowest LSB of the bus as the starting point, explore the logic cones using the debug function of the formal verification tool. By comparing the two logic cones and checking the discrepancies between them, find an easiest way to make them functionality equivalent.
4) Formal check the modified netlist and the new netlist. There can be 3 kinds of results,
● The two designs are equivalent. Then the logic fix is finished.
● All the failing points remain.
● The LSB failing point becomes matched, but other failing points remain. In this case, select the second lowest LSB of the remaining failing points as starting point.
5) Repeat 3 and 4 until the two designs are totally functionality equivalent.
3. Formal verification
Previously, formal verification tool is regarded as best friend for ECO, but not a must. However, when fixing datapath bugs, it becomes indispensable, because
The traditional simulation
1) Very hard to cover all possible input vectors when the datapath becomes more complex,
2) Very hard to do functional coverage analysis of the simulation results,
3) Great time consuming;
In contrast, formal verification tools
4) Can cover all possible input vectors to check equivalence between two designs,
5) Much more faster than the traditional simulation,
6) Of great help for debugging and finding out the points causing the bugs.
In my point of view, traditional simulation is impossible to fully check the equivalence of datapath designs. However, formal verification tool can check equivalence of two designs by exhausting all possible input vectors. It’s highly recommended to have a formal verification tool at hand before performing ECO on datapath.
4. Flow
4.1 Design flow with MC integrated
A basic design flow with MC integrated is shown in Figure 1. The design is partitioned into two parts, logic described in HDL and datapath modeled in MCL.
First, MCL is compiled and synthesized to get MC gate netlist,
Second, input the MC gate netlist and HDL code to DC to get top-level gate netlist,
Then, physical implementation of the netlist in back end tools.

Below is a list of tools used in the flow,
Module Compiler, for datapath synthesis
Design Compiler, for logic synthesis
Physical Compiler, for physical synthesis
Apollo, for placing & routing
PrimeTime, for Static Timing Analysis
Formality, for formal verification
4.2 ECO flow
Some terms are defined in Table 1 for the description of ECO flow. Relationship among different netlists is shown in Figure 2.


The ECO flow is composed of the following steps:
1) Use Formality to confirm equivalence of the old MC gate netlist and the corresponding module in the old netlist.
2) Synthesize the new MCL to get the new MC behavioral and gate netlists.
3) Use Formality to confirm differences between the new MC gate netlist and the module in the old netlist.
4) Find out logic fixes to the bugs in the old netlist.
5) Modify the old netlist to make the ECO netlist.
6) Use Formality to confirm equivalence of the new MC gate netlist and that module in the ECO netlist.
7) Implement the ECOs in back-end tools.
8) Extract parasitic and do static timing analysis.
4.3 Flow exploration
1) Use Formality to confirm equivalence of the old MC gate netlist and the corresponding module in the old netlist
This step is to ensure that the module in the old netlist is the one you are intended to change. This is very important. Don’t go ahead before confirming the equivalence of the two blocks. There are two cases for the verification to fail.
One case is that, you really pick up the wrong module. So before verification you should find out the right module to be verified first.
Another is that, it is the right module, but it has been optimized in DC or Physical Compiler, this is possible if “compile -boundary_optimization” is used in DC or the attribute of boundary_optimization is set to TRUE in PC. For example, DC or PC has inverted some ports of the module. In this case, the command of “set_user_match” with the option of “-inverted” should be used. Then re-run the formal verification to check the equivalence.
2) Synthesize the new MCL to get the new MC behavioral and gate netlists
Modify the old MCL to get the new MCL. The modification should be limited to small changes, because even very small changes can result in big differences of the synthesized logic. If the changes are on the structure and lead to too many differences between the two designs, this means it is not a problem that can be solved by ECO.
Another way to see if the changes can be fixed by ECO or not is, to check the reports of MC to find out what cells have been used in both designs. The portion of “Cell Use Summary” in the report can tell what cells have been instantiated in the netlist.
3) Use Formality to confirm differences between the new MC gate netlist and the module in the old netlist
This performs the same operations as step 1, but it is to prove that the changes in the new MCL have taken place. At this time, those bug related compare points in the old design should be functionality un-equivalent to those in the new MC gate netlist.
It should be noted that there might be problem if the variable name_match takes the default value, all. This is because that these two designs are similar and have many instances and nets with the same name, but in some designs, the ending points of logic cones having the same name don’t compose a pair of compare points. One way to deal with this is to set the variable name_match to port [6].
4) Find out a logic fix to the bugs in the old netlist
Among all these steps, this one is the most difficult and critical. Fixing a simple datapath bug can take much time and efforts. As stated in section 2, it’s recommended to fix bugs at algorithm level first, if no solution is found, then use Formality to explore both designs to find out logic fixes to the bugs.
a). Fixing bugs at algorithm level
For one algorithm, there may exist different ways to realize it. Fix bugs at algorithm level is to make changes to the old algorithm to realize the new algorithm. The old algorithm has been implemented in the old design. The changes should be able to be easily implemented. The following two examples will show how to find logic fixes at algorithm level.
Example 1
This is a FIR filter with fixed coefficients. Its structure is shown in Figure 3.

Below is part of the MC script,
integer c0 = 7, c1 = -53, c2 = 302, c_odd = 512; // coefficients
wire signed [20:0] preadd0 = data_even_dly0 + data_even_dly5;
wire signed [20:0] preadd1 = data_even_dly1 + data_even_dly4;
wire signed [20:0] preadd2 = data_even_dly2 + data_even_dly3;
// directive (round=10); // !!! this directive has been missed in the old MCL
wire signed [30:0] product = preadd0*c0 + preadd1*c1 + preadd2*c2 + data_odd_delay2*c_odd;
In the old MCL, the “directive (round=10)” is missed. In MC, simple rounding of data the lowest N bits is realized by adding 1<<(N-1). Below is the implementation of the “product” with and without rounding.
Without rounding,
product = preadd0*c0 + preadd1*c1 + preadd2*c2 + data_odd_delay2*c_odd
With rounding,
product = preadd0*c0 + preadd1*c1 + preadd2*c2 + data_odd_delay2*c_odd + (1<<9)
To fix the bug, 1<<9 (=1024) need to be added to the “product” of the old design. Even though it is just a simple add operation, it is not easy to implement, because
1). Due to the “product” is not the ending points of logic cones, the internal results have been optimized. So it’s impossible to find “product” in the gate netlist.
2). Even if the “product” is the ending points of logic cones in some situations, adding a constant to it will require a serials of adders.
3). The synthesized logic is very large. For this filter, the gate netlist includes 534 instances and 833 nets.
But if we explore the algorithm, notice that c_odd is equal to 512 (= (1<<8)). Name the new product as product_eco. Then
product_eco = preadd0*c0 + preadd1*c1 + preadd2*c2 + data_odd_delay2*c_odd + (1<<9)
= preadd0*c0 + preadd1*c1 + preadd2*c2 + (data_odd_delay2 + 20’b010 )*c_odd
The “product_eco” can be realized if 20’b010 can be added to data_odd_delay2, in fact, adding 20’b010 to data_odd_delay2 is equivalent to adding 1 to data_odd_delay2[1]. In the old netlist, data_odd_delay2[1] has been renamed to N2306, which is input of half adder I320 as shown in Figure 4 (a). The function of half adder is
S = A ^ B; CO = A & B;
When adding 1 to data_odd_delay2[1], the desired S and CO is
S1 = A ^ B ^ 1’b1 = ~(A ^ B);
CO1 = ((A ^ B) & 1’b1) + (A & B) = (A ^ B) + (A & B);
(A ^ B) and (A & B) have been realized with N4172 and N4173 in the old netlist, so
S1 = ~ S; CO1 = S | CO;
A logic fix in Figure 4 (b) is designed, only one INV and one OR gate are needed to fix the bug.

Example 2
It is also a FIR filer with fixed coefficients.

Part of the MCL is as below,
integer c0 = -2, c1 = 3, c2 = 15; // coefficients
wire signed [20:0] preadd0 = data_dly0 + data_dly5;
wire signed [20:0] preadd1 = data_dly1 + data_dly4;
wire signed [20:0] preadd2 = data_dly2 + data_dly3;
// directive (round=5); // !!! this directive has been missed in the old MCL
wire signed [25:0] product = preadd0*c0 + preadd1*c1 + preadd2*c2;
In the old MCL, the “directive (round=5)” is missed, which is to round the lowest 5 bits of product. Below is the realization of the “product” in MC with and without rounding.
Without rounding,
product = preadd0*c0 + preadd1*c1 + preadd2*c2
With rounding,
product = preadd0*c0 + preadd1*c1 + preadd2*c2 + (1<<4)
We can use the same method as example 1, but among the coefficients of –2 and 3 and 15, 3 and 15 are not power of 2, -2 has different sign from 16.
But add all the coefficients together,
c0 + c1 + c2 = -2 + 3 + 15 = 16
Name the new product as product_eco, use the arithmetic studied at primary school,
product_eco = preadd0*c0 + preadd1*c1 + preadd2*c2 + (1<<4)
= (preadd0 + 21’b01)*c0 + (preadd1 + 21’b01)*c1 + (preadd2 + 21b’01)*c2
In the old netlist, data_dly0[0] is I_data[0] and data_dly5[0] is N1223 as shown in Figure 4 (a), which are inputs of half adder AHHCONX2, which generates arithmetic sum (S) and active-low carry-out (CON) of the input operand (A) and with carry-in (CI) . Its function is as blow
S = A ^ CI; CON = ~(A & CI);
When adding 1 to preadd0[0], the desired sum (S1) and carry-out (CON1) are
S1 = A ^ CI ^ 1’b1 = ~(A ^ CI);
CON1 = ~(((A ^ CI) & 1’b1) | (A & CI)) = ~(A ^ B) & ~(A &B);
(A ^ B) and (A & B) have been realized in the old netlist, so
S1 = ~ S; CO1 = ~S & CON;
So, one half adder with one INV and one AND can realize a full adder. Totally, three INVs and three ANDs are needed to fix the bug as shown in Figure 6 (b).

b). Exploring designs with Formality
It has been shown that if alternatives to realize the same algorithm of new MCL can be found, very small changes can fix the bugs. But due to the complexity of datapath, sometimes you can’t find out one. Even in such situation, maybe you still think the bug can be fixed. In this situation, you can try to explore the both designs with formal verification tool like Formality.
Example 3
This example models a Multiply and Accumulator (MAC). The structure of the MAC is as Figure 7.

Part of the MCL is as below,
directive (carrysave=”convert”, multtype=”booth”, round=3);
wire signed [25:0] product = I_data*I_coef;
wire signed [25:0] S, C;
csconvert(S,C,product);
wire signed [2:0] fdback_add_zero = 0;
directive local (pipeline=”off”, carrysave=”off”);
// directive (round=0); // !!! this directive has been missed in the old MCL
wire [27:0] accum, accum_temp;
accum = C + S + cat(I_fdback,fdback_add_zero);
In the old MCL, the “product” and “O_data” are both rounded at the lowest 3 bits, but the correct algorithm requires only one, so the other should be removed.
For this example, an alternative of the algorithm can’t be found to fix the bug. The recommended method is to explore the old and new designs with Formality, by comparing the discrepancies between them, the points causing the bug may be found.
I’d like to give some tips on the debugging process [7].
● First find out all falling points between the two designs. These points usually compose a bus.
● Select the lowest LSB of the failing points as the staring point.
● Trace back from this starting point. When back to a device with several inputs, try different input patterns in Formality to identify those contributing to differences at the output. Select one of them and continue to trace back.
● When one part of the logic is identified to be different, find out the points causing the discrepancies. Design a logic changes in the old netlist to make it functionally equivalent to the new design.
● After the lowest LSB is fixed but there are still other failing points, select the LSB of the remaining failing points as the new staring point. Repeat until the two designs are totally functionality equivalent.
5) Modify the old netlist to make the ECO netlist
It is to implement the logic fixes designed in the previous step by manual modification of the old netlist. You can use any editors you prefer, but it’s better to define a set of naming rules for the newly added instances or nets. For example, you can name the instances with I*_eco and the nets with N*_eco, so you can position or grep out what have been changed very soon. Modification for example 1 is as below.
// ECO on fir1: begin
//ADDHX2 I320 (.A(N2306), .B(N205), .CO(N4173), .S(N4172)); //original
wire N4172_eco, N4173_eco;
INVX1 I101_eco (.A(N4172_eco), .Y(N4172) );
OR2X1 I102_eco (.B(N4172_eco), .A(N4173_eco), .Y(N4173) );
ADDHX2 I320 (.A(N2306), .B(N205), .CO(N4173_eco), .S(N4172_eco));
// ECO on fir1: end
6) Use Formality to confirm equivalence of the new MC gate netlist and that module in the ECO netlist
This is same to step 1, but it is to verify the logic fixes just designed. If the new MC gate netlist and that module in the ECO netlist are equivalent, your ECO at logic level is done, if not, you should return to step 4.
7) Implement the ECO in back-end tools
While designing the logic fixes in step 4, you don’t need to care about timing only if the newly added cells are available in the spare cells. Even though this step is same as that of common ECO, usually the critical timing requirement of datapath makes it more difficult than ECO on control logic.
For back-end tools like Apollo and Astro, they have the ability of ECO auto routing. You don’t need to indicate which cell is used exactly. For example, to fix the bug of example 1, one INVX1 is needed. In the spare cell, there may be more than one INVX1 available. Apollo or Astro will search for that one that can achieve better timing. This is a very good feature, but in some cases, for example, in the layout one INVX3 is closer to the changes than any other INVX1. So your active participation in the selection of cells is preferred.
In GUI of back-end tools, highlight those instances related to any changes in the old netlist, then highlight all spare cells, select those closer to the changes, and modify the ECO netlist accordingly.
Do ECO routing in back-end tools, and report timing after then. If there are big timing violations on the fixes because the path is too long, try to design logic equivalent cells with available spare cells near to the changes, for example, using NAND to replace INV.
Then modify the ECO netlist and re-do ECO routing. Usually 3 iterations can make timing closed if the changes are not too complicated. What should be noted is to repeat step 5 once the ECO netlist is modified.
Below is an Astro “freeze silicon” ECO flow:
● Backup the original lib and cell prior to proceeding further.
● Read in the new netlist with the same settings used when the original netlist was read. This will create NETL view. Then expand the netlist using same settings as the original expansion. This will create EXP view. (Command: auVerilogIn, cmCmdExpand)
● Use ECO by Net Compare Method. If we do not want to change clock tree nets or Scan Chains, select “Freeze” options. (Command: auECOByNetCmp)
● After opening ECO Library and top cell, set the silicon freeze status. Because we want Astro to maintain the pin and pad locations and placement of standard and macro cells during an ECO operation. (Command: axSetFreezeSiliconECO (geGetEditCell) #t)
● Preserve hierarchy of the cell. (Command: astInitHierPreservation, astMarkHierAsPreserved)
● Marks groups of cells as spare cells. Because Astro cannot move any cells, we need to provide the spare cells a reserve at specific locations that we might later need for adding cells during ECO process. The groups have named during spare cells placement process. (Command: axgECOMarkSpareGroup)
● Automatically merge or split spare cells for swapping with new cell instances. (Command: axgECOAutoPlaceFS)
● Performs incremental routing for new cells. If layout changes are minor, set “modified nets first, others later” option. (Command: axgECORouteDesign)
● ECO completed. Run DRC and LVS.
8) Extract parasitic and do static timing analysis
This timing analysis is the last step to verify the ECO implemented design. If no timing violations arise, your ECO is done.
5. Advanced topics on datapath RTL-to-Gate verification
There is often a need to do equivalence check between RTL and gate netlists or between the MC behavioral and gate netlists. This is a very tough job. In the new releases of Formality, some new features and enhancements are available to speed up the datapath verification.
1) Datapath Solver (DPS) enhancement [8]
Formality has a dedicated solver targeting complex arithmetic components. For example, the solvers will be invoked if Formality can identify multipliers in both the reference and implementation versions of the design. If the multiplier solvers can prove equivalence, a “Pre-verification SUCCESSFUL” message appears in the log file and those multipliers will be black boxed. This should allow Formality to run much faster during the full verification state when the other solvers are used to verify the design.
If the multiplier solvers cannot prove equivalency during the pre-verification stage, a “Pre-verification INCONCLUSIVE” message will be shown in the log file for the corresponding multiplier. This simply means the multiplier in question could not be proven equivalent with the faster multiplier solver so the regular logic solvers will need to verify that multiplier during full verification.
The DPS has been enhanced to support additional arithmetic instantiated DesignWare components. In previous releases, the automatic deployment of the Datapath solver was limited to multipliers. In the version of v2003.12, the supported DesignWare parts include DW02_MAC, DW02_PRODSUM, DW02_PRODSUM1, DW02_SUM, DW_SQUARE, DW02_MULT and DW02_MULT_N_STAGE.
2) Multiplier Generator [9,10,11]
A complex datapath that has been flattened after synthesis might be difficult to verify from RTL. The DPS only works when multipliers have their own level of hierarchy. So, the regular logic solvers will be used for this verification. This might take a very long time and even return inconclusive verification. The problem with multipliers is that the architecture implementation is not known at the RTL stage.
A new algorithm has been introduced to help the regular logic solver when the Datapath Solver (DPS) could not work. The Multiplier Generator enables Formality to “build” the multiplier implementation of RTL designs. This makes the RTL and Gate representation of the multipliers structurally very similar, greatly helping the verification solvers.
The Multiplier Generator is disabled by default, so you’ll need to use the following variables:
set enable_multiplier_generation true
set hdlin_multiplier_architecture “dw_foundation”
3) Verification Effort Level and Incremental Verification
The new verification_effort_level variable is used to set the solver effort level to low, medium, or high (the default). By setting the effort level to values low or medium, you may be able to quickly solve the less complex logic cones at the expense of limiting the ability to solve some of the more complex logic cones. This can allow you to locate any complex points faster than a run using the default setting of high.
After verification is completed or stopped, you can go back and re-verify aborted compare points without starting over. The status of previously passing or failing points is retained and verification continues with points that were aborted due to complexity, timeout limit, failing point limit, or user interrupt.
The combination of these features are useful in cases (usually RTL to gate verifications) when the verify command appears to be stuck. The recommended usage mode is to use the default settings of these variables for initial verification runs and to use these new features as needed in cases where the verify command appears to get stuck when there are many points still left to be verified.
4) Distributed Verification
The verification processes can be executed in parallel across a maximum of four additional CPUs to enhance performance. The processor running the original fm_shell program is considered the “Master” and you can add the additional CPUs before verification begins. The master process will partition the design so that it can spread the verification work among the processors you specified.
6. Conclusions and Recommendations
This paper introduces a feasible ECO methodology and flow for fixing datapath bugs. Even though the datapath bugs are very difficult to fix and verify, it is possible for the ECO to succeed if a good flow is available. Below are some conclusions and recommendations.
1) It’s possible to fix datapath bugs by ECO. Don’t give up before you try your best, especially when the chip has taped out. Re-run the entire design flow means you have to re-make the full set of masks. That’s a great amount of money still increasing with the scaling down of process.
2) Formal verification tool like Formality is a must for fixing datapath bugs. If you don’t have one in place, persuade your manager buy one before you proceed.
3) Hierarchy design is of great help to ECO. It’s preferred to separate the datapath from other control logic. A good partition can easy the datapath debug and verification.
4) Compare the MC log files of synthesis of the old and new MCL. The log file lists all the cells used in the gate netlist. Then you can find how much they are different, especially to check how many arithmetic units are different.
5) Select the lowest LSB of the falling points as the starting point. The failing points of datapath usually compose a bus. The lowest LSB can cause the higher bits to fail, so fixing the LSB first is very important.
6) Active participant in the ECO routing can get better timing performance. Find the ECO related cells and wires in the layout and then highlight available space cells around them, select those close to them.
Because the complexity of datapath and different timing and area requirements, whether a datapath ECO can succeed or not is design dependent. If the methodology and flow presented in this paper can be of some help to your work, it’s my great pleasure.
7. References
[1] Mark Thomas Fox, “Methodology of ECO Compiler,”
[2] John Horgans, John Pedicone, Greg Guiher, James P. Flynn, “Formal Verification: Verification of an ECO-Intensive Hiearchical Design,” SNUG Europe 2003.
[3] Steve Golson, “The Human ECO Compiler,” SNUG San Jose 2004.
[4] “Module Compiler User Guide,” Synopsys, Version 2003.12
[5] “Formality User Guide,” Synopsys, Version 2003.12
[6] “Disabling Name Matching for Select Compare Points”, Synopsys, SolvNet Doc ID: 000808, 09/17/2003
[7] “Updated Formality Debugging Methodology Guide”, Synopsys, SolvNet Doc ID: 003993, 02/26/2003
[8] “Formality Datapath Solvers Is Not Called”, Synopsys, SolvNet Doc ID: 005504, 04/22/2003
[9] “Formality Verification of Complex Datapath RTL2FlatGate with Multiplier Generator”, Synopsys, SolvNet Doc ID: 007945, 09/17/2003
[10] “How Do I Speed Up the Verification of a Design That Contains Multpliers?”, Synopsys, SolvNet Doc ID: 007724, 09/18/2003
[11] “How to Verify a Flatten Netlist Including Multipliers With Formality”, Synopsys, SolvNet Doc ID: 006982, 09/18/2003



