有限遅延幅モデルにおける非同期式回路の検証について (テストと設計検証論文特集)

概要

論文の詳細を見る
従来, 非同期式回路の設計検証においては, 主に素子の遅延時間は0から無限大として取り扱われてきた. しかし, どのように遅延時間が大きくても正しく動作するように設計しようとすると, 回路が複雑になり結果として動作速度が低下する。そこで, 最近では素子の最大遅延はある有限値であると仮定し, その仮定のもとで回路を設計することが行われている. しかし, このようにして設計された回路は, 従来のいわゆるuntimedモデルに基づく検証方式では設計の正しさを確認できない. そこで, このような回路をより正確にモデル化するために, 実時間制約を表現できるモデルとそれに基づく検証方式が必要となる. 本論文では, 従来のトレース理論のモデルを拡張した, タイムペトリネットによるモデルを考え, そのもとでsafety failureとliveness failureに基づく正しさを定義する. また, その正しさを実際に判定する方法を示し, それを実現するアルゴリズムとその正しさの証明を与える.
社団法人電子情報通信学会の論文
1999-07-25