Verilog-HDL による大規模ハードウェア設計の検証支援ツールの開発

摘要

本稿では，Verilog-HDL で記述された大規模ハードウェア設計の検証支援ツールについて報告する．検証には, フォーマル検証技術のー種である記号モデル検査に基づく検証器であろNuSMV を用いる．本ツールでは，Verilog-HDL による設計記述を，NuSMV の入力となるSMV プログラムへと自動的に変換する．また，Verilog コードの構文解析中まpyverilog を用いており，pyverilog が生成した抽象構文木を入力として，SMV プログラムの生成を行う．