| 研究概要 |
現在,大部分の非同期式回路のデータパスは2線式符号を用いて設計されている.この場合データパス内に制御用記憶素子(C素子と呼ばれる)が多数必要となる.これは,状態空間の拡大,処理速度の低下等の問題を引き起こしている.そこで,本研究では2線式符号の替りに3線式符号を用い,C素子を用いずにデータパス構成する設計手法を確立した.まず3値2線式符号を一つ決め,それに基づいて,与えられた真理値表から基本ゲートを得るための手法をいくつか考案した.その中で,有効と思われる2つの方法について,アルゴリズムや得られた回路の複雑度について比較検討した.さらに,基本ゲート生成アルゴリズム・簡単化アルゴリズムについて検討した.
上記のような設計手法を用いることにより状態空間・C素子数が削減でき,設計検証の計算量は大幅に削減されることが期待できるが,特にデータパスを含む回路の計算量は依然として大きいと予想される.そこで,本研究ではより実現性の高い,「データパスは(ランダムデータに基づき)確率的に,制御部は網羅的に」検証を行うことで,人手による簡単化・抽象化を不要とする手法を開発した.まず,データパスを確率的に扱うために,データパス回路にランダムデータを与え,データパス回路から受け取った値が(その与えた値に対して)正しい値であるかを判定できるように,タイムペトリネットモデルの拡張を行った.すなわち,データトランジション,条件トランジションといったデータを出力・比較するトランジションを設け,その発火規則を形式的に定義した.さらに,拡張したタイムペトリネットを効率的に解析するために,検証に必要ない部分の状態解析を効率的に除去する,partial order reductionと呼ばれる手法を適用し,いくつかのベンチマーク回路を検証して効率を評価した.その結果,partial order reduction手法の効果は非常に大きいことを確認するとともに,レベル指向モデルを用いることにより,モデルが大幅に簡単になることがあり,そのような場合には,従来の遷移指向モデルで記述した場合よりも検証自体の高速化が図れることがわかった.
|
