| 研究概要 |
ハードウェア記述言語Verilog-HDLを入力として等価なTLM記述を生成するトランスレータの開発を行った.具体的には,まずVerilog-HDL記述を構文解析した結果の構文木のデータ構造を生成し,そこから個々のVerilogモジュールをインスタンス化した意味モデルの生成を行う.さらにこの意味モデルからシミュレーション用のモデルの生成を行う.
本来のVerilog-HDLの意味モデルではかなり自由なスタイルでハードウェアの記述を行えるが,実際に論理合成を行って回路を生成できる記述スタイルはかなり制限されている.具体的には,あらかじめ「クロック信号」と規定された信号線に同期して各記憶素子の値が切り替わる,というモデルである.そこで,論理合成対象の回路記述に対してはこのような単純化された意味モデルを用いてシミュレーションを行うことで基本となるシミュレーション速度の向上を図っている.
これらの技術そのものは学術的にはそれほど先進的なものではないが,シミュレーションモデルの抽象化という本研究の本題の技術を開発するための基礎となるものであり,今後の研究を進める上で不可欠のものとなっている
また,抽象化を行う際に用いる充足可能性判定問題(SAT)ソルバの開発を行った.既存のプログラムでトップクラスのMiniSatとほぼ同等の性能を達成している.これに述語論理の判定アルゴリズムを付加することで一階述語論理の検証が行なえるSMTソルバを開発することができる.このSMTソルバを用いて数学的に正しいと保証される変換を行うことで抽象化を行う.
|
