請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/5540
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 黃鐘揚(Chung-Yang (Ric) | |
dc.contributor.author | Cheng-Yin Wu | en |
dc.contributor.author | 吳政穎 | zh_TW |
dc.date.accessioned | 2021-05-15T18:02:12Z | - |
dc.date.available | 2014-08-21 | |
dc.date.available | 2021-05-15T18:02:12Z | - |
dc.date.copyright | 2014-08-21 | |
dc.date.issued | 2014 | |
dc.date.submitted | 2014-08-19 | |
dc.identifier.citation | [1] E. M. Clarke, O. Grumberg, and D. Peled, Model checking. MIT press, 1999.
[2] K. L. McMillan, Symbolic model checking. Springer, 1993. [3] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without bdds,” Tools and Algorithms for the Construction and Analysis of Systems, pp. 193– 207, 1999. [4] M. Sheeran, S. Singh, and G. St°almarck, “Checking safety properties using induction and a sat-solver,” in Formal Methods in Computer-Aided Design, pp. 127–144, Springer, 2000. [5] N. E’en and N. S‥orensson, “Temporal induction by incremental sat solving,” Electronic Notes in Theoretical Computer Science, vol. 89, no. 4, pp. 543–560, 2003. [6] K. McMillan, “Interpolation and sat-based model checking,” in Computer Aided Verification, pp. 1–13, Springer, 2003. [7] H. Jain, D. Kroening, N. Sharygina, and E. Clarke, “Vcegar: Verilog counterexample guided abstraction refinement,” Tools and Algorithms for the Construction and Analysis of Systems, pp. 583–586, 2007. [8] A. Bradley, “Sat-based model checking without unrolling,” in Verification, Model Checking, and Abstract Interpretation, pp. 70–87, Springer, 2011. [9] N. Een, A. Mishchenko, and R. Brayton, “Efficient implementation of property directed reachability,” in Formal Methods in Computer-Aided Design (FMCAD), 2011, pp. 125–134, IEEE, 2011. [10] C.-Y. Wu, C.-A. Wu, C.-Y. Lai, and C.-Y. Huang, “A counterexample-guided interpolant generation algorithm for sat-based model checking,” in Design Automation Conference (DAC), 2013 50th ACM/EDAC/IEEE, pp. 1–6, IEEE, 2013. [11] A. R. Bradley, F. Somenzi, Z. Hassan, and Y. Zhang, “An incremental approach to model checking progress properties,” in Formal Methods in Computer-Aided Design (FMCAD), 2011, pp. 144–153, IEEE, 2011. [12] K. Claessen and N. S‥orensson, “A liveness checking algorithm that counts.,” in FMCAD, pp. 52–59, 2012. [13] A. Biere, “The aiger and-inverter graph (aig) format,” Available at fmv. jku. at/aiger, 2007. [14] D. Thomas and P. Moorby, The Verilog R Hardware Description Language, vol. 2. Springer, 2002. [15] “Ieee standard for system verilog-unified hardware design, specification, and verification language,” IEEE STD 1800-2009, pp. C1 –1285, 2009. [16] H.-H. Yeh, C.-Y. Wu, and C.-Y. Huang, “Property-specific sequential invariant extraction for sat-based unbounded model checking,” in Proceedings of the International Conference on Computer-Aided Design, pp. 674–678, IEEE Press, 2010. [17] G. Cabodi and S. Nocco, “Optimized model checking of multiple properties,” in Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011, pp. 1–4, IEEE, 2011. [18] G. Cabodi, S. Nocco, and S. Quer, “Thread-based multi-engine model checking for multicore platforms,” ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 18, no. 3, p. 36, 2013. [19] R. Brayton and A. Mishchenko, “Abc: An academic industrial-strength verification tool,” in Computer Aided Verification, pp. 24–40, Springer, 2010. [20] “Hardware Model Checking Competition,” http://fmv.jku.at/hwmcc/. [21] H.-H. Yeh, C.-Y.Wu, and C.-Y. Huang, “Qutertl: towards an open source framework for rtl design synthesis and verification,” Tools and Algorithms for the Construction and Analysis of Systems, pp. 377–391, 2012. [22] R. Brummayer, A. Biere, and F. Lonsing, “Btor: bit-precise modelling of wordlevel problems for model checking,” in Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, pp. 33–38, ACM, 2008. [23] A. Biere, K. Heljanko, and S. Wieringa, “Aiger 1.9 and beyond,” Available at fmv.jku.at/hwmcc11/beyond1.pdf, 2011. [24] M. N.Wegman and F. K. Zadeck, “Constant propagation with conditional branches,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 13, no. 2, pp. 181–210, 1991. [25] O. Coudert, C. Berthet, and J. C. Madre, “Verification of synchronous sequential machines based on symbolic execution,” in Automatic verification methods for finite state systems, pp. 365–373, Springer, 1990. [26] A. Kuehlmann, V. Paruthi, F. Krohm, and M. Ganai, “Robust boolean reasoning for equivalence checking and functional property verification,” Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, vol. 21, no. 12, pp. 1377– 1394, 2002. [27] R. Brummayer and A. Biere, “Boolector: An efficient smt solver for bit-vectors and arrays,” Tools and Algorithms for the Construction and Analysis of Systems, pp. 174–177, 2009. [28] A. Biere, C. Artho, and V. Schuppan, “Liveness checking as safety checking,” Electronic Notes in Theoretical Computer Science, vol. 66, no. 2, pp. 160–177, 2002. [29] A. Mishchenko, M. Case, R. Brayton, and S. Jang, “Scalable and scalably-verifiable sequential synthesis,” in Computer-Aided Design, 2008. ICCAD 2008. IEEE/ACM International Conference on, pp. 234–241, IEEE, 2008. [30] R. Armoni, L. Fix, R. Fraer, T. Heyman, M. Vardi, Y. Vizel, and Y. Zbar, “Deeper bound in bmc by combining constant propagation and abstraction,” in Design Automation Conference, 2007. ASP-DAC’07. Asia and South Pacific, pp. 304–309, IEEE, 2007. [31] G. S. Tseitin, “On the complexity of derivation in propositional calculus,” in Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970 (J. Siekmann and G. Wrightson, eds.), pp. 466–483, Berlin, Heidelberg: Springer, 1983. [32] D. A. Plaisted and S. Greenbaum, “A structure-preserving clause form translation,” Journal of Symbolic Computation, vol. 2, no. 3, pp. 293–304, 1986. [33] S. A. Cook, “The complexity of theorem-proving procedures,” in Proceedings of the third annual ACM symposium on Theory of computing, pp. 151–158, ACM, 1971. [34] N. E’en and N. S‥orensson, “An extensible sat-solver,” in Theory and Applications of Satisfiability Testing, pp. 333–336, Springer, 2004. [35] A. Biere, “Picosat essentials.,” JSAT, vol. 4, no. 2-4, pp. 75–97, 2008. [36] A. Biere, “Lingeling, plingeling, picosat and precosat at sat race 2010,” FMV Report Series Technical Report, vol. 10, no. 1, 2010. [37] G. Audemard and L. Simon, “Predicting learnt clauses quality in modern sat solvers.,” in IJCAI, vol. 9, pp. 399–404, 2009. [38] M. Soos, “Cryptominisat 2.5. 0,” SAT Race competitive event booklet, 2010. [39] E. Clarke, O. Grumberg, and D. Long, “Model checking and abstraction,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 16, no. 5, pp. 1512–1542, 1994. [40] A. Mishchenko, S. Chatterjee, R. Jiang, and R. K. Brayton, “Fraigs: A unifying representation for logic synthesis and verification,” tech. rep., ERL Technical Report, 2005. [41] A. Mishchenko, S. Chatterjee, and R. Brayton, “Dag-aware aig rewriting a fresh look at combinational logic synthesis,” in Proceedings of the 43rd annual Design Automation Conference, pp. 532–535, ACM, 2006. [42] A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani, “The mathsat5 smt solver,” Tools and Algorithms for the Construction and Analysis of Systems, 2013. [43] L. De Moura and N. Bjorner, “Z3: An efficient smt solver,” Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340, 2008. [44] H. Jain, D. Kroening, N. Sharygina, and E. Clarke, “Word level predicate abstraction and refinement for verifying rtl verilog,” in Proceedings of the 42nd annual Design Automation Conference, pp. 445–450, ACM, 2005. [45] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement,” in Computer Aided Verification, pp. 154–169, Springer, 2000. [46] M. L. Case, A. Mishchenko, and R. K. Brayton, “Automated extraction of inductive invariants to aid model checking,” in Formal Methods in Computer Aided Design, 2007. FMCAD’07, pp. 165–172, IEEE, 2007. [47] J. Giomi, “Finite state machine extraction from hardware description languages,” in ASIC Conference and Exhibit, 1995., Proceedings of the Eighth Annual IEEE International, pp. 353–357, IEEE, 1995. [48] J. Giomi, “Method of extracting implicit sequential behavior from hardware description languages,” June 30 1998. US Patent 5,774,370. [49] K. Nanshi and F. Somenzi, “Guiding simulation with increasingly refined abstract traces,” in Proceedings of the 43rd annual Design Automation Conference, pp. 737– 742, ACM, 2006. [50] J. Baumgartner and H. Mony, “Maximal input reduction of sequential netlists via synergistic reparameterization and localization strategies,” in Correct Hardware Design and Verification Methods, pp. 222–237, Springer, 2005. [51] P. Bjesse and J. Kukula, “Automatic generalized phase abstraction for formal verification,” in Computer-Aided Design, 2005. ICCAD-2005. IEEE/ACM International Conference on, pp. 1076–1082, IEEE, 2005. [52] C. E. Leiserson and J. B. Saxe, “Retiming synchronous circuitry,” Algorithmica, vol. 6, no. 1-6, pp. 5–35, 1991. [53] A. Biere, “Lingeling, plingeling and treengeling entering the sat competition 2013,” Proceedings of SAT Competition, pp. 51–52, 2013. [54] H. Mony, J. Baumgartner, V. Paruthi, and R. Kanzelman, “Exploiting suspected redundancy without proving it,” in Proceedings of the 42nd annual Design Automation Conference, pp. 463–466, ACM, 2005. [55] R. Tarjan, “Depth-first search and linear graph algorithms,” SIAM journal on computing, vol. 1, no. 2, pp. 146–160, 1972. [56] “OpenCores,” http://opencores.org/. [57] “VIS Verification Benchmarks,” http://vlsi.colorado.edu/ vis/. [58] “Standard template library programmer’s guide,” https://www.sgi.com/tech/stl/. [59] “Technical report on c++ library extensions,” http://www.openstd. org/jtc1/sc22/wg21/docs/papers/2005/n1836.pdf. [60] “Synopsys Verdi,” https://www.synopsys.com. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/5540 | - |
dc.description.abstract | 模型檢驗(亦稱為屬性檢驗)是一種典型的方法用以正規地驗證一個硬體系
統。給定一個硬體系統與一組屬性,模型檢驗演算法將斷定該系統滿足以及不滿 足哪些屬性。然而隨著設計複雜度不斷地提高以及所需檢驗的屬性數量隨之增 加,模型檢驗的能力將因其本身的高複雜度而下降。 在這篇博士論文中我們發表了一個工具適用於暫存器轉移階層硬體系統的模 型檢驗。該工具包含了以下三個部分:正規模型、前端處理、以及模型檢驗。首 先正規模型將對一個複雜的暫存器轉移階層硬體系統進行解析與合成,最後將它 表示成一個文字階層的電路。其次,在前端處理中我們將該電路進行改寫以及重 新合成,並進一步從該電路的抽象層面抽取與所需檢驗之屬性相關的條件與恆真 屬性,以促進模型檢驗。在前端處理最後所需驗證之屬性都將被合成之後。在模 型檢驗階段,我們設計了一個組合式的模型檢驗器用以檢驗所有的屬性。特別的 是,各式各樣的屬性檢驗演算法將在第一時間互相分享彼此獲得的情報(例如: 已知最深的臨界,以及計算出可達到之範圍等等),以彌補單一演算法能力之不 足。我們採用了數個暫存器轉移階層的驗證問題作為實驗的對象,而實驗結果說 明了我們所提出的技術讓我們的驗證工具能夠有效地處理包含數千個屬性的複雜 模型檢驗問題。 | zh_TW |
dc.description.abstract | Model checking, or property checking, is a classic methodology for formally verifying a hardware system. More specifically, given a system and a set of properties, model
checkers judge whether the system satisfies a property or not. However, due to the high complexity of model checking, as the design complexity and the number of property to be verified grows rapidly, the capability of model checking decreases. In this thesis, we present a complete framework for model checking of RT-level hardware systems. The framework consists of three major building blocks: FORMAL MODELING, PREPROCESSING, and MODEL CHECKING. Starting from FORMAL MODELING, a complicated RT-level design is parsed, synthesized, and then modeled as a word-level network. Next in the PREPROCESSING stage, rewriting and resynthesis techniques are applied to optimize the network, and moreover, property-directed constraints and invariants are extracted from design abstraction for improving model checking. After properties are elaborated at the end of PREPROCESSING, a portfolio-based model checker starts to verify all the properties in the MODEL CHECKING stage, and in particular, different model checking algorithms share information (e.g. deep bounds and reachabilities) on-the-fly to complement each other. Our experimental evaluation shows that our framework, equipped with abovementioned techniques, is capable of model checking RT-level benchmarks with thousands of properties efficiently. | en |
dc.description.provenance | Made available in DSpace on 2021-05-15T18:02:12Z (GMT). No. of bitstreams: 1 ntu-103-D99943034-1.pdf: 6025400 bytes, checksum: ad6eb178c109811d01dc15719b9b59af (MD5) Previous issue date: 2014 | en |
dc.description.tableofcontents | 1 Introduction 1
2 Preliminaries 8 2.1 Register Transfer Level (RT-Level) Hardware Description Language . . . 8 2.2 Word-level Network . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3 Propositional Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.4 Transition System of a Network . . . . . . . . . . . . . . . . . . . . . . 12 2.5 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.5.1 Property Specification . . . . . . . . . . . . . . . . . . . . . . . 13 2.5.2 Safety Property Checking . . . . . . . . . . . . . . . . . . . . . 15 2.5.3 Liveness Property Checking . . . . . . . . . . . . . . . . . . . . 18 2.6 Abstract Transition System . . . . . . . . . . . . . . . . . . . . . . . . . 20 3 Formal Modeling of RT-level Hardware Systems 22 3.1 Front-end Modeling of RT-Level Hardware Systems . . . . . . . . . . . . 23 3.2 The Construction of a Word-level Network for Verification . . . . . . . . 25 3.2.1 Signals and Flip-Flops of a Network . . . . . . . . . . . . . . . . 26 3.2.2 Operators in a Network . . . . . . . . . . . . . . . . . . . . . . . 26 3.2.3 Representation of a Network . . . . . . . . . . . . . . . . . . . . 28 3.2.4 The Construction of Word-level Networks from QuteRTL . . . . 30 3.3 Property Elaboration . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3.1 Addressing Invariant Constraints . . . . . . . . . . . . . . . . . . 32 3.3.2 Liveness Checking as Safety Checking . . . . . . . . . . . . . . 34 3.4 Optimizing the Elaborated Network . . . . . . . . . . . . . . . . . . . . 37 3.4.1 Cone-of-Influence Reduction . . . . . . . . . . . . . . . . . . . . 38 3.4.2 Structural Hashing . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.4.3 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.4.4 Bit-Blasting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4 Preprocessing Techniques Toward Verification Instance Optimization 42 4.1 Extracting Property-directed Invariant for Safety Properties . . . . . . . . 43 4.1.1 Combinational and Sequential Invariants . . . . . . . . . . . . . 43 4.1.2 The Construction of Abstract Transition Systems . . . . . . . . . 45 4.1.3 Extracting Invariants from Abstract Transition Systems . . . . . . 56 4.2 Extracting Fairness Constraints for Liveness Properties . . . . . . . . . . 58 5 A Portfolio-based Model Checker for Checking Single Property 61 5.1 Hardware Model Checking: Trends and Facts . . . . . . . . . . . . . . . 62 5.1.1 Problem Formulation to a Single Property Checking Instance . . . 63 5.1.2 Existing Approaches to Single Property Checking . . . . . . . . . 64 5.2 Towards an Efficient Portfolio-based Model Checker for Single Property Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 5.2.1 An Overview of Our Portfolio-based Model Checker . . . . . . . 67 5.2.2 Model Checking Algorithms: Comparisons, Analyses, and Summaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.2.3 Model Checking Cloud: A Platform for Information Sharing . . . 73 5.2.4 The Resource Control Mechanism . . . . . . . . . . . . . . . . . 76 6 A Portfolio-based Model Checker for Checking Multiple Properties 81 6.1 The Differences between Checking Multiple Properties and Single Property 82 6.1.1 A Summary to The Multiple Property Track of HWMCC . . . . . 82 6.1.2 Practical Issues to Model Checking Multiple Properties . . . . . . 84 6.2 Towards a High-throughput Portfolio-based Model Checker for Multiple Property Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 6.2.1 Property Reordering . . . . . . . . . . . . . . . . . . . . . . . . 88 6.2.2 Model Checking Cloud Revisited . . . . . . . . . . . . . . . . . 93 6.2.3 More on the Resource Control Mechanism . . . . . . . . . . . . 95 6.3 Incremental Model Checking: Never Start-over . . . . . . . . . . . . . . 98 6.3.1 Making a Model Checking Procedure Incremental . . . . . . . . 99 6.3.2 Rendering a Model Checking Algorithm Incremental . . . . . . . 100 7 Experimental Evaluation 106 7.1 Experimental Evaluation of Formal Modeling . . . . . . . . . . . . . . . 108 7.2 Experimental Evaluation of Preprocessing . . . . . . . . . . . . . . . . . 112 7.2.1 The Effect of Property-directed Invariants to Safety Checking . . 113 7.2.2 The Effect of Fairness Constraints to Liveness Checking . . . . . 117 7.3 Experimental Evaluation of Single Property Checking . . . . . . . . . . . 120 7.3.1 Effect of Shared Information to Runtime Performance . . . . . . 121 7.3.2 Effect of Shared Information to Deep Bound . . . . . . . . . . . 124 7.4 Experimental Evaluation of Multiple Property Checking . . . . . . . . . 125 7.4.1 A Toolbox for Property Generation . . . . . . . . . . . . . . . . 125 7.4.2 The Result of Multiple Property Checking . . . . . . . . . . . . . 130 8 Conclusions and Future Work 135 References 138 | |
dc.language.iso | en | |
dc.title | 暫存器轉移階層硬體系統模型檢驗 | zh_TW |
dc.title | Model Checking RT-Level Hardware Systems | en |
dc.type | Thesis | |
dc.date.schoolyear | 102-2 | |
dc.description.degree | 博士 | |
dc.contributor.oralexamcommittee | 江介宏(Jie-Hong (Roland),李建模(Chien-Mo (James),王凡(Farn Wang),王柏堯(Bow-Yaw Wang),顏嘉志(Chia-Chih Yen) | |
dc.subject.keyword | 正規驗證,硬體模型檢驗, | zh_TW |
dc.subject.keyword | Formal Verification,Hardware Model Checking, | en |
dc.relation.page | 145 | |
dc.rights.note | 同意授權(全球公開) | |
dc.date.accepted | 2014-08-20 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-103-1.pdf | 5.88 MB | Adobe PDF | 檢視/開啟 |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。