Development of Coverage Metric for Formal Property Verification

2020 Fiscal Year Annual Research Report

• Project/Area Number: 17K00089
• Research Institution: Ishikawa National College of Technology
• Principal Investigator: 松本 剛史 石川工業高等専門学校, 電子情報工学科, 准教授 (40536140)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Keywords: 機能検証 / プロパティ検証

Outline of Annual Research Achievements

本研究では、論理回路のプロパティ検証におけるプロパティの網羅性を表す指標を開発することを目的としている。プロパティ検証とは、回路が満たすべき性質（プロパティ）を入力パタンに関わらずに満たしているかどうかを調べる検証手法であり、シミュレーションやエミュレーションといった回路に入力パタンを与えて行う動的検証手法を補完するために用いられている。動的検証では、検証の進み具合を知るための指標として、設計記述中のどの部分が入力パタンの集合によって網羅されたかを表すカバレッジが用いられているが、プロパティ検証ではそのような指標が確立されておらず、どの程度の数のプロパティを用いれば、十分に回路を検証できたと言えるかについて知ることができない。本研究では、論理回路のプロパティ検証において網羅性の指標を開発し、この問題を解決することを目指している。
令和2年度の研究では、前年度の研究で提案した網羅性指標の計算をFPGA回路実行することによって高速化する検討を行った。提案する網羅性指標は、検証対象の状態遷移システムに対してあるプロパティを検証した結果と、検証対象システムからある状態遷移を削除して得られるシステムで同じプロパティを検証した結果が異なるのであれば、削除された状態遷移はプロパティの検証でチェックされていると考えるものである。有限クロックサイクルのプロパティ検証は回路として実装することができるため、外部信号によって状態遷移の削除を制御する機能を追加することにより、回路上で網羅性指標の計算も可能である。そこで、この考えに基づいて網羅性指標を計算する回路をFPGA上に実装し、実際に計算ができることを確認した。