研究シーズ集

情報・通信 ---------------------------- 2024-16 濵口　清治　教授 ハードウェア論理設計の正しさを検証する 工学部情報工学科 ■研究業績等 【著書】 ・著書『システムLSI設計工学』オーム社(共著):2006/10 ・著書『超並列計算講義』共立出版(共著):1996/06 【論文】 ・学術論文「Parallelizing Random and SAT-based Verification Processes for Improving Toggle Coverage」IPSJ Transactions on System and LSI Design Methodology Information Processing Society of Japan 16:45-53(単著):2023/06 ・学術論文「Applying an SMT Solver to Coverage-driven Design Verification(カバレッジ駆動型設計検証へのSMTソルバの適用)」IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences Vol.E101-A(No.07):pp.1053-1056(単著):2018/07 ・学術論文「Coverage-driven Design Verification Using a Diverse SAT Solver(ダイバースSATソルバーを用いたカバレッジ駆動型設計検証)」IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences Vol.E100-A(No.07):pp.1481-1487(共著):2017/07 【学会発表】 ・Error Detection Capacity of SAT-based Coverage-driven Design Verification(2021 Synthesis and Simulation Meeting and International Interchange):2021/03 ・Parallelizing SAT-based Coverage-Driven Design Verification(2019 Synthesis and Simulation Meeting and International Interchange):2019/10 ・正規表現照合器の複数サイクル状態遷移に着目したFPGA実装とその評価(LSIとシステムのワークショップ2019):2019/05 機械学習技術やIoTシステムの普及とともに消費電力削減また計算速度の向上を目標として、多種多様な回路設計がFPGA上または専用回路として実現されるようになってきています。手数の多い論理・レジスタ転送レベルでの設計検証を、可能なかぎり自動化することを目標として研究を行っています。特に通常のシミュレーション技術に加えて、SATソルバ(Satisfiability Solver, 論理式の充足可能性判定器)を併用した手法について研究を行ってきており、特定用途に限らない設計を扱う点を特徴のひとつとしています。枠組みとしてはカバレッジと呼ばれる数値的指標の改善を目標としたカバレッジ駆動検証手法を取り扱っています。種々のカバレッジ、とくにトグルカバレッジやクロスカバレッジの改善と高速化を目指しつつ、設計誤りの検出率の実験的評価も行って、より実用的な設計検証システムの実現を狙っています。 VerilogやVHDLなどのハードウェア記述言語で記述されたゲートレベルやレジスタ転送レベルの設計に対して、その動作が設計者の意図したものとなっているかを調べる設計検証の問題は、設計工程の過半を占めておりボトルネックとなっています。すべての入力パターンを直接的に網羅的にテストすることは、パターン数の指数的増大のため非現実的であるため、設計検証の目安としてカバレッジと呼ばれる基準が用いられています。カバレッジの改善を目指すのがカバレッジ駆動検証です。カバレッジにはいろいろな種類がありますが、ここではとくに、論理回路内の信号線のうちどのくらいの割合で0から1または1から0へ変化するかどうかに注目するトグルカバレッジを扱っています。 自動化のためランダムシミュレーションを実施してカバレッジの改善を図りつつ、飽和状態に達したところで、並行してSATソルバを用いてブルートフォースでカバレッジを改善するための入力パターンを発見して、検証をすすめるシステムを開発してきています。実験の結果、カバレッジの改善に効果があることを確認しています。 設計検証 設計自動化 フォーマル検証 カバレッジ駆動検証