氏名　パラシオス　アルベルト
学位の種類　工学博士
学位記番号　博甲第33号
学位授与の日付　平成3年3月25日
学位論文の題目　Functional Verification of RTL Hardware Designs（レジスタ転送レベルのハードウェア設計における機能検証）
論文審査委員
　主査　教授　内藤　祥雄
　副査　教授　神山　忠一
　副査　教授　松田　甚一
　副査　助教授　高橋　勲
　副査　東京工業大学　教授　南谷　崇

• 論文目次
• 論文要旨

［平成2（1990）年度博士論文題名一覧］ ［博士論文題名一覧］に戻る．

目次
第1章　緒論　p.1
§1　序論　p.1
§2　本研究の背景　p.3
2-1　従来の研究の概要　p.4
2-2　従来の方法及び本検証方法の適用範囲　p.6
§3　本研究の意義と応用　p.7
第2章　基礎、ハードウェア記述、故障モデル　p.9
§1　機能記述法と基礎定義　p.9
1-1　機能記述　p.9
§2　ハードウェア記述言語（HDL）　p.15
2-1　仕様記述言語、バッファ（Buffer）　p.16
2-1-1　Buffer文法の特徴　p.16
2-1-2　Bufferの構文規則及び意味論の概説　p.17
2-2　レジスタ転送レベル（RTL）のHDL、AHPL　p.20
2-2-1　AHPLの基本的な文　p.21
§3　故障モデル　p.23
3-1　仕様における誤り　p.23
3-2　故障モデル　p.24
第3章　設計検証　p.27
§1　仕様と設計のモデル化　p.27
1-1　枠グラフの簡約化　p.28
1-2　枠グラフのラベル付け、原始レベルの動作確認　p.33
§2　処理順序及び制御順序の検証　p.37
2-1　可観測及び可制御動作の制御順序を表す正規表現　p.38
2-2　処理及び制御に関する設計の正常性　p.42
2-2-1　正規表現の等価性　p.42
2-2-2　正規表現の包含関係　p.46
§3　設計検証、故障検出　p.49
3-1　故障検出、故障の位置決定　p.52
3-2　設計検証　p.53
第4章　検証用の正規表現の生成方法　p.55
§1　基本的な概念と用語　p.55
1-1　パス表現　p.56
1-2　パス集合　p.58
§2　検証用の正規表現の求め方　p.59
2-1　パス集合の生成　p.61
§3　グラフの分解　p.63
3-1　強連結成分の分解　p.63
第5章　検証システムの実現、計算量
§1　仕様書と設計書の処理　p.68
1-1　可観測及び可制御動作の確認　p.68
1-1-1　仕様の可制御文及び可観測分の確認　p.68
1-1-2　設計の可制御文及び可観測分の確認　p.71
§2　グラフ上のパスの計算　p.73
§3　検証用のグラフのデータ構造、計算量　p.75
3-1　グラフのデータ構造　p.75
3-2　データ構造に関する計算量　p.81
§4　検証用の各手順の計算量　p.81
4-1　枠グラフを作成するための計算量　p.81
4-2　枠グラフの簡約化　p.81
4-3　ラベル付け及びラベルの統一　p.83
4-4　N-セット及びE-セットの計算量　p.83
4-5　正規表現の等価性の計算量　p.84
§5　評価　p.84
第6章　結論　p.85
参考文献　p.88
付録　p.93
A　バッファの構文規則　p.93
B　形式言語、関連定義　p.95
C　正規表現の基礎　p.99
D　プログラムリスト　p.105
謝辞　p.131

