超高速非同期式システムのための設計および検証ツールに関する研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12680334
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 米田 友洋 東京工業大学, 大学院・情報理工学研究科, 助教授 (30182851)
• Keywords: 非同期式回路 / 3値論理回路 / 3線式符号 / 形式的検証 / 有限幅遅延モデル / タイムペトリネット / Partial order reduction

Research Abstract

現在,大部分の非同期式回路のデータパスは2線式符号を用いて設計されている.この場合データパス内に制御用記憶素子(C素子と呼ばれる)が多数必要となる.これは,状態空間の拡大,処理速度の低下等の問題を引き起こしている.そこで,本研究では2線式符号の替りに3線式符号を用い,C素子を用いずにデータパス構成する設計手法を確立することを目的の一つとしている.本年度は,3線式符号を3値論理値を用いて2線で実現することを考え,まず3値2線式符号を一つ決め,それに基づいて,与えられた真理値表から基本ゲートを得るための手法をいくつか考案した.その中で,有効と思われる2つの方法について,アルゴリズムや得られた回路の複雑度について比較検討した.次年度は,SPICEシミュレーションやレイアウトCADを用いた評価を通して,3値2線式符号および基本ゲート生成アルゴリズム・簡単化アルゴリズムの決定を行う予定である.
一方,本研究のもう一つの目的は,データパスは(ランダムデータに基づき)確率的に,制御部は網羅的に検証を行うことで,人手による簡単化・抽象化を不要とする手法を確立することにある.本年度は,データパスを確率的に扱えるように,データパス回路にランダムデータを与え,データパス回路から受け取った値が(その与えた値に対して)正しい値であるかを判定できるように,タイムペトリネットモデルの拡張を行った.すなわち,データトランジション,条件トランジションといったデータを出力・比較するトランジションを設け,その発火規則を形式的に定義した.また,状態解析を効率よく行うため,partial order reductionと呼ばれる手法を,拡張したタイムペトリネットに適用することを検討した.その結果,アルゴリズムの大枠を得ることができたため,来年度はこれを実装し,効率を評価する予定である.