|
本研究課題では、２つの設計記述に対して、タイミングを考慮した等価性検証を行うことを目的としている。前年度までに、入出力タイミングを考慮した高位設計の等価性検証の前提となる、等価性を判定するタイミングの数学的定義をを行い、その定義に基づいて、与えられた２つの設計記述の入出力変数・内部変数において成り立つ等価性を効率的に推定する手法とそのGPU上での実装に関する研究開発を行った。最終年度である今年度は、等価性検証自体の高精度化・高効率化を目指し、設計記述の一部分の論理が変更された場合に、それを検出することのできるテストパタンの生成手法に関する研究を行った。これは、その設計において使用可能な演算器(演算回路)を任意に適用可能な部分回路によって設計記述の一部を置換し、設計記述全体が仕様と等価になるように部分回路の論理を一意に定義するために必要となるテストパタンを求めるものである。このテストパタンを用いることによって、全ての可能な入力パタンに対して設計が仕様と等価であるかどうかを少数のテストパタンに対するテストによって検証することができる。実験によって、置換する設計部分の演算数が数個程度の設計であれば、非常に少数のテストパタンで等価性を検証できることが示された。
本研究では、研究期間全体を通して、レイテンシ・スループットと付加条件に基づく等価性の定義、効率的な等価変数(内部変数含む)の推定手法、テストパタンに基づく完全な等価性検証の基本手法を得ることができた。
|
