In this thesis, we optimize the algorithms in prior backward-cut-based functional ECO work [7] [8] and propose a dual-phase ECO method. In the merging phase, the Strash and FRAIG technique identifies the input-side frontier of the patch. In the matching phase, a cut-matching algorithm based on simulation is applied to identify the output-side frontier of the patch. For each matching iteration, we remove the redundant parts of output-side frontier by a pair-refinement algorithm. This move not only reduce the patch cost but also save us run time. The experimental results show that our ECO engine can rectify multi-errors ECO problems with small patch sizes within reasonable run time. In addition, we apply the backward-cut approach to equivalence checking and compare the performance with other forward-based method, such as FRAIG. The experimental results demonstrate that our backward-cut-based EC method works for some testcases.
For the future work on ECO problems, we plan to design a QBF solving algorithm for pair-refinement so that we can refine the rectification pairs more precisely and get a smaller patch. For EC, we need a more effective cut-matching algorithm, which can generate the matched cuts with high probability even when dealing with complex circuits.
Reference
[1] Kuochun Lee, Tsung-Yen Chen, “Automatic engineering change order methodology,” U.S. Patent 6 453 454, September 17, 2002.
[2] M. Fujita, T. Kakuda, Y. Matsunaga, "Redesign and Automatic Error Correction of Combinational Circuits", Logic and Architecture Synthesis, ed. G. Saucier, North-Holland: Elsevier Science Publishers B.V., pp. 253-262.
[3] C.-C Lin, K.-C. Chen, and M. Marek-Sadowska, “Logic Synthesis for Engineering Change”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and
Systems, March 1999.
[4] Andal Jayalakshmi, "Functional Eco Automation Challenges and Solutions", 2nd Asia Symposium on Quality Electronic Design, pp. 126-129, 2010.
[5] C.-Y. Huang, C.-J. Hsu, and C.-A. Wu, “2017 ICCAD CAD Contest Problem A: Resource-aware patch generation,” in Proc. ICCAD, 2017.
http://cad-contest-2017.el.cycu.edu.tw/Problem_A/default.html
[6] A.-C. Cheng, I. H.-R. Jiang and J.-Y. Jou, “Resource-aware functional ECO patch generation,” Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1036-1041, 2016.
[7] S.-L. Huang, W.-H. Lin, P.-K. Huang and C.-Y. Huang, “Match and replace: A functional ECO engine for multi-error circuit rectification,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), vol. 32, no.
3, pp. 467-478, March 2013.
[8] Chia-Lin Hsieh, “Semi-Formal ECO Method,” Master Thesis, Graduate Institute of Electronics Engineering, College of Electrical Engineering and Computer Science, National Taiwan University, Jul. 2018.
https://hdl.handle.net/11296/g3b8pj
[9] N. So ̈rensson and N. Ee ́, “Minisat v1. 13: A SAT solver with conflict- clause minimization,” in Proc. SAT, pp. 53–54, 2005.
[10] D. Brand, “Verification of large synthesized designs,” in Proc. IEEE/ACM ICCAD, pp. 534–537, Nov. 1993.
[11] A. Mishchenko, S. Chatterjee, and R. Brayton, “Fraigs: A unifying representation for logic synthesis and verification,” EECS Dept., UC Berkeley, Tech. Rep, 2005.
[12] M. Abadir, J. Ferguson, and T. Kirkland, “Logic design verification via test generation,” IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol. 7, no. 1,
pp. 138–148, Jan. 1988.
[13] P.-Y. Chung and I. Hajj, “Accord: Automatic catching and correction of logic design errors in combinational circuits,” in Proc. Int. ITC, pp. 742–751, Sep. 1992.
[14] A. Veneris and I. Hajj, “Design error diagnosis and correction via test vector simulation,” IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol. 18, no.
12, pp. 1803–1816, Dec. 1999.
[15] Y.-S. Yang, S. Sinha, A. Veneris, and R. Brayton, “Automating logic rectification by approximate SPFDs,” in Proc. ASP-DAC, pp. 402–407, Jan. 2007.
[16] A. Ling, S. Brown, S. Safarpour, and J. Zhu, “Toward automated ECOs in FPGAs,”
IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol. 30, no. 1, pp. 18–30, Jan. 2011.
[17] B.-H. Wu, C.-J. Yang, C.-Y. Huang, and J.-H. Jiang, “A robust functional ECO engine by SAT proof minimization and interpolation techniques,” in Proc.
IEEE/ACM Int. Conf. ICCAD, pp. 729–734, Nov. 2010.
[18] K. H. Chang, I. Markov, and V. Bertacco, “Fixing design errors with counterexamples and resynthesis,” IEEE Trans. Comput.-Aided Design Integr.
Circuits Syst., vol. 27, no. 1, pp. 184–188, Jan. 2008.
[19] K.-F. Tang, C.-A. Wu, P.-K. Huang, and C.-Y. Huang, “Interpolation-based incremental ECO synthesis for multi-error logic rectification,” in Proc. 48th ACM/EDAC/IEEE DAC, pp. 146–151, Jun. 2011.
[20] K.-F. Tang, P.-K. Huang, C.-N. Chou and C.-Y. Huang, "Multi-patch generation for multi-error logic rectification by interpolation with cofactor reduction," Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1567-1572, 2012.
[21] S.-Y. Huang, K.-C. Chen, and K.-T. Cheng, “Autofix: A hybrid tool for automatic logic rectification,” IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol. 18, no. 9, pp. 1376–1384, Sep. 1999.
[22] D. Hoffmann and T. Kropf, “Efficient design error correction of digital circuits,” in Proc. ICCD, pp. 465–472, Sep. 2000.
[23] D. Brand, “Incremental synthesis,” in Proc. IEEE/ACM ICCAD, pp. 14–18, Nov.
1994.
[24] S. Krishnaswamy, H. Ren, N. Modi, and R. Puri, “DeltaSyn: An efficient logic difference optimizer for ECO synthesis,” in Proc. IEEE/ACM ICCAD, pp. 789–796,
Nov. 2009.
[25] A. Kuehlmann and F. Krohm, “Equivalence checking using cuts and heaps,” in Proc.
34th ACM/IEEE DAC, pp. 263–268, Jun. 1997.
[26] Q. Zhu, N. Kitchen, A. Kuehlmann, and A. Sangiovanni-Vincentelli, “SAT sweeping with local observability don’t-cares,” in Proc. 43rd ACM/IEEE DAC, pp.
229–234, Jul. 2006.
[27] ABC: A system for sequential synthesis and verification. Berkeley Logic Synthesis and Verification Group.
http://www-cad.eecs.berkeley.edu/~alanmi/abc
[28] A. Biere, “The AIGER And-Inverter Graph (AIG) format version 20071012” in Technical report FMV Reports Series Institute for Formal Models and Verification, Johannes Kepler University, 2007.
http://fmv.jku.at/papers/Biere-FMV-TR-07-1.pdf
[29] M. Soeken, “IWLS 2017 Programming Contest: Y Logic Synthesis,” 2017.
https://github.com/msoeken/iwls2017-contest
[30] L.Amaru ́, P.-E.Gaillardon, and G.DeMicheli, “The epfl combinational benchmark suite,” in Proc. 24th International Workshop on Logic & Synthesis (IWLS), no.
EPFL-CONF-207551, 2015.
https://lsi.epfl.ch/page-102566-en-html/benchmarks/