2018 Fiscal Year Research-status Report
| Project/Area Number |
17K00089
|
|---|
| Research Institution | Ishikawa National College of Technology |
|---|
Principal Investigator |
松本 剛史 石川工業高等専門学校, 電子情報工学科, 准教授 (40536140)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 機能検証 / プロパティ検証 |
|---|
| Outline of Annual Research Achievements |
論理回路を正しく設計するために、機能の検証は不可欠である。回路設計検証においては、テストパタンを用いたシミュレーションに加えて、回路が満たすべき性質（プロパティ）を数学的に検証するプロパティ検証も行われている。プロパティ検証は、任意の入力パタン（シーケンス）について正しさを検証することができるため、シミュレーション検証で問題となるテストパタン不足による検証漏れの恐れのない手法である。一方で、プロパティ検証では、回路の性質を網羅的に列挙することができない場合に検証できていない部分が生じてしまう。本研究では、プロパティ検証において、プロパティの質の高さを表す指標を確立することを目的としている。
平成30年度は、所属する高等専門学校で回路作成の学生実験に用いられている簡易CPU回路に対する検証を対象にして、学生が実験で実際に起こした回路誤りを検出するために必要となるプロパティ集合がどのようなものであるかを考察し、対象回路の検証に有効であると考えられるプロパティ集合を作成した。その後、一つ一つのプロパティによって検出することのできる回路部分を基にして、プロパティの網羅性を計算した。次年度は、この考え方をより大規模な回路で適用し、より一般的なプロパティの網羅性の定義について考案と評価を行う予定である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
プロパティの網羅性について、小さな設計例題での評価をしており、次年度は、プロパティ網羅性の改良や応用について研究を行える状況である。
|
| Strategy for Future Research Activity |
研究期間3年間の3年目となる次年度は、今年度の学生実験用CPU回路での評価を通して得られた成果を基にして、より大規模な回路でプロパティ網羅性の評価を行い、その改良や応用について研究を行う。
|
| Causes of Carryover |
研究補助として学生への謝金支払いを予定していたが、研究補助に適する学生がいなかったため、これを行わなかった。一方、プロパティ網羅性を高速に計算するためにFPGAボードを用いることを予定しており、次年度にその購入を予定している。
|
