請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/9005完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 江介宏 | |
| dc.contributor.author | Hsuan-Po Lin | en |
| dc.contributor.author | 林炫伯 | zh_TW |
| dc.date.accessioned | 2021-05-20T20:06:22Z | - |
| dc.date.available | 2009-08-14 | |
| dc.date.available | 2021-05-20T20:06:22Z | - |
| dc.date.copyright | 2009-08-14 | |
| dc.date.issued | 2009 | |
| dc.date.submitted | 2009-08-11 | |
| dc.identifier.citation | [1] R. L. Ashenhurst. The decomposition of switching functions. Computation Lab,
Harvard University, Vol. 29, pp.74-116, 1959. [2] Berkeley Logic Synthesis and Veri cation Group. ABC: A system for sequential synthesis and veri cation. http://www.eecs.berkeley.edu/ alanmi/abc/ [3] J. Cong and Y.-Y. Hwang. Boolean matching for LUT-based logic blocks with applications to architecture evaluation and technology mapping. IEEE Transac- tions on Computer-Aided Design of Integrated Circuits, 20(9):1077-1090, 2001. [4] J. Cong and K. Minkovich. Improved SAT-based Boolean matching using implicants for LUT-based FPGAs. In Proc. ACM International Symposium on Field Programmable Gate Arrays, pp.139-147, 2007. [5] S. A. Cook. The complexity of theorem proving procedures. Proc. Third Annual ACM Symposium on the Theory of Computing, pp.151-158, 1971. [6] W. Craig. Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic, 22(3):250-268, 1957. [7] H. A. Curtis. New Approach to the Design of Switching Circuits. Van Nostrand, Princeton, NJ, 1962. [8] M. Davis and H. Putnam. A Computing Procedure for Quanti cation Theory. Journal of the ACM, 7(3):201-215, 1960. [9] M. Davis, G. Logemann, and D. Loveland. A machine program for theoremproving. Communications of the ACM, 5(7):394-397, 1962. [10] N. E en and N. S oensson. An extensible SAT-solver. In Proc. International Con- ference on Theory and Applications of Satis ability Testing, pp.502-518, 2003. [11] J.-H. R. Jiang and R. K. Brayton. Functional dependency for veri cation reduction. In Proc. International Conference on Computer Aided Veri cation, pp.268-280, 2004. [12] J.-H. R. Jiang, J.-Y. Jou, and J.-D. Huang. Compatible class encoding in hyperfunction decomposition for FPGA synthesis. In Proc. ACM/IEEE Design Au- tomation Conference, pp.712-717, 1998. [13] G. Karypis, R. Aggarwal, V. Kumar, and S. Shekhar. Multilevel Hypergraph Partitioning: Application in VLSI Domain. In Proc. ACM/IEEE Design Au- tomation Conference, pp.526-529, 1997. [14] R. M. Karp. Functional decomposition and switching circuit design. J. Soc. Ind. Appl. Math. 11(2):291-335, 1963. [15] Y.-T. Lai, M. Pedram, and S. B. K. Vrudhula. BDD based decomposition of logic functions with applications to FPGA synthesis. In Proc. ACM/IEEE De- sign Automation Conference, pp.642-647, 1993. [16] C.-C. Lee, J.-H. R. Jiang, C.-Y. Huang, and A. Mishchenko. Scalable exploration of functional dependency by interpolation and incremental SAT solving. In Proc. IEEE/ACM International Conference on Computer-Aided Design, pp.227-233, 2007. [17] R.-R. Lee, J.-H. R. Jiang, and W.-L. Hung. Bi-decomposing large Boolean functions via interpolation and satis ability solving. In Proc. ACM/IEEE Design Automation Conference, pp.636-641, 2008. [18] H.-P. Lin, J.-H. R. Jiang, and R.-R. Lee. To SAT or Not to SAT: Ashenhurst Decomposition in a Large Scale. In Proc. IEEE/ACM International Conference on Computer-Aided Design, pp.32-37, 2008. [19] A. C. Ling, D. P. Singh, and S. D. Brown. FPGA technology mapping: A study of optimality. In Proc. ACM/IEEE Design Automation Conference, pp.427-432, 2005. [20] K. L. McMillan. Interpolation and SAT-based model checking. In Proc. Inter- national Conference on Computer Aided Veri cation, pp.1-13, 2003. [21] P. Pudl ak. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62(3):981-998, September 1997. [22] J. P. Roth and R. M. Karp. Minimization over Boolean graphs. IBM Journal, pp.227-238, 1962. [23] C. Scholl. Functional Decomposition with Applications to FPGA Synthesis. Kluwer Academic Publishers, 2001. [24] H. Sawada, T. Suyama, and A. Nagoya. Logic synthesis for look-up table based FPGAs using functional decomposition and support minimization. In Proc. IEEE/ACM International Conference on Computer-Aided Design, pp.353-358, 1995. [25] T. Stanion and C. Sechen. A Method for Finding Good Ashenhurst Decompositions and Its Application to FPGA Synthesis. In Proc. ACM/IEEE Design Automation Conference, pp.60-64, 1995. [26] S. Safarpour, A. G. Veneris, G. Baeckler, and R. Yuan. E cient SAT-based Boolean matching for FPGA technology mapping. In Proc. ACM/IEEE Design Automation Conference, pp.466-471, 2006. [27] G. S. Tseitin. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, pp.466-483, 1970. [28] K.-H. Wang and C.-M. Chan. Incremental learning approach and SAT model for Boolean matching with don't cares. In Proc. IEEE/ACM International Con- ference on Computer-Aided Design, pp.234-239, 2007. [29] B. Wurth, K. Eckl, and K. Antreich. Functional Multiple-Output Decomposition: Theory and an Implicit Algorithm. In Proc. ACM/IEEE Design Automa- tion Conference, pp.54-59, 1995. [30] B. Wurth, U. Schlichtmann, K. Eckl, and K. Antreich. Functional multipleoutput decomposition with application to technology mapping for lookup tablebased FPGAs. ACM Trans. on Design Automation of Electronic Systems, 4(3):313-350, 1999. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/9005 | - |
| dc.description.abstract | 函式拆解著眼於將一個布林函式拆解成一系列較小的子函式。在本篇論文裡面，
我們著重在亞氏函式拆解，這是一種因為他的簡易性而有許多實際應用的常見函 式拆解法。我們將函式拆解問題包裝成可滿足性求解問題，更進一步的採用克雷 格內插法以及函式相依性計算來找出相對應的子函式。在我們採用可滿足性求解 法為核心的研究中，輸入變數分組的過程可以被自動的處理，並且嵌入我們的函 式拆解演算法中。我們也可以自然的將我們的演算法延伸，應用在允許共用輸入 變數與多輸出變數的函式拆解問題上，這些問題在以往採用二元決策圖為核心資 料結構的演算法中都很難被解決。實驗結果顯示，我們提出的演算法可以有效的 處理輸入變數達到三百個之多的函式。 | zh_TW |
| dc.description.abstract | Functional decomposition aims at decomposing a Boolean function into a set of smaller sub-functions. In this thesis, we focus on Ashenhurst decomposition, which has practical applications due to its simplicity. We formulate the decomposition problem as SAT solving, and further apply Craig interpolation and functional dependency computation to derive composite functions. In our pure SAT-based solution, variable partitioning can be automated and integrated into the decomposition procedure. Also we can easily extend our method to non-disjoint and multiple-output decompositions which are hard to handle using BDD-based algorithms. Experimental results show the scalability of our proposed method, which can effectively decompose functions with up to 300 input variables. | en |
| dc.description.provenance | Made available in DSpace on 2021-05-20T20:06:22Z (GMT). No. of bitstreams: 1 ntu-98-R96943076-1.pdf: 680572 bytes, checksum: 5ccbc3358e2510d39742cbaa14656813 (MD5) Previous issue date: 2009 | en |
| dc.description.tableofcontents | Acknowledgements i
Chinese Abstract ii Abstract iii List of Figures viii List of Tables ix 1 Introduction 1 1.1 Thesis Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.3 Our Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Thesis Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2 Preliminaries 11 2.1 Functional Decomposition . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.1 Decomposition Chart . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Functional Dependency . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3 Satisability and Interpolation . . . . . . . . . . . . . . . . . . . . . . 16 2.3.1 Conjunctive Normal Form . . . . . . . . . . . . . . . . . . . . 16 2.3.2 Circuit to CNF Conversion . . . . . . . . . . . . . . . . . . . . 16 2.3.3 Propositional Satisability . . . . . . . . . . . . . . . . . . . . 18 2.3.4 Refutation Proof . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.3.5 Craig interpolation . . . . . . . . . . . . . . . . . . . . . . . . 22 3 Main Algorithms 27 3.1 Single-Output Ashenhurst Decomposition . . . . . . . . . . . . . . . . 27 3.1.1 Decomposition with Known Variable Partition . . . . . . . . . 28 3.1.2 Decomposition with Unknown Variable Partition . . . . . . . 37 3.2 Multiple-Output Ashenhurst Decomposition . . . . . . . . . . . . . . 43 3.2.1 Shared Variable Partition . . . . . . . . . . . . . . . . . . . . 45 3.3 Beyond Ashenhurst Decomposition . . . . . . . . . . . . . . . . . . . 46 3.4 Decomposition under Don't-Cares . . . . . . . . . . . . . . . . . . . . 47 3.5 Implementation Issues . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.5.1 Minimal UNSAT Core Renement . . . . . . . . . . . . . . . . 48 3.5.2 Balanced Partition . . . . . . . . . . . . . . . . . . . . . . . . 48 3.5.3 Elimination of Equality Constraint Clauses . . . . . . . . . . . 49 3.6 A Complete Example . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 4 Experimental Results 54 4.1 Single- and Two-Output Ashenhurst Decomposition . . . . . . . . . . 54 4.2 Quality of Variable Partition . . . . . . . . . . . . . . . . . . . . . . . 59 4.3 Fast Variable Partitioning . . . . . . . . . . . . . . . . . . . . . . . . 61 4.4 n-Output Ashenhurst Decomposition . . . . . . . . . . . . . . . . . . 67 4.5 Quality of Composite Functions . . . . . . . . . . . . . . . . . . . . . 68 5 Conclusions and Future Work 71 Bibliography 74 | |
| dc.language.iso | en | |
| dc.title | 利用可滿足性求解法與克雷格內插法之大尺度亞氏函式拆解 | zh_TW |
| dc.title | Large Scale Ashenhurst Decomposition via SAT Solving and Craig Interpolation | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 97-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 王國華,張耀文,江蕙如,黃鐘揚 | |
| dc.subject.keyword | 布林函式,函式拆解,可滿足性求解法,克雷格內插法,函式相依性, | zh_TW |
| dc.subject.keyword | Boolean function,functional decomposition,SAT solving,Craig interpolation,functional dependency, | en |
| dc.relation.page | 78 | |
| dc.rights.note | 同意授權(全球公開) | |
| dc.date.accepted | 2009-08-12 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
| 顯示於系所單位： | 電子工程學研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-98-1.pdf | 664.62 kB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。