跳到主要內容

臺灣博碩士論文加值系統

(34.204.180.223) 您好!臺灣時間:2021/07/31 18:04
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:范寬
研究生(外文):Kuan Fan
論文名稱:利用邏輯閘層級抽象化技術增進性質導向可達性技術
論文名稱(外文):Improving Property Directed Reachability Using Gate-Level Abstraction
指導教授:黃鐘揚
口試委員:江介宏王柏堯吳政穎
口試日期:2015-07-06
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電子工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2015
畢業學年度:103
語文別:英文
論文頁數:41
中文關鍵詞:性質導向可達性技術邏輯閘層級抽象化技術
外文關鍵詞:Property Directed ReachabilityGate-Level Abstraction
相關次數:
  • 被引用被引用:0
  • 點閱點閱:73
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
性質導向可達性技術是一種高效的模型驗證演算法。然而,對於大規模集成電路的驗證,設計邏輯的複雜性可能會阻礙性質導向可達性技術建構可達性之抽象,導致未能成功證明。在本篇論文中,我們提出了整合性質導向可達性技術與邏輯閘級,混合抽象技術,這使得性質導向可達性技術成為更具擴展性的模型驗證方法。我們將此技術實作於ABC且評估其效能於HWMCC13,HWMCC14。我們的實驗結果顯示,該方法顯著優於典型的性質導向可達性技術且與其有可觀的互補性。

Property directed reachability(PDR aka IC3) is an efficient and complete model checking procedure. However, for large problems, the complexities of design logic might hinder PDR from construction of over-approximations, leading to failure to prove them. In this thesis, we present a novel model-checking technique that integrates PDR/IC3 with gate-level, hybrid abstraction, which makes PDR a more scalable model checking method. We implemented the technique in ABC and evaluated it on the HWMCC13, HWMCC14 benchmark suites. Our results show that the proposed method significantly outperforms standard PDR and complements it on a large number of benchmark instances.

口試委員會審定書 i
誌謝 ii
中文摘要 iii
英文摘要 iv
1 Introduction 1
1.1 Relatedwork ................................ 4
2 Preliminaries 5
2.1 Propositional Satisfiability ......................... 5
2.2 Finite State Transition System ....................... 5
2.3 Property Directed Reachability....................... 6
2.4 Abstraction Methods and Abstract Transition System . . . . . . . . . . . 11
2.5 GLA—Gate-level,Hybrid Abstraction................... 13
3 Abstract Model Checking via PDR and GLA 16
3.1 Main Algorithm............................... 16
3.2 Abstract Counterexamples Refinement................... 21
3.3 UNSAT Cores Extraction.......................... 21
3.4 Soundness and Completeness........................ 22
3.5 Implementation Details........................... 23
4 Experimental Results.............26
5 Conclusions and Future Work................39
References................40

[1] P. Chauhan, E. Clarke, J. Kukula, S. Sapra, H. Veith, and D. Wang, “Automated abstraction refinement for model checking large state spaces using sat based conflict analysis,” in Formal Methods in Computer-Aided Design, pp. 33–51, Springer, 2002.
[2] K. L. McMillan and N. Amla, “Automatic abstraction without counterexamples,” in Tools and Algorithms for the Construction and Analysis of Systems, pp. 2–17, Springer, 2003.
[3] N. Amla and K. L. McMillan, “A hybrid of counterexample-based and proof-based abstraction,” in Formal Methods in Computer-Aided Design, pp. 260–274, Springer, 2004.
[4] 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.
[5] A.R.Bradley,“Sat-basedmodelcheckingwithoutunrolling,”inVerification,Model Checking, and Abstract Interpretation, pp. 70–87, Springer, 2011.
[6] A. Mishchenko, N. Een, R. Brayton, J. Baumgartner, H. Mony, and P. Nalla, “Gla: gate-level abstraction revisited,” in Proceedings of the Conference on Design, Au- tomation and Test in Europe, pp. 1399–1404, EDA Consortium, 2013.
[7] B. L. Synthesis and V. Group, “Abc a system for sequential synthesis and verifica- tion.”
[8] S. Lee and K. A. Sakallah, “Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction,” in Computer Aided Verifi- cation, pp. 849–865, Springer, 2014.
[9] Y. Vizel, O. Grumberg, and S. Shoham, “Lazy abstraction and sat-based reacha- bility in hardware model checking,” in Formal Methods in Computer-Aided Design (FMCAD), 2012, pp. 173–181, IEEE, 2012.
[10] R. P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton university press, 2014.
[11] A. Mishchenko, N. Een, R. Brayton, J. Baumgartner, H. Mony, and P. Nalla, “Vari- able time-frame abstraction,” in in IWLS, Citeseer, 2012.
[12] N. Een, A. Mishchenko, and N. So ̈rensson, “Applying logic synthesis for speeding up sat,” in Theory and Applications of Satisfiability Testing–SAT 2007, pp. 272–286, Springer, 2007.
[13] Z. Hassan, A. R. Bradley, and F. Somenzi, “Better generalization in ic3,” in Formal Methods in Computer-Aided Design (FMCAD), 2013, pp. 157–164, IEEE, 2013.

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關論文
 
1. 5.張龍文,論公同共有(原載法學叢刊第四期,1956年10月),收錄於鄭玉波主編,民法物權論文選輯,五南圖書公司,頁417-432。
2. 7.陳和慧,論共有物分割,(原載法令月刊第二十四卷第五期,1973年5月),收錄於鄭玉波主編,民法物權論文選輯,五南圖書公司,頁332-347,1984年7月。
3. 12.開正懷,共有物協議分割抑判決分割,我亦曰處分行為,(原載法令月刊第三十卷第十期,1979年10月),收錄於鄭玉波主編,民法物權論文選輯,五南圖書公司,頁359-368,1984年7月。
4. 14.楊與齡,論共有物之分割,(原載法學叢刊第三十二期,1963年10月),收錄於鄭玉波主編,民法物權論文選輯,五南圖書公司,頁348-358,1984年7月。
5. 15.謝在全,分別共有之內部關係,(原載法學叢刊106期,1982年4月),收錄於鄭玉波主編,民法物權論文選輯,五南圖書公司,頁302-331,1984年7月。
6. 1.王文宇,物權法定原則與物權債權區分-兼論公示登記制度,月旦法學雜誌(NO﹒93),頁138-165,2003年1月。
7. 4.何宇明,工地使用與交易成本,中國工商學報第十八期,頁301-305,1996年6月。
8. 5.吳明軒,試論不動產分割之訴,月旦法學雜誌第八十一期,頁77-91,2002年2月。
9. 6.吳明軒,試論共有不動產之協議分割,中華法學第七期,頁19-31,1997年4月。
10. 7.吳明軒,請求履行共有協議分割契約之訴,月旦法學教室第五十一期,2007年1月。
11. 8.吳家慶,論形成權,警專學報,第貳卷第五期,頁65-88,1998年6月。
12. 9.吳清輝,論土地問題的本質與根源,土地問題研究季刊NO.1.,頁19-27,2002年3月。
13. 10.巫惠玲,共有物分割爭議處理之探討,現代地政,頁28-33,2001年3月。
14. 14.林英彥,論正常價格與限定價格,土地問題研究季刊NO.6.,頁84-86,2003年6月。
15. 15.林修正,土地增值稅與土地利用之關係,中州學報第十七期,頁143-151,2003年6月。
 
無相關點閱論文