第9回は“アサーションで行うフォーマル検証”について紹介します。
フォーマル検証は、設計の正しさを数学的に確認する手法です。
従来は専門的で扱いが難しい技術とされていましたが、近年はツールの進化により、実務でも活用される機会が増えています。
本記事では、アサーションを用いたフォーマル検証の基本的な考え方を整理します。

◆アサーションで行うフォーマル検証とは

フォーマル検証では、ダイナミック検証のようなシナリオやテストベンチを用いた検証とは異なり、状態空間を網羅的に解析します。そのため、波形駆動の検証環境に依存しない点が特徴です。
アサーションで定義した動作が、DUT（検証対象ブロック）に存在するすべての組み合わせにおいて成立するか否かを検証するため、フォーマル検証でPASSとなったアサーションは、同じ前提条件のもとではダイナミック検証でも満たされることが期待されます。
フォーマル検証は原理的にすべての条件を対象とするため、設計上意図していない入力条件でもFAILが検出されることがあります。
そのような場合は、assume文で入力条件に制約を与えることで、不要な条件を解析対象から除外できます。

＜assumeの記述例＞
assume property (@(posedge clk) (indata >= 10) && (indata <= 100));
この場合、入力信号indata（DUTへの入力値）は10～100の範囲に限定して検証が行われます。

assert や cover の記述自体はダイナミック検証と共通ですが、フォーマル検証ではそれらを網羅的に評価できる点が特徴です。