為了降低電路的設計時間以及製造的成本，功能性的工程變更
命令 (ECO) 已經在現代的超大型積體電路 (VLSI) 設計中成為一
項重要的技術。在這篇論文，我們提出了一個兩階段的演算法來找
出兩個電路相異的部分。藉由可滿足性 (SAT) 檢測程式，我們找
到了兩電路相同部分的輸入端邊界。另一方面，藉由我們提出的電
路結構對應演算法，我們找出了兩電路相同部分的輸出端邊界。從
實驗結果可以得知，我們的演算法在尋找邊界上非常的有效率，同
時，在大部分的案例上都有不錯的效果。

In order to reduce the circuit developing time and manufacture cost, functional
ECO becomes an important technique in modern VLSI design. In this
thesis, we propose a dual-phase algorithm to find the difference between two
circuits. The input-side and output-side boundaries are found by SAT engine
and our structure matching algorithm respectively. The experimental results
show that our method is very efficient to find the boundary and performs
good in most cases.

1 Introduction . 1
2 Previous Work . 5
3 Algorithm . 8
3.1 Input-side Equivalence Checking . 8
3.2 Output-side Circuit Structure Matching . 10
3.2.1 Similarity Computation . 12
3.2.2 Fan-in Matching . 13
3.2.3 Output Side Boundary Decision. 14
4 Experimental Results . 16
4.1 Experimental Setup . 16
4.2 Results and Analysis . 17
5 Conclusion . 19

[1] S. Krishnaswamy, H. Ren, N. Modi, and R. Puri, “DeltaSyn: An Efficient
Logic Difference Optimizer for ECO Synthesis,” Proc. of Inter-
national Conference on Computer-Aided Design (ICCAD), pp. 789-796,
2009.
[2] S. Huang, W. Lin, P. Huang, and C. R. Huang “Match and Replace:
A Functional ECO Engine for Multierror Circuit Rectification,” IEEE
Transactions on Computer-Aided Design of Intergrated Circuits and Sys-
tems (TCAD), vol. 32, no. 3, pp. 467-478, 2013.
[3] H. Ren, R. Puri, L. Reddy. S. Krishnaswamy, C. Washburn, J. Earl,
J. Keinert “Intuitive ECO Synthesis for High Performance Circuits,”
Proc. of Design, Automation & Test in Europe Conference & Exhibition
(DATE), pp. 1002-1007, 2013.
[4] S. Y. Huang, K. C. Chen and K. T. Cheng, “Error Correction Based
on Verification Techniques,” Proc. of Design Automation Conference
(DAC), pp. 258-261, 1996.
[5] S. Y. Huang, K. C. Chen and K. T. Cheng, “AutoFix: A Hybrid Tool
for Automatic Logic Rectification,” IEEE Transactions on Computer-
20
Aided Design of Intergrated Circuits and Systems (TCAD), vol. 18, no.
9, pp. 1376-1384, 1999.
[6] A. C. Ling, S. D. Brown, J. Zhu, S. Safarpour, “Toward Automated
ECOs in FPGAs,” IEEE Transactions on Computer-Aided Design of
Intergrated Circuits and Systems (TCAD), vol. 30, no. 1, pp. 18-30,
2010.
[7] K. F. Tang, C. A. Wu, P. K. Huang, C. Y. Huang, “Interpolation-based
Incremental ECO Synthesis for Multi-error Logic Rectification,” Proc.
of Design Automation Conference (DAC), pp. 146-151, 2011.
[8] B. H.Wu, C. J. Yang, C. Y. Huang, J. H. R. Jiang, “A Robust Functional
ECO Engine by SAT Proof Minimization and Interpolation Techniques,”
Proc. of International Conference on Computer-Aided Design (ICCAD),
pp. 729-734, 2010.
[9] S. Safarpour, H. Mangassarian, et al., “Improved Design Debugging
Using Maximum Satisfiability,” Proc. of Formal Methods in Computer-
Aided Design (FMCAD), pp. 13-19, 2007.
[10] 2012 CAD Contest at ICCAD.
http://cad_contest.cs.nctu.edu.tw/CAD-contest-at-ICCAD2012/
[11] LEDA: C++ Class Library for Efficient Data Yypes and Algorithms
http://www.algorithmic-solutions.com/leda/
[12] Limboole: A Simple Tool for Checking Satisfiability.
http://fmv.jku.at/limboole/