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