請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/48000
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang Huang) | |
dc.contributor.author | Ting-Hao Lin | en |
dc.contributor.author | 林庭豪 | zh_TW |
dc.date.accessioned | 2021-06-15T06:44:12Z | - |
dc.date.available | 2011-07-18 | |
dc.date.copyright | 2011-07-18 | |
dc.date.issued | 2011 | |
dc.date.submitted | 2011-07-01 | |
dc.identifier.citation | [1] Kevin Oo Tinmaung, David Howland, and Russell Tessier, “Power-aware FPGA Logic Synthesis Using Binary Decision Diagrams”, In Proc. of FPGA 2007, Feb 2007.
[2] Michael Keating, David Flynn, Robert Aitken, Alan Gibbons, Kijian Shi, “Low Power Methodology Manual For System on Chip Design”, Electronic Edition, Springer, 2007. [3] M. Hamada, M. Takahashi, H. Arakida, A. Chiba, T. Terazawa, T. Ishikawa, M. Kanazawa, M. Igarashi, K. Usami, and T. Kuroda, “A top-down low power design technique using clustered voltage scaling with variable supply-voltage scheme,” in Proc. IEEE Custom Integrated Circuits Conference, May 1998, pp. 495-498. [4] L. Benini, G. De Micheli, “Automatic synthesis of low power gated-clock finite-state machines,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol.15, Iss.6, Jun 1996. [5] Aaron P. Hurst, “Automatic Synthesis of Clock Gating Logic with Controlled Netlist Perturbation,” In Proc. of DAC 2008, pages 654-657, 2008. [6] H. Jacobson, P. Bose, Z. Hu, P. Eickemeyer, L. Eisen, J. Griswell, “Stretching the Limits of Clock-Gating Efficiency in Server-Class Processors,” In Proc. of HPCA 2005, pages 238-242, Feb 2005. [7] Biggs, T. et al., “A 1 Watt 68040-compatible microprocessor.” In Proc. of the IEEE Symposium on Low Power Electronics IEEE Computer Society Press, Los Alamitos, CA 12-13. [8] R. E. Bryant. “Graph-based algorithms for Boolean function manipulation,” IEEE Transactions on Computers, 35:677-691, 1986. [9] Eli Arbel, Cindy Eisner, Oleg Rokhlenko, “Resurrecting Infeasible Clock-Gating Functions,” In Proc. of DAC 2009, pages 160-165, 2009. [10] Eli Arbel, Oleg Rokhlenko, and Karen Yorav, “SAT-based Synthesis of Clock Gating Functions Using 3-Valued Abstraction,” In FMCAD 2009, pages198-204, 2009. [11] W. Craig, “Linear reasoning: A new form of the Herbrand-Gentzen theorem,” J. Symbolic Logic, 22(3):250-268, 1957. [12] G. S. Tseitin, “On the Complexity of Derivation in Propositional Calculus,” in Studies in Constructive Mathematics and Mathematical Logic, Part 2, 1968. [13] H. Z hang, “SATO: An efficient propositional prover”, Intl. Conf. on Automated Deduction 1997, pp. 272-275. [14] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: engineering an efficient SAT solver”, DAC 2001, pp. 530 – 535. [15] J.P. Marques-Silva and K.A. Sakallah, “GRASP-A search algorithm for propositional satisfiability”, T. Comp., vol. 48, pp. 506 – 521, 1999. [16] L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, “Efficient Conflict Driven Learning in a Boolean Satisfiability Solver”, ICCAD 2001, pp. 279 – 285. [17] E. Goldberg, Y. Novikov, “BerkMin: A Fast and Robust Sat-Solver”, DATE 2002, pp. 142 – 149. [18] M. Davis, and H. Putnam, 1960. “A computation procedure for quantification theory”. Journal of the Association for Computer Machinery 7, pp.201–215. [19] Nadel, B. 1990. “Some Applications of the Constraint Satisfaction Problem”. Technical Report CSC-90-008, Computer Science Department, Wayne State University. [20] J. Alan Robinson (1965), “A Machine-Oriented Logic Based on the Resolution Principle”. Journal of the ACM (JACM), Volume 12, Issue 1, pp. 23–41. [21] P. Pudlák, “Lower bounds for resolution and cutting plane proofs and monotone computations,” J. Symbolic Logic, 62(3):981-998, 1997. [22] K. L. McMillan, “Interpolation and SAT-based model checking,” in Proc. CAV, pp. 1-13, 2003. [23] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. “Symbolic model checking: 1020 states and beyond”. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990. [24] O. C., C. Berthet, and J.-C. Madre. “Verification of synchronous sequential machines based on symbolic execution”. In Joseph Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, June 1989. [25] Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. “Symbolic model checking without BDDs”. In TACAS’99, volume 1579 of LNCS, pages 193–207, 1999. [26] McMillan, K. L. “Interpolation and SAT-based model checking,” In CAV 2003, vol. 2725 of LNCS, Springer, pp. 1-13. [27] V. Kravets and P. Kudva. “Implicit enumeration of structural changes in circuit optimization”. In Proc. DAC, pp. 438-441, 2004. [28] E. Sentovich, H. Toma, and G. Berry. “Latch optimization in circuits generated from high-level descriptions”. In Proc. ICCAD, pp. 428-435, 1996. [29] B. Lin and A. R. Newton. “Exact redundant state registers removal based on binary decision diagrams”. In Proc. Int'l Conf. Very Large Scale Integration, pp. 277-286, 1991. [30] J.-H. R. Jiang and R. K. Brayton. “Functional dependency for verification reduction”. In Proc. CAV, pp. 268-280, 2004. [31] Chih-Chun Lee, Jie-Hong R. Jiang, Chung-Yang (Ric) Huang, and Alan Mishchenko. “Scalable Exploration of Functional Dependency by Interpolation and Incremental SAT Solving”. In Proc. IEEE/ACM Int'l Conf. on Computer-Aided Design (ICCAD'07), pages 227--233, San Jose, USA, November 2007. [32] U. Feige, “A Threshold of ln n for Approximation Set Cover,” J. of the ACM, 45(5): 634-652, 1998. [33] Niklas Eén, Niklas Sörensson, “A SAT Solver with Conflict-Clause Minimization,” poster for SAT 2005, 2005. http://minisat.se/Papers.html | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/48000 | - |
dc.description.abstract | 現今低功率消耗電路設計中節省動態功率消耗越來越受到重視,節省動態功率消耗最有效的技術之一是時脈閘控(Clock Gating),該技術阻擋那些不需要的時脈切換活動以達到節省動態功率消耗的目的。在這篇論文中,我們應用內插技術(Interpolation)在可滿足性基礎的時脈閘控演算法中給予增大原演算法求得之時脈閘控函數的靈活性。我們還開發了多種技術來改良時脈閘控演算法所需的時間花費與記憶體使用量,其中包含了一個根據時脈閘控函數能力的篩選器以減少可滿足性時脈閘控演算法中所需要的正規滿足性驗證的次數。一個可滿足性解法器中動態返回次數限制機制以縮短可滿足性解法器在驗證時脈閘控函數所需的驗證時間。此外,一個縮減時脈閘控函數邏輯閘的方法來減輕因增加時脈閘控邏輯閘所造成的面積花費。實驗結果顯示我們所提出的演算法在增加百分之五的面積花費中條件下能有阻擋兩倍於現今可靠性基礎的時脈閘控演算法中不需要的時脈切換活動。 | zh_TW |
dc.description.abstract | Dynamic power saving is gaining its dominance in modern low power designs, while clock gating, which blocks unnecessary clock switching activities, is one of the most efficient approaches to reduce the dynamic power. In this thesis, we exploit the interpolation technique in a SAT-based clock gating algorithm in order to grant a greater flexibility in enlarging the gating capabilities over the original gating candidates. We also developed several techniques to improve the runtime and memory usage of the clock gating algorithm, including a gating capability filter to reduce the number of formal SAT proofs, a dynamic backtracking limit controller to shorten the SAT runs, and a shrinking method to ease the final gate count overhead. The experimental results show that our proposed algorithm can gate up to 2X clock switches with less than 5% area overhead when compared to the state-of-the-art SAT-based clock gating methodology. | en |
dc.description.provenance | Made available in DSpace on 2021-06-15T06:44:12Z (GMT). No. of bitstreams: 1 ntu-100-F92921089-1.pdf: 1029487 bytes, checksum: c986645ce306e59a07fac0d43567d456 (MD5) Previous issue date: 2011 | en |
dc.description.tableofcontents | 口試委員會審定書 #
誌謝 i 中文摘要 ii ABSTRACT iii CONTENTS iv LIST OF FIGURES vi LIST OF TABLES vii Chapter 1 Introduction 1 1.1 The Basic of the Automatic Clock Gating Problems 5 1.2 The Symbolic Automatic Clock Gating Method 7 1.3 The SAT-based Automatic Clock Gating Method 8 1.4 Nowadays Automatic Clock Gating Algorithms 9 1.5 Our Contributions 11 Chapter 2 Preliminaries 13 2.1 Boolean Satisfiablity Problem 14 2.1.1 The CNF-based Boolean Satisfiability Solver 15 2.1.2 The Implication Graph 17 2.1.3 The Resolution Graph 18 2.2 Craig Interpolation 20 2.2.1 Construct Craig Interpolant by McMillan's Algorithm 20 2.2.2 Applications of the Interpolants 23 2.3 Modeling Clock Gating as a Satisfiability Problem 27 Chapter 3 Our Clock Gating Algorithm 30 3.1 Identifying Clock Gating Candidates 31 3.2 Extracting Interpolants 32 3.3 Selecting Gating Signals for Power Optimization 34 Chapter 4 Implementation 38 4.1 Memory Usage Improvement 39 4.2 Runtime Improvement 41 Chapter 5 Experimental Results 42 5.1 Comparison of Hurst’s Algorithm and Our Algorithm 43 5.2 Comparison of Applying and Not Applying the Proposed Techniques in Our Algorithm 45 Chapter 6 Conclusion 48 REFERENCE 49 | |
dc.language.iso | en | |
dc.title | 利用可滿足性基礎的克萊格內插法增大栓鎖時脈之函數 | zh_TW |
dc.title | Using SAT-based Craig Interpolation to Enlarge Clock Gating Functions | en |
dc.type | Thesis | |
dc.date.schoolyear | 99-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 黃俊郎(Jiun-Lang Huang),李建模(Chien-Mo Li),陳中平(Chung-Ping Chen),顧孟愷(Mong-Kai Ku) | |
dc.subject.keyword | 可滿足性解法器,克萊格內插法,栓鎖時脈, | zh_TW |
dc.subject.keyword | SAT solver,Craig Interpolation,Clock Gating, | en |
dc.relation.page | 52 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2011-07-01 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
顯示於系所單位: | 電機工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-100-1.pdf 目前未授權公開取用 | 1.01 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。