　近年の半導体集積化技術の進歩に伴いディジタルシステムの設計の効率化が益々強く望まれるようになってきている。その中でも、設計の誤りをいかにして少なくするかということが重大な問題となっている。この問題を解決するために、設計過程における検査及び検証に関する研究が盛んに行われており、これが新しい設計技術や新たなハードウェア記述言語（HDL）等の開発の一因になっている。本研究は、システムの設計を行う際に混入する誤設計を検出する方法に関するものである。ここで提案する検証方法は、特定のハードウェア記述言語や専用の設計システム等の特性に依存せず、現在広く用いられているレジスタ転送レベル（RTL）の任意のHDLで書かれた設計に対して適用可能である。但し、設計すべきシステムの機能は仕様記述言語で表現され、設計はRTL言語を用いて記述されていることを前提としている。
　現在、設計の最初の段階におけるシステムの仕様はハードウェア記述言語あるいはそのサブセットの仕様記述言語で記述されることが多い。しかしながら、これらの言語に共通な特徴は、設計の正しさを確認するためにほとんどの言語でその言語独自の方法を用いなければならないことである。これらの設計検証のレベルはまちまちであり、さらに現在用いられているほとんどのHDLの他のHDLとの互換性や変換性は非常に悪いため、任意のRTLで記述された設計の正当性を検証する一般的な方法はまだ確立されていない。そこで本研究においては、本文で提案される方法の一般性を高めるために、まず第一に検証の基準となる仕様を高レベルの仕様記述言語で与えることにした。従来の仕様記述言語は、特定の設計記述言語と密接な関係をもっていたり、特定の検証方法の適用を目的として開発されたものがほとんどであるため、本研究においては設計記述用の言語と独立でしかも十分な表現能力をもつ簡単な仕様記述言語を提案する。この言語の主な特徴は簡単な構文規則をもち、使い易いことにある。
　本論文で述べる検証方法は、システムの記述を制御信号の流れとデータ処理の流れの2つに分けることに基づいている。しかも、システムの故障モデルを高レベルにするために、検証すべき制御順序およびデータ処理順序の記述文をシステムの入力および出力に直接関連するものに限定している。すなわち、可観測あるいは可制御の信号を処理する文に着目し、仕様および設計の記述からシステムのモデル化を行う。これらの文をそれぞれ可観測文あるいは可制御文と呼ぶ。まず、記述中のデータ処理を表す文をノードで表し、制御を表す文を弧とした有向グラフを作る。これを枠グラフと呼んでいる。仕様および設計に対応し、二つの枠グラフが得られる。この枠グラフの弧およびノードにラベルを付することによって数学的な扱いができるようにする。これらのグラフ中の非可制御文および非可観測文に対応するノードを縮退させ、可制御および可観測文、または簡約化不能な文に対測文あるいは可制御文と呼ぶ。まず、記述中のデータ処理を表す文をノードで表し、制御を表す文を弧とした有向グラフを作る。これを枠グラフと呼んでいる。仕様および設計に対応し、二つの枠グラフが得られる。この枠グラフの弧およびノードにラベルを付することによって数学的な扱いができるようにする。これらのグラフ中の非可制御文および非可観測文に対応するノードを縮退させ、可制御および可観測文、または簡約化不能な文に対応する弧またはノードしか含まない簡約化されたグラフを得ることができる。ついで、ラベル付けされ簡約化された、仕様および設計から得られるそれぞれのグラフのノードおよび弧を用いて、グラフのすべての可観測文を表すノード間のすべてのパスをもとめて、正規表現の順序対を作る。この対の1つの要素は、ノードのラベルのみに着目したすべてのパスであり、もう一つは、このラベルのみからなるすべてのパスである。これらのパスは着目しているノード間で生じ得るすべての可観測文あるいは可制御文の実行系列を表している。本研究においては、このようにして得られる仕様上のすべての可観測文と可制御文の実行系列が設計から得られるグラフに含まれているか否かを確認することによって設計が仕様を満たしていることを検証する。モデルの中核となっている可観測文（動作）および可制御文（動作）に基づくグラフを用いることによって仕様と設計との記述に共通で最も重要な動作の特徴のみを取り出して設計を検証することができる。また、このグラフモデルを用いることによって、各々の動作の正しさだけでなくシステム全体の動作、すなわち制御と処理の関わり合う実行順序の正しさについても調べることができる。
　本論文で述べた方法は機能レベル（動作記述のレベル）での設計の（部分）正当性を検証するものである。このため、大規模なシステムの設計検証にも適用可能である。また、本検証法中で用いられるアルゴリズムは実現容易な理論および手法に基づいているため、本文中で述べられている成果は充分実用的であると考えられる。