HDLコードに対するSMTソルバを用いた自動検証システムの提案

情報処理学会

書誌事項

タイトル別名
  • A Testing System Using an SMT Solver for HDL Code

説明

HDL（Hardware Description Language）コードをシミュレーションで検証する時，実行されていないステートメントは未検証となってしまうため，コードのカバレッジ（網羅率）が検証の品質を計測する重要な指標の一つとなる．一般的なランダム検証ではモジュール（HDLコード）への入力をランダムに決めるため，十分なカバレッジが得られないことがある．そこで我々はブランチカバレッジを100\%にするための自動検証システムを提案する．提案システムの特徴はレジスタ値を直接設定する仕組みを検証対象のモジュールに入れ，モジュールの検証されていないステートに強制的に遷移させる点にある．これにより遷移先のステートメントを実行することでカバレッジを向上させる．モジュールへの入力とレジスタに設定する値はモジュールに含まれるif文などの条件をもとにSMT（Satisfiability Modulo Theories）ソルバを用いて求める．実験では一般に公開されているIPコア3つを用意し，提案システムによりブランチカバレッジがいずれも100\%になることを確認した．加えて，ランダム検証の結果も比較対象として載せる．

When a module in HLD code is tested using a simulation, HDL-code coverage is one of the most important metrics for testing because part of the code is not checked if it is not executed. This makes it necessary to obtain as high coverage as possible. In this paper, we propose a testing system for modules written in HDL code, aiming at a branch coverage of 100\% during a simulation. For this aim, our system previously inserts input pins to a target module for directly setting its register values. Our system then automatically changes the current state of a module to another state during a simulation by setting the corresponding registers via the inserted pins. At this time, our system uses an SMT solver to obtain such register values for the state transition by satisfying branch-conditions contained in a module.

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