文献

J-GLOBAL ID：201702247094251020   整理番号：17A0980550

多様なSATソルバーを用いたカバレッジ駆動型設計検証

Coverage-Driven Design Verification Using a Diverse SAT Solver

著者 (2件)： KAKIUCHI Yosuke (Department of Computer Science, Faculty of Applied Information Science, Hiroshima Institute of Technology) ,  HAMAGUCHI Kiyoharu (Department of Mathematics and Computer Science, Shimane University)
資料名： IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences (Web)  (IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences (Web))
巻： E100.A  号： 7  ページ： 1481-1487(J-STAGE)  発行年： 2017年 
JST資料番号： U0466A  ISSN： 1745-1337  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 英語 (EN)

抄録/ポイント： 論理設計の検証は,自動化と効率向上が厳しいニーズを伴うハードウェア設計プロセスにおいて長年のボトルネックである。このために,主にシミュレーションに基づく検証が用いられ,最近,カバレッジ駆動検証が広く利用され,その対象はカバレッジと呼ばれるいくつかの性能指標の改善である。本文の目標はトグルカバレッジと呼ぶ指標とし,各信号にあるトグルを引き起こす入力パターンを見付けるために,充足可能性(SAT)ソルバを用いることができるが,これは計算時間が掛る。本文は,ランダムシミュレーションとSATソルバの併用効果を検討した。特に,複数の「多様な」解を見付けられるSATソルバを用いる。このソルバを用いて類似パターンの生成は回避できるが,カバレッジの改善は見込めない。SATソルバーの呼出しが少数なら,簡単なランダムシミュレーションと比べ,トグルカバレッジ全体を効果的に改善できることを実験結果で示した。(翻訳著者抄録)

シソーラス用語： *集積回路 ,  *論理回路 ,  *論理設計 ,  *検証 ,  充足可能性問題 ,  応用プログラム ,  *自動試験 ,  検査
準シソーラス用語： RTL ,  ソルバ ,  テストベンチ ,  *設計検証

著者キーワード (4件)： RTL verification ,  coverage-driven verification ,  sat solver ,  auomated testbench

分類 (2件)： 集積回路一般  (NC03161C) ,  論理回路  (NC05070B)

引用文献 (16件)：

• [1] A. Nadel, “Generating diverse solutions in SAT,” Theory and Applications of Satisfiability Testing-SAT, pp.287-301, 2011. 10.1007/978-3-642-21581-0_23
• [2] S. Yang, R. Wille, and R. Drechsler, “Determining cases of scenarios to improve coverage in simulation-based verification,” Symp. on Integrated Circuits and System Design, 2014. 10.1145/2660540.2660979
• [3] S. Yang, R. Wille, D. Große, and R. Drechsler,“Coverage-driven stimuli generation,” EUROMICRO Symp. on Digital System Design, pp.525-528, 2012. 10.1109/dsd.2012.37
• [4] S. Chakraborty, K.S. Meel, and M.Y. Vardi, “A scalable and nearly uniform generator of SAT witnesses,” Computer-Aided Verification, pp.608-623, 2013. 10.1007/978-3-642-39799-8_40
• [5] I. Wagner, V. Bertacco, and T. Austin, “Microprocessor verification via feedback-adjusted Markov models,” IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol.26, no.6, pp.1126-1138, 2007. 10.1109/tcad.2006.884494

タイトルに関連する用語 (4件)： SAT ,  ソルバー ,  カバレッジ ,  設計検証