請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/16097
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚 | |
dc.contributor.author | Kai-Fu Tang | en |
dc.contributor.author | 湯凱富 | zh_TW |
dc.date.accessioned | 2021-06-07T18:00:56Z | - |
dc.date.copyright | 2012-08-27 | |
dc.date.issued | 2012 | |
dc.date.submitted | 2012-08-06 | |
dc.identifier.citation | [1] M. S. Abadir, J. Ferguson, and T. E. Kirkland. Logic design veri cation
via test generation. IEEE Trans. on CAD of Integrated Circuits and Systems, 7(1):138{148, 1988. [2] C. Albrecht. IWLS 2005 benchmarks. In http://iwls.org/iwls2005/benchmarks.html. [3] A. Ayari and D. A. Basin. Bounded model construction for monadic second-order logics. In Proc. CAV, pages 99{112, 2000. [4] M. Benedetti. Quanti er trees for QBFs. In Proc. SAT, pages 378{385, 2005. [5] Berkeley Logic Synthesis and Veri cation Group. ABC: A system for sequential synthesis and veri cation. [6] A. Biere. Resolve and expand. In Proc. SAT, pages 59{70, 2004. [7] D. Brand. Veri cation of large synthesized designs. In Proc. ICCAD, pages 534{537, 1993. [8] D. Brand, A. D. Drumm, S. Kundu, and P. Narain. Incremental synthesis. In Proc. ICCAD, pages 14{18, 1994. [9] R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Convergence testing in term-level bounded model checking. In Proc. CHARME, pages 348{362, 2003. [10] K.-H. Chang, I. L. Markov, and V. Bertacco. Fixing design errors with counterexamples and resynthesis. IEEE Trans. on CAD of Integrated Circuits and Systems, 27(1):184{188, 2008. [11] D. Chen and D. Singh. Line-level incremental resynthesis techniques for FPGAs. In Proc. FPGA, pages 133{142, 2011. [12] P.-Y. Chung and I. N. Hajj. ACCORD: Automatic catching and correction of logic design errors in combinational circuits. In Proc. ITC, pages 742{751, 1992. [13] J. Cong and K. Minkovich. Improved SAT-based Boolean matching using implicants for LUT-based FPGAs. In Proc. FPGA, pages 139{ 147, 2007. [14] W. Craig. Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symb. Log., 22(3):250{268, 1957. [15] M. Davis, G. Logemann, and D. W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394{397, 1962. [16] N. Dershowitz, Z. Hanna, and J. Katz. Bounded model checking with QBF. In Proc. SAT, pages 408{414, 2005. [17] N. Dershowitz, Z. Hanna, and A. Nadel. A scalable algorithm for minimal unsatis able core extraction. In Proc. SAT, pages 36{41, 2006. [18] N. E en and N. S orensson. An extensible SAT-solver. In Proc. SAT, pages 502{518, 2003. [19] U. Egly, M. Seidl, H. Tompits, S. Woltran, and M. Zolda. Comparing di erent prenexing strategies for quanti ed Boolean formulas. In Proc. SAT, pages 214{228, 2003. [20] Z. Feng, Y. Hu, L. He, and R. Majumdar. IPR: In-place recon guration for FPGA fault tolerance. In Proc. ICCAD, pages 105{108, 2009. [21] M. Fujita, Y. Tamiya, Y. Kukimoto, and K.-C. Chen. Application of Boolean uni cation to combinational logic synthesis. In Proc. ICCAD, pages 510{513, 1991. [22] E. Giunchiglia, M. Narizzano, and A. Tacchella. Quanti er structure in search-based procedures for QBFs. IEEE Trans. on CAD of Integrated Circuits and Systems, 26(3):497{507, 2007. [23] L. Henkin. Some remarks on in nitely long formulas. In In nitistic methods, pages 167{183. 1961. [24] M. Herbstritt, B. Becker, and C. Scholl. Advanced SAT-techniques for bounded model checking of blackbox designs. In Proc. MTV, pages 37{44, 2006. [25] E. L. Horta, J. W. Lockwood, D. E. Taylor, and D. B. Parlour. Dynamic hardware plugins in an FPGA with partial run-time recon guration. In Proc. DAC, pages 343{348, 2002. [26] Y. Hu, Z. Feng, L. He, and R. Majumdar. Robust FPGA resynthesis based on fault-tolerant Boolean matching. In Proc. ICCAD, pages 706{ 713, 2008. [27] S.-Y. Huang, K.-C. Chen, and K.-T. Cheng. Error correction based on veri cation techniques. In Proc. DAC, pages 258{261, 1996. [28] S.-Y. Huang, K.-C. Chen, and K.-T. Cheng. AutoFix: A hybrid tool for automatic logic recti cation. IEEE Trans. on CAD of Integrated Circuits and Systems, 18(9):1376{1384, 1999. [29] C. Kao. Bene ts of partial recon guration. Xcell Journal, pages 65{67, 2005. [30] J. Katz, Z. Hanna, and N. Dershowitz. Space-e cient bounded model checking. In Proc. DATE, pages 686{687, 2005. [31] S. Krishnaswamy, H. Ren, N. Modi, and R. Puri. DeltaSyn: An e cient logic di erence optimizer for ECO synthesis. In Proc. ICCAD, pages 789{796, 2009. [32] A. Kuehlmann, D. I. Cheng, A. Srinivasan, and D. P. LaPotin. Error diagnosis for transistor-level veri cation. In Proc. DAC, pages 218{224, 1994. [33] Y. Kukimoto and M. Fujita. Recti cation method for lookup-table type FPGA's. In Proc. ICCAD, pages 54{61, 1992. [34] C.-F. Lai, J.-H. R. Jiang, and K.-H.Wang. Boolean matching of function vectors with strengthened learning. In Proc. ICCAD, pages 596{601, 2010. [35] C.-F. Lai, J.-H. R. Jiang, and K.-H. Wang. BooM: a decision procedure for Boolean matching with abstraction and dynamic learning. In Proc. DAC, pages 499{504, 2010. [36] C.-C. Lin, K.-C. Chen, and M. Marek-Sadowska. Logic synthesis for engineering change. IEEE Trans. on CAD of Integrated Circuits and Systems, 18(3):282{292, 1999. [37] C.-H. Lin, Y.-C. Huang, S.-C. Chang, and W.-B. Jone. Design and design automation of recti cation logic for engineering change. In Proc. ASP-DAC, pages 1006{1009, 2005. [38] A. C. Ling, S. D. Brown, S. Safarpour, and J. Zhu. Toward automated ECOs in FPGAs. IEEE Trans. on CAD of Integrated Circuits and Sys- tems, 30(1):18{30, 2011. [39] A. C. Ling, S. D. Brown, J. Zhu, and S. Safarpour. Towards automated ECOs in FPGAs. In Proc. FPGA, pages 3{12, 2009. [40] A. C. Ling, D. P. Singh, and S. D. Brown. FPGA logic synthesis using quanti ed Boolean satis ability. In Proc. SAT, pages 444{450, 2005. [41] A. C. Ling, D. P. Singh, and S. D. Brown. FPGA technology mapping: a study of optimality. In Proc. DAC, pages 427{432, 2005. [42] F. Lonsing and A. Biere. Integrating dependency schemes in searchbased QBF Solvers. In Proc. SAT, pages 158{171, 2010. [43] J. C. Madre, O. Coudert, and J. P. Billon. Automating the diagnosis and the recti cation of design errors with PRIAM. In Proc. ICCAD, pages 30{33, 1989. [44] K. L. McMillan. Interpolation and SAT-based model checking. In Proc. CAV, pages 1{13, 2003. [45] D. Mesquita, F. G. Moraes, J. Palma, L. M oller, and N. L. V. Calazans. Remote and partial recon guration of FPGAs: Tools and trends. In Proc. IPDPS, page 177, 2003. [46] G. Peterson, S. Azhar, and J. Reif. Lower bounds for multiplayer noncooperative games of incomplete information. Journal of Computers and Mathematics with Applications, 41:957{992, 2001. [47] P. Pudl ak. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62(3):981{998, 1997. [48] S. Safarpour, A. G. Veneris, G. Baeckler, and R. Yuan. E cient SATbased Boolean matching for FPGA technology mapping. In Proc. DAC, pages 466{471, 2006. [49] C. Scholl and B. Becker. Checking equivalence for partial implementations. In Proc. DAC, pages 238{243, 2001. [50] N. P. Sedcole, B. Blodget, T. Becker, J. Anderson, and P. Lysaght. Modular partial recon guration in Virtex FPGAs. In Proc. FPL, pages 211{216, 2005. [51] T. Shinsha, T. Kubo, Y. Sakataya, J. Koshishita, and K. Ishihara. Incremental logic synthesis through gate logic structure identi cation. In Proc. DAC, pages 391{397, 1986. [52] A. Smith, A. G. Veneris, and A. Viglas. Design diagnosis using Boolean satis ability. In Proc. ASP-DAC, pages 218{223, 2004. [53] S. Szeider. Minimal unsatis able formulas with bounded clause-variable di erence are xed-parameter tractable. In Proc. COCOON, pages 548{ 558, 2003. [54] K.-F. Tang, C.-A. Wu, P.-K. Huang, and C.-Y. Huang. Interpolationbased incremental ECO synthesis for multi-error logic recti cation. In Proc. DAC, pages 146{151, 2011. [55] G. S. Tseitin. On the complexity of derivation in propositional calculus. In Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pages 466{483. Springer, 1983. [56] A. G. Veneris and I. N. Hajj. Design error diagnosis and correction via test vector simulation. IEEE Trans. on CAD of Integrated Circuits and Systems, 18(12):1803{1816, 1999. [57] C. Wrathall. Complete sets and the polynomial-time hierarchy. Theor. Comp. Science, 3(1):23{33, 1976. [58] B.-H. Wu, C.-J. Yang, C.-Y. Huang, and J.-H. R. Jiang. A robust functional ECO engine by SAT proof minimization and interpolation techniques. In Proc. ICCAD, pages 729{734, 2010. [59] Y.-S. Yang, S. Sinha, A. G. Veneris, and R. K. Brayton. Automating logic recti cation by approximate SPFDs. In Proc. ASP-DAC, pages 402{407, 2007. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/16097 | - |
dc.description.abstract | In modern VLSI designs, late design changes are nearly inevitable to fix the design bugs or to cope with the specification changes. Due to the cost and time-to-market pressure, it is unlikely that designers would like to modify the register-transfer level (RTL) design and re-run the whole design flow from the beginning. Instead, they identify a patch circuit to rectify the gate-level design for the differences. This process is called logic rectification.
This dissertation focuses on two closely related rectification problems: rectification for application-specific integrated circuits (ASICs) and field-programmable gate arrays (FPGAs). Rectification for ASICs For a design with multiple functional errors, multiple patches are usually needed to correct the design. Previous works on logic rectification are limited to single-output patch. In other words, only one erroneous behaviors can be fixed in one iteration. As a result, it may lead to unnecessarily large patches or even failure in rectification. We generalize the existing rectification techniques to a great extent and propose direct and incremental logic rectifications. For direct logic rectification, we derive multiple-output patch by interpolation with cofactor reduction. The multiple-output patch considers multiple design errors simultaneously. For incremental logic rectification, single- and multiple-output partial patches are identified in an iterative manner. Our experiments incorporate both direct and incremental methods, and the algorithms perform well on large designs. Rectification for FPGAs We present rectification methods for look-up table (LUT) type FPGAs to correct an erroneous circuit implementation by in-place logic reconfiguration; that is, we only reconfigure the functions of the LUTs and do not change the routing of the erroneous circuit. Therefore, the rectification can be very efficient since the relatively much more expensive re-routing can be avoided. Our proposed algorithm is based on the Boolean satisfiability (SAT) solver and use dynamic learning techniques to accelerate the computation. To enhance the reconfiguration power, both direct and incremental methods are investigated. Experimental results demonstrate that the learning techniques are effective in pruning infeasible solutions for both academic and industrial benchmarks. | en |
dc.description.provenance | Made available in DSpace on 2021-06-07T18:00:56Z (GMT). No. of bitstreams: 1 ntu-101-D94943039-1.pdf: 6139235 bytes, checksum: cf9b2768f2b3e4c61b6fcb9b392557fc (MD5) Previous issue date: 2012 | en |
dc.description.tableofcontents | 1 Introduction 5
1.1 Objective and Contributions . . . . . . . . . . . . . . . . . . . 10 1.2 Organization of the Dissertation . . . . . . . . . . . . . . . . . 12 2 Background 13 2.1 Boolean Satisability . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.1 Basic Denitions . . . . . . . . . . . . . . . . . . . . . 14 2.1.2 SAT-Solving Algorithms . . . . . . . . . . . . . . . . . 16 2.1.3 Unsatisable Core . . . . . . . . . . . . . . . . . . . . 17 2.1.4 Interpolation . . . . . . . . . . . . . . . . . . . . . . . 18 2.1.5 Tseitin Transformation . . . . . . . . . . . . . . . . . . 21 2.2 Quantied Boolean Formula (QBF) . . . . . . . . . . . . . . . 24 2.2.1 Basic Denitions . . . . . . . . . . . . . . . . . . . . . 25 2.2.2 Applications of Quantied Boolean Formulae . . . . . . 26 2.3 Dependency Quantied Boolean Formula (DQBF) . . . . . . . 27 I Minimal Logic Dierence Identication for ASIC Rectication 30 3 Direct Logic Rectication 31 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.3 Single-Output Patch . . . . . . . . . . . . . . . . . . . . . . . 37 3.4 The k-Direct-Rectiability Problem . . . . . . . . . . . . . . . 39 3.5 Multiple-Output Patch . . . . . . . . . . . . . . . . . . . . . . 43 3.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 4 Incremental Logic Rectication 51 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.3 Overview of the Incremental Approach . . . . . . . . . . . . . 55 4.4 Single-Output Partial Patch . . . . . . . . . . . . . . . . . . . 58 4.4.1 Rectication for All Outputs . . . . . . . . . . . . . . . 64 4.4.2 Rectication for an Output Subset . . . . . . . . . . . 66 4.5 Multiple-Output Partial Patch . . . . . . . . . . . . . . . . . . 67 4.6 Integrated Logic Rectication Flow . . . . . . . . . . . . . . . 72 4.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 5 Experimental Results 75 6 Conclusions 84 II In-Place Logic Reconguration for FPGA Rectication 86 7 Logic Reconguration for FPGAs 87 7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 7.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 7.3 Logic Reconguration for FPGAs . . . . . . . . . . . . . . . . 93 7.3.1 Finding Candidate LUTs . . . . . . . . . . . . . . . . . 94 7.3.2 SAT-Based Logic Reconguration . . . . . . . . . . . . 97 7.3.3 Reconguration with Dynamic Learning . . . . . . . . 101 7.3.4 Incremental Reconguration . . . . . . . . . . . . . . . 106 7.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 8 Experimental Results 111 9 Conclusions 118 10 Bibliography 120 | |
dc.language.iso | en | |
dc.title | 基於內插法與滿足性之邏輯修正 | zh_TW |
dc.title | Interpolation and SAT-Based Logic Rectification | en |
dc.type | Thesis | |
dc.date.schoolyear | 100-2 | |
dc.description.degree | 博士 | |
dc.contributor.oralexamcommittee | 江蕙如,江介宏,顏嘉志,王俊堯 | |
dc.subject.keyword | 邏輯修正,內插法,滿足性, | zh_TW |
dc.subject.keyword | logic rectification,interpolation,satisfiability, | en |
dc.relation.page | 129 | |
dc.rights.note | 未授權 | |
dc.date.accepted | 2012-08-07 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-101-1.pdf 目前未授權公開取用 | 6 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。