簡易檢索 / 詳目顯示

回結果列表
研究生： 陳勇志
Chen, Yung-Chih
論文名稱： 驗證意識之超大型積體電路邏輯最佳化技術之研究
On Synthesis and Optimization of VLSI Designs for Verification
指導教授： 王俊堯
Wang, Chun-Yao
口試委員: 黃婷婷
張世杰
王廷基
黃錫瑜
魏慶隆
葉經緯
李昆忠
黃俊達
學位類別： 博士
Doctor
系所名稱： 電機資訊學院 - 資訊工程學系
Computer Science
論文出版年： 2011
畢業學年度： 99
語文別： 中文
論文頁數： 87
中文關鍵詞： 超大型積體電路 、設計自動化 、電腦輔助設計 、電路驗證 、電路最佳化
外文關鍵詞： Very-large-scale integration, Electronic design automation, Computer-aided design, Design verification, Logic optimization
相關次數： 點閱：1  下載：0 
分享至:
查詢本校圖書館目錄 查詢臺灣博碩士論文知識加值系統 勘誤回報

    • 隨著設計複雜度增加，驗證(verification)已成為電路設計過程中的主要瓶頸之一。研究顯示，驗證可能花費整體電路開發過程的40%~70%的時間。因此，若能有效地加速驗證將可以直接地減少電路開發所花費的時間。在本論文中，我們提出三個邏輯最佳化技術以加速電路驗證程序。
    首先，對於以模擬為基礎的驗證程序，我們提出一個可以簡化限制電路(constraint circuit)的技術。限制電路乃是用於產生合法輸入值給欲驗證的電路(design under verification)。對於限制電路，我們關注的是其所會產生的所有輸出組合(output range)，而非其功能(functionality)。而我們所提出的技術則可以在不改變限制電路的所有輸出組合條件下簡化之(減少輸入與邏輯閘數量)。簡化後的限制電路，可以在相同的運算時間內產生更多不同的合法輸入值，因此可以加速驗證。
    接著，對於以滿足性(satisfiability)為基礎的等效驗證方法，我們提出兩個改變電路架構並簡化電路的技術。首先，我們研究合併電路中兩節點的技術，也就是使用電路中的一節點去取代另一節點。因為，被取代的節點可以被移除而不改變電路的功能，所以此技術可以簡化電路並改變電路架構。接著，我們延伸此節點合併技術，透過加入一節點已取代欲移除的節點。當加入的節點數比移除的節點數少時，此技術一樣可以簡化電路並改變電路架構。我們所提出的方法比過去的技術更有效率，而同時具有相當的電路簡化能力。最後，我們將此兩技術應用於以滿足性為基礎的等效驗證，透用簡化電路並改變電路架構以降低驗證複雜度，而加速驗證時間。結果顯示，我們對於所使用的所有測試電路，總共可以省下27小時的驗證時間。

    With the growth of design complexity, verification has become one of the primary bottlenecks of the design process. Studies show that verification could take 40% to 70% of the total development effort for the design. As a result, reducing verification time directly affects the design cycle. In this dissertation, we propose three logic optimization methods to facilitate verification process.

    We first focus on simulation-based functional verification. A range-equivalent circuit optimization method is proposed to minimize a constraint circuit that is responsible for generating legal input patterns for a design under verification. This method could minimize a constraint circuit while preserving its range such that the pattern generation process could be accelerated and the patterns remain legal. The experimental results show that the proposed method can minimize a benchmark with an average of 37.06% reduction in terms of the number of primary inputs, and an average of 36.31% reduction in terms of the number of nodes. Additionally, each simplified benchmark can generate more output combinations than the non-simplified one for the same random simulation time.

    Next, we focus on satisfiability (SAT)-based equivalence checking. A node-merging method is proposed to merge two nodes (use one node replace another node) in a circuit which are functional equivalent or their functional differences are never observed at any primary output. When two nodes are merged, one of them can be removed from the circuit, and this merger may cause other redundancies in the circuit such that the resultant circuit is minimized. The experimental results show that the proposed method is 46 times faster than a previous method and has a competitive capability of circuit size reduction. Furthermore, a node addition and removal (NAR) method is proposed to enhance the node-merging method. It creates a node merger by adding a node into the circuit. When more than one node is removed due to the addition of the new node, the circuit size is reduced as well. The experimental results show that the optimization capability of the NAR method is better than that of the proposed node-merging method with a ratio of 1.27. The overall CPU time overhead is only 242.8 seconds. We further apply these two methods to facilitate bounded sequential equivalence checking. A total of approximately 27-hour verification time is saved for all the benchmarks.

    Abstract i List of Figures v List of Tables vii 1 Introduction 1 1.1 Range-equivalent circuit minimization . . . . . . . . . . . . . . . . . . 2 1.2 Node merging with don't cares . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Node addition and removal with don't cares . . . . . . . . . . . . . . 8 2 Background 11 3 An implicit approach to minimizing range-equivalent circuits 13 3.1 Range-redundant primary input identification . . . . . . . . . . . . . 13 3.1.1 Stuck-at fault test for a circuit's range . . . . . . . . . . . . . 14 3.1.2 Range mandatory assignments . . . . . . . . . . . . . . . . . . 15 3.2 More range mandatory assignment identification . . . . . . . . . . . . 23 3.2.1 Propagating assignment identification . . . . . . . . . . . . . . 24 3.2.2 COA and NCOA identification . . . . . . . . . . . . . . . . . 25 3.2.3 Range-redundant PI identification algorithm . . . . . . . . . . 27 3.3 Range-preserving simplification . . . . . . . . . . . . . . . . . . . . . 27 3.3.1 Split fanout and merge primary inputs . . . . . . . . . . . . . 27 3.3.2 Overall algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.4 Experimental results . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.4.1 Comparison of simplification capabilities . . . . . . . . . . . . 32 3.4.2 Effect of different orders of removed PIs . . . . . . . . . . . . 34 3.4.3 Generation of output combinations . . . . . . . . . . . . . . . 36 3.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4 Fast node merging with don't cares using logic implications 43 4.1 An example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 4.2 Substitute node identification . . . . . . . . . . . . . . . . . . . . . . 44 4.2.1 Effect of merging two nodes . . . . . . . . . . . . . . . . . . . 45 4.2.2 Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 4.3 Circuit size reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.3.1 Wire replacement . . . . . . . . . . . . . . . . . . . . . . . . . 49 4.3.2 Redundancy removal . . . . . . . . . . . . . . . . . . . . . . . 50 4.3.3 MA reuse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.3.4 Overall algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.4 Experimental results . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 4.4.1 Substitute node identification . . . . . . . . . . . . . . . . . . 53 4.4.2 Circuit size reduction . . . . . . . . . . . . . . . . . . . . . . . 55 4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 5 Node addition and removal in the presence of don't cares 57 5.1 An example of NAR . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 5.2 Node addition and removal . . . . . . . . . . . . . . . . . . . . . . . . 59 5.2.1 Sufficient conditions for NAR . . . . . . . . . . . . . . . . . . 59 5.2.2 Types of added substitute nodes . . . . . . . . . . . . . . . . . 61 5.2.3 NAR algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . 62 5.3 Circuit size reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 5.3.1 Node merging . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 5.3.2 Redundancy removal . . . . . . . . . . . . . . . . . . . . . . . 64 5.3.3 MA reuse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 5.3.4 Overall algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 66 5.4 SAT-based BSEC facilitation . . . . . . . . . . . . . . . . . . . . . . . 68 5.5 Experimental results . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 5.5.1 Replaceable node identification . . . . . . . . . . . . . . . . . 71 5.5.2 Circuit size reduction . . . . . . . . . . . . . . . . . . . . . . . 73 5.5.3 SAT-based BSEC facilitation . . . . . . . . . . . . . . . . . . 75 5.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 6 Conclusion and future work 78 Publication list 86

    [1] M. S. Abadir, J. Ferguson, and T. E. Kirkland, “Logic Design Verification via Test Generation," IEEE Trans. Computer-Aided Design, vol. 7, pp. 138-148, Jan. 1988.
    [2] M. Abramovici, M. A. Breuer, and A. D. Friedman, Digital Systems Testing and Design for Testability, IEEE Press, 1990.
    [3] K. A. Bartlett, R. K. Brayton, G. D. Hachtel, R. M. Jacoby, C. R. Morrison, R. L. Rudell, A. Sangiovanni-Vincentelli and A. R. Wang, “Multilevel Logic Minimization Using Implicit Don't Cares," IEEE Trans. Computer-Aided Design, vol. 7, pp. 723-740, Jun. 1988.
    [4] J. Baumgartner, “Automatic Structural Abstraction Techniques for Enhanced Verification," PhD Thesis, University of Texas, Austin, TX, Chapter 7, Dec. 2002.
    [5] J. Baumgartner and H. Mony, “Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies," in Proc. Int. Conf. on Correct Hardware Design and Verification Methods, 2005, pp. 222-237.
    [6] Berkeley Logic Synthesis and Verification Group, “ABC: A System for Sequential Synthesis and Verification," http://www.eecs.berkeley.edu/~alanmi/abc/.
    [7] C. L. Berman and L. H. Trevillyan, “Functional Comparison of Logic Designs for VLSI Circuits," in Proc. Int. Conf. on Computer-Aided Design, 1989, pp. 456-459.
    [8] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures instead of BDDs," in Proc. Design Automation Conf., 1999, pp. 317-320.
    [9] A. Biere, A. Cimatti, E. M. Clarke, O. Strichmanm and Y. Zhu, “Bounded Model Checking," Advances in Computers, vol. 58, 2003.
    [10] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs," in Proc. Tools and Algorithms for the Construction and Analysis of Systems., 1999, pp. 193-207.
    [11] P. Bjesse and A. Boralv, “DAG-Aware Circuit Compression for Formal Verification", in Proc. Int. Conf. on Computer-Aided Design, 2004, pp. 42-49.
    [12] D. Bostick, G. D. Hachtel, R. Jacoby, M. R. Lightner, P. Moceyunas, C. R. Morrison and D. Ravenscroft “The Boulder Optimal Logic Design System," in Proc. Int. Conf. on Computer-Aided Design, 1987, pp. 62-65.
    [13] R. Bryant, “Graph-based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, vol. 35, pp. 677-691, Aug. 1986.
    [14] M. Case, V. Kravets, A. Mishchenko, and R. Brayton, “Merging Nodes Under Sequential Observability,” in Proc. Design Automation Conf., 2008, pp. 540-545.
    [15] Lynn C. L. Chang, Charles H. P. Wen, and J. Bhadra, “Speeding up Bounded Sequential Equivalence Checking with Cross-Timeframe State-Pair Constraints from Data Learning," in Proc. Int. Test Conf., 2009, pp. 1-8.
    [16] C. W. Jim Chang, M. F. Hsiao, and M. M. Sadowska, “A New Reasoning Scheme for Efficient Redundancy Addition and Removal," IEEE Trans. Computer-Aided Design, vol. 22, pp. 945-952, Jul. 2003.
    [17] S. C. Chang, M. Marek-Sadowska, and K. T. Cheng, “Perturb and Simplify: Multi-level Boolean Network Optimizer," IEEE Trans. Computer-Aided Design, vol. 15, pp. 1494-1504, Dec. 1996.
    [18] S. C. Chang, K. T. Cheng, N. S. Woo, and M. Marek-Sadowska, “Postlayout Logic Restructuring Using Alternative Wires," IEEE Trans. Computer-Aided Design, vol. 16, pp. 587-596, Jun. 1997.
    [19] S. C. Chang, J. C. Chuang, and Z. Z. Wu, “Synthesis for Multiple Input Wires Replacement of a Gate for Wiring Consideration," in Proc. Int. Conf. on Computer-Aided Design, 1999, pp. 115-118.
    [20] S. C. Chang, L. P. P. P. Van Ginneken, and M. M. Sadowska, “Circuit Optimization by Rewiring," IEEE Trans. Computers, vol. 48, pp. 962-970, Sep. 1999.
    [21] Y. C. Chen and C. Y. Wang, “An Improved Approach for Alternative Wire Identification," in Proc. Int. Conf. on Computer Design, 2005, pp. 711-716.
    [22] Y. C. Chen and C. Y. Wang, “An Implicit Approach to Minimizing Range-Equivalent Circuits," IEEE Trans. Computer-Aided Design, vol. 27, pp.1942-1955, Nov. 2008.
    [23] Y. C. Chen and C. Y. Wang, “Fast Detection of Node Mergers Using Logic Implications," in Proc. Int. Conf. on Computer-Aided Design, 2009, pp. 785-788.
    [24] Y. C. Chen and C. Y. Wang, “Fast Node Merging with Don't Cares Using Logic Implications," IEEE Trans. Computer-Aided Design, vol. 29, pp. 1827-1832, Nov. 2010.
    [25] Y. C. Chen and C. Y. Wang, “Node Addition and Removal in the Presence of Don't Cares," in Proc. Design Automation Conf., 2010, pp. 505-510.
    [26] K. T. Cheng and L. A. Entrena, “Multi-level Logic Optimization by Redundancy Addition and Removal," in Proc. European Conf. on Design Automation, 1993, pp. 373-377.
    [27] F. S. Chim, T. K. Lam, and Y. L.Wu, “On Improved Scheme for Digital Circuit Rewiring and Application on Further Improving FPGA Technology Mapping," in Proc. Asia South Pacific Design Automation Conf., 2009, pp. 197-202.
    [28] L. A. Entrena and K. T. Cheng, “Combinational and Sequential Logic Optimization by Redundancy Addition and Removal," IEEE Trans. Computer-Aided Design, vol. 14, pp. 909-916, Jul. 1995.
    [29] T. Kirkland and M. R. Mercer, “A Topological Search Algorithm for ATPG," in Proc. Design Automation Conf., 1987, pp. 502-508.
    [30] A. Kuehlmann, “Dynamic Transition Relation Simplification for Bounded Propery Checking," in Proc. Int. Conf. on Computer-Aided Design, 2004, pp. 50-57.
    [31] A. Kuehlmann and F. Krohm, “Equivalence Checking Using Cuts and Heaps," in Proc. Design Automation Conf., 1997, pp. 263-268.
    [32] A. Kuehlmann, V. Paruthi, F Krohm, and M. K. Ganai, “Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification," IEEE Trans. Computer-Aided Design, vol. 21, pp. 1377-1394, Dec. 2002.
    [33] J. H. Kukula and T. R. Shiple, “Building Circuits from Relations," in Proc. Int. Conf. on Computer Aided Verification, 2000, pp. 131-143.
    [34] W. Kunz and D. K. Pradhan, “Recursive Learning: An Attractive Alternative to the Decision Tree for Test Generation for Digital Circuits," in Proc. Int. Test Conf., 1992, pp. 816-825.
    [35] C. C. Lin and C. Y. Wang, “Rewiring Using Irredundancy Removal and Addition," in Proc. Design, Automation and Test in Europe, 2009, pp. 324-327.
    [36] W. H. Lo and Y. L. Wu, “Improving Single-Pass Redundancy Addition and Removal with Inconsistent Assignments," in Proc. Int. Symp. on VLSI Design, Automation and Test, 2006, pp. 175-178.
    [37] Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits," in Proc. Design Automation Conf., 1996, pp. 629-634.
    [38] A. Mishchenko, S. Chatterjee, and R. Brayton, “DAG-Aware AIG Rewriting: A Fresh Look at Combinational Logic Synthesis," in Proc. Design Automation Conf., 2006, pp. 532-536.
    [39] A. Mishchenko, S. Chatterjee, R. Brayton, and N. Een, “Improvements to Combinational Equivalence Checking, " in Proc. Int. Conf. on Computer-Aided Design, 2006, pp. 836-843.
    [40] I. H. Moon, H. H. Kwak, J. Kukula, T. Shiple and C. P, “Simplify Circuits for Formal Verification Using Parametric Representation," in Proc. Int. Conf. on Formal Methods in Computer Aided Design, 2002, pp. 52-69.
    [41] J. Moondanos, C. H. Seger, Z. Hanna, and D. Kaiss, “CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination," in Proc. Int. Computer Aided Verification Conf., 2001, pp. 131-143.
    [42] S. Plaza, K. H. Chang, I. Markov, and V. Bertacco, “Node Mergers in the Presence of Don't Cares," in Proc. Asia South Pacific Design Automation Conf., 2007, pp. 414-419.
    [43] H. Savoj, R. K. Brayton and H. J. Touati, "Extracting Local Don't Cares for Network Optimization," in Proc. Int. Conf. on Computer-Aided Design, 1991, pp. 514-517.
    [44] M. H. Schulz amd E. Auth, “Advanced Automatic Test Pattern Generation and Redundancy Identification Techniques," in Proc. Int. Fault-Tolerant Computing Symp., 1988, pp. 30-35.
    [45] E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton, and A. Sangiovanni-Vincentelli, “SIS: A System for Sequential Circuit Synthesis," Technical Report UCB/ERL M92/41, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, May 1992.
    [46] K. Shimizu and D. L. Dill, “Deriving a Simulation Input Generator and a Coverage Metric From a Formal Specification," in Proc. Design Automation Conf., 2002, pp. 801-806.
    [47] D. Stoffel, M.Wedler, P.Warkentin, and W. Kunz, “Structural FSM Traversal," IEEE Trans. Computer-Aided Design, vol. 23, pp. 598-619, May 2004.
    [48] A. Veneris and M. S. Abadir, “Design Rewiring Using ATPG," IEEE Trans. Computer-Aided Design, vol. 21, pp. 1469-1479, Dec. 2002.
    [49] C. A. Wu, T. H. Lin, S. L. Huang, and C. Y. Huang, “SAT-Controlled Redundancy Addition and Removal － A Novel Circuit Restructuring Technique," in Proc. Asia South Pacific Design Automation Conf., 2009, pp. 191-196.
    [50] W. Wu and M. S. Hsiao, “Mining Global Constraints With Domain Knowledge for Improving Bounded Sequential Equivalence Checking," IEEE Trans. Computer-Aided Design, vol. 27, pp. 197-201, Jan. 2008.
    [51] Y. L. Wu, W. Long, and H. Fan, “A Fast Graph-based Alternative Wiring Scheme for Boolean Networks," in Proc. Int. VLSI Design Conf., 2000, pp. 268-273.
    [52] Y. L. Wu, C. C. Cheung , D. I. Cheng , H. Fan, “Further Improve Circuit Partitioning Using GBAW Logic Perturbation Techniques," IEEE Trans. Very Large Scale Integration Systems, vol. 11, pp. 451-460, Jun. 2003.
    [53] X. Q. Yang, T. K. Lam, and Y. L. Wu, “ECR: A Low Complexity Generalized Error Cancellation Rewiring Scheme," in Proc. Design Automation Conf., 2010, pp. 511-516.
    [54] J. Yuan, K. Albin, A. Aziz and C. Pixley, “Constraint Synthesis for Environment Modeling in Functional Verification," in Proc. Design Automation Conf., 2003, pp. 296-299.
    [55] J. Yuan, K. Shultz, C. Pixley, H. Miller, and A. Aziz, “Modeling Design Constraints and Biasing in Simulation Using BDDs," in Proc. Int. Conf. on Computer-Aided Design, 1999, pp. 584-589.
    [56] F. Zaraket, J. Baumgartner and A. Aziz, “Scalable Compositional Minimization via Static Analysis," in Proc. Int. Conf. on Computer-Aided Design, 2005, pp. 1060-1067.
    [57] Q. Zhu, N. Kitchen, A. Kuehlmann, and A. Sangiovanni-Vincentelli, “SAT Sweeping with Local Observability Don't Cares," in Proc. Design Automation Conf., 2006, pp. 229-234.
    [58] http://iwls.org/iwls2005/benchmarks.html.
    [59] http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

    無法下載圖示 全文公開日期 本全文未授權公開 (校內網路)
    全文公開日期 本全文未授權公開 (校外網路)

    QR CODE