SystemVerilog アサーション (SVA) 入門

---

## 1. はじめに

筆者は普段はソフトウェア開発やモデルベース開発＆検証の業務を中心にしていますが、**仕事で時々半導体（ASIC など）の検証にも携わる** ことがあります。  
モデルベース開発や高位合成の一環で **SystemC** を利用し、**システムレベルやトランザクションレベル**の検証を行う場面も多いです。  
しかし、**SystemC は高レベルのアーキテクチャ検証やアルゴリズム検証に向いている一方で、RTL レベルの詳細なタイミング検証やカバレッジ測定は得意とは言えません。**  
そうした**低レイヤーの挙動**や**大規模設計の網羅的な検証**を行うには、やはり **SystemVerilog と SVA (SystemVerilog Assertions)** が欠かせないというのが実情です。

特に、**ハードウェア検証**を考慮すると、SystemC だけでは完結しきれず、**SystemVerilog と混在した環境**での検証フローが必要になります。  
その際に非常に役立つのが、SystemVerilog で提供される **SVA (SystemVerilog Assertions)** です。  
SVA を使いこなせば、時相的な動作チェックや機能的カバレッジを一元的に管理できるため、**半導体の検証に携わるエンジニアにとっては必須の知識** と言えるでしょう。

そこで本記事では、そんな **SVA** について、  
- どんなときに役立つのか  
- 基本的な書き方  
- 実際に使う際のポイント  

を**初学者向け**にまとめました。  

「SystemC/SystemVerilog はなんとなく検証で使っているけど、もっと厳密な検証が必要…」  
「波形でチェックしてたけど、何か自動化できる方法はないの？」  
という方にも読んでいただける内容を目指しています。

---

## 2. なぜアサーションが必要か

### 2.1 テストベンチだけでは不十分

RTL のシミュレーションでテストベンチから刺激を与え、出力波形をチェックする――これは従来からある手法です。  
しかし、設計が大規模化・複雑化するほど**すべての動作タイミングや内部信号を波形で完全にカバーするのは難しい**のが現状です。  
波形レビューだけに頼ると、**微妙な一瞬のバグ**や**複雑な時系列制約**を見落とす可能性が高まります。

### 2.2 仕様を“コード”で明示するアサーション

そこで登場するのが **SVA（SystemVerilog Assertions）** です。  
- 「リセットがアクティブの間は開始信号を上げてはいけない」  
- 「valid が立っているときは次のクロックで ready も立つ」  

といった**時相的・論理的な仕様**を、SystemVerilog の構文で直接表現しておきます。  
実行時に違反があれば即座に警告やエラーを出してくれるので、**波形の人力チェックだけに頼らない自動検証**が可能となり、大幅な効率化・品質向上を見込めます。

---

## 3. SVA の基本要素と構文

SVA には大きく 3 つの要素があります。

1. **`assert property`**  
   - 設計が必ず満たすべき「ルール」を記述し、違反時にエラーとして報告

2. **`assume property`**  
   - 入力・環境が守るべき制約を記述し、フォーマル検証などで利用

3. **`cover property`**  
   - 指定した時相・条件が実際に起きたかどうかを観測し、カバレッジとして記録する

### 3.1 `property` と `sequence`

SVA で**時系列（時相的）パターン**を表すには `sequence` を使い、それを組み合わせて `property` として定義します。

```systemverilog
sequence req_ack_seq;
  req ##[1:3] ack; // req が立ってから1～3サイクル以内に ack が立つ
endsequence

property req_ack_property;
  @(posedge clk) disable iff (rst) req_ack_seq;
endproperty

assert property (req_ack_property);
```

- `sequence` で「req → (1～3 サイクル後) → ack」の時間的関係を定義  
- `property` で「リセット中は無効 (disable)、クロック立ち上がりごとにこの sequence をチェック」というルールを記述  
- `assert property` で「守られなければエラー」を検証

---

## 4. `assert property`：仕様通り動いているかをチェック

### 4.1 基本構文

```systemverilog
assert property (@(posedge clk) disable iff (!reset) <sequence or condition>);
```

- `@(posedge clk)`: クロックの立ち上がりで評価  
- `disable iff (!reset)`: リセットが 0（アクティブ）なら property チェックを無効化  
- `<sequence or condition>`: 時相的パターンやブール式

### 4.2 実例：リセットとスタートの競合

```systemverilog
property no_reset_and_start;
  @(posedge clk) disable iff (!rst_n)
    !(start && rst_n == 0); // リセット中に start をアサートしてはいけない
endproperty

assert property (no_reset_and_start)
  else $error("Reset and start are asserted simultaneously!");
```

- リセット(アクティブ Low)期間中に `start` を立てないようにするルール  
- 違反したら `$error` でログ表示・シミュレーション停止などを行う  
- 波形で見落としがちなタイミング制約もアサーションなら自動検出可能

---

## 5. `assume property`：入力・環境の制約

フォーマル検証で特に役立つのが **`assume property`** です。  
- 「入力 X は絶対に 0～255 の範囲しか取らない」  
- 「リセット時にはクロックが止まらない」  
など、**設計外部の前提**をツールに示します。

```systemverilog
property valid_range;
  @(posedge clk) disable iff (!rst_n)
    (in_data < 256);
endproperty

assume property (valid_range);
```

これによりツールは「`in_data` が 256 以上になるシナリオ」を探索対象から除外し、**より的確に検証**できます。  
シミュレーションでも「テストベンチがこの制約を破ったらテストベンチ自体がバグ」という形でチェックを行えます。

---

## 6. `cover property`：発生確認 (機能カバレッジ)

`cover property` は、指定した**時相的イベント**が実際に発生したかどうかを観測します。  
特に**設計の内部挙動**や**プロトコルシーケンス**をウォッチしたいときに便利です。

```systemverilog
sequence start_to_done;
  start ##[1:10] done;
endsequence

cover property (@(posedge clk) disable iff (!rst_n) start_to_done)
  else $display("start->done sequence occurred!");
```

- “`start` が立ってから 1～10 サイクル以内に `done` が立った”パターンが起きればカバレッジで記録  
- シミュレーション終了後、レポートを見れば「指定シーケンスを踏んだかどうか」が一目瞭然

---

## 7. 仕様をアサーション（SVA）へ落とし込むには

### 7.1 自然言語の“仕様”を分析し、ルールやシーケンスに分解する

多くの場合、仕様書は**自然言語（日本語や英語）** や簡単なフローチャートで書かれています。  
ここからアサーションを作るには、**仕様を「条件」「タイミング」「許可/禁止ルール」** に分解し、SVA の `property` として定義できる形にする作業が必要です。

1. **キーとなる信号や状態を洗い出す**  
   - たとえば「`start` 信号が立ったら、`busy` 状態になる」「`done` 信号は必ず `busy` のみで立ち下がる」など。  
   - 仕様書やフローチャートの要点を抽出すると整理しやすい。

2. **時相的要件を洗い出す**  
   - 「N サイクル以内に応答する」「後続ステージが進む前にフラグが下がる」など、時間軸に依存する部分を `sequence` で表せるか考える。  
   - `##[1:3]` といった繰り返し数や範囲指定が必要かどうかを決める。

3. **必要に応じて複数の property に分割**  
   - 1 つの文章で複数の条件が書かれている場合は、**アサーションを細かい単位**に切り分けるとデバッグしやすい。  
   - 例: 「`start` が立ったら `busy` になる」(property A) と 「`busy` 状態では `done` が 1 サイクルだけ立つ」(property B) など。

### 7.2 担当者間レビューで仕様とアサーションの対応関係を確認

仕様をアサーション化するときは、**レビューを通じて誤解や抜け漏れを防ぐ**ことが大切です。

- **設計者・仕様策定者**と検証担当が、**アサーション文書**（or ソースコード）を見ながら、  
  「この文章はここの `assert property(...)` でカバー」「この FSM の状態遷移図はこう書き起こした」など、1:1 で対応を確認。  
- 「ここは SVA にしにくいが、テストベンチの Directed テストでカバーしている」というように、**他の手法との分担**も把握する。

> **ポイント**: 「仕様に書いてあるルールが本当にすべてアサーションで表現されているか？」「逆に、アサーションが勝手に拡大解釈していないか？」をチェックします。

---

## 8. アサーションと仕様が一致しているかのチェック方法

### 8.1 最終的には“人的レビュー”が要

残念ながら、**自動で「アサーションと自然言語仕様が一致しているか」を検証するツールは一般的ではありません**。  
基本的には次のようなアプローチになります。

1. **同じ仕様書を参照しながらコードレビュー**  
   - 「仕様書 3.2 節の条件 A は、ここの `assert property(...)` でカバーできているか」を設計者 or チームで確認。  
   - 口頭やチャットで「この書き方だと仕様の解釈が違う」「こういう例外ケースは？」など議論を行う。

2. **相互レビュー (2 人以上の目)**  
   - 検証担当者だけでなく、設計者や仕様策定者もアサーションのコードを確認する。  
   - 第三者視点で「もしこのタイミングでリセットが来たらどうなる？」といった検討を行うことで、見落としを防ぐ。

### 8.2 リファレンス表やトレーサビリティマトリクスを作る

**「仕様の章・条項と、対応するアサーション ID を表にまとめる」** という手法もよく使われます。

| 仕様書項目    | SVAファイル / property名 | 概要      | 担当/レビュー日        |
|:----------------:|:----------------:|:------------------:|:----------------:|
| 3.2.1 リセット時は start禁止 | `reset_no_start`  |リセット中に start=1 にならない | 設計者A/検証者B, 2025/01/10 |
| 3.2.2 start→busy 遷移  | `start_to_busy`  | startでbusyフラグが立つ  | 設計者A/検証者C, 2025/01/10 |

こうした **トレーサビリティマトリクス** を作ると、  
「仕様のどの項目がどのアサーションで検証されているか」  
「この条項はアサーションが見当たらない…」  
といった抜け漏れを発見しやすくなります。

### 8.3 フォーマル検証＋アサーションのカバレッジ

一部のフォーマル検証ツールでは、**アサーションが常に成立（もしくは不成立）のままで実質検証できていない** 場合などに警告を出す機能があります。  
- これにより「アサーションに書いたけど、実は常に真 (true) になっていて無意味」「常に偽 (false) で到達不能」などの誤用を検出可能。  
- ただし、それでも **“アサーションが仕様と同じか”** までは保証できません。  
- あくまでレビューとの併用が必要です。

---

## 9. アサーションをどこに書く？

### 9.1 テストベンチ側

- UVM など**検証環境**にまとめるケースが多い  
- RTL を汚さず、検証者が自由にアサーションを追加しやすい  
- 検証対象 (DUT) が複数のレイヤーにまたがる場合、アサーションも TB 側で階層的に配置すると管理しやすい

### 9.2 RTL 内部

- クリティカルな仕様や、設計とセットで管理したい場合に有効  
- 「このレジスタはこういうルールで書き換わるはず」というのを RTL と一緒に記述することで可読性が増す  
- ただし、プロジェクト方針によってはテストベンチ以外への記述を嫌う場合もあるので要確認

---

## 10. 実行とレポートの流れ

1. **シミュレーション**  
   - Xcelium / VCS / Questa など主要シミュレータは SVA 対応  
   - アサーション違反時にログで `assertion failure` と報告→即デバッグ  
   - シミュレーション結果を波形で見る際も、アサーション違反箇所にジャンプすれば素早く問題点を把握できる

2. **カバレッジレポート**  
   - `cover property` で観測したシーケンスが起きたかを確認  
   - 構造的カバレッジ（ステートメント / ブランチ / トグルなど）と合わせて“どこが未達成か”を把えられる  
   - 機能カバレッジ（covergroup）と合わせれば、設計の重要なシナリオが網羅されているかもわかる

3. **フォーマル検証**（オプション）  
   - `assume` で入力制約を与え、`assert` が常に成立するか証明  
   - ツールが全パスを網羅的にチェックし、違反があればカウンター例を提示  
   - 時間・リソースは必要だが、深刻なバグやレアケースの早期発見に有効

---

## 11. よくある質問（FAQ）

#### **Q1. アサーションを書いたらシミュレーションが重くなりませんか？**

A. 多少は負荷が上がりますが、最近のシミュレータは最適化が進んでいて、アサーション数百～数千行程度なら大抵問題なく動きます。  
むしろ、**波形で延々とデバッグする時間を削減** できるメリットが大きいでしょう。  
大規模設計でも、アサーションを適切に分割・階層化すればパフォーマンス上の問題は比較的抑えられます。

---

#### **Q2. すでにテストベンチでチェックしてるのに、アサーションが必要ですか？**

A. テストベンチ(例えば UVM)でカバーしきれない、**時相的・内部的な動作**をアサーションが自動監視してくれます。  
波形レビューでは見落としがちな **一瞬の破綻** や **特殊な状態遷移** も、アサーションなら即エラー報告してくれるため、品質向上に寄与します。  
また、テストベンチは主に **外部インターフェイスからの刺激** に注目しますが、アサーションを設計内部へ仕込むことで「本当に意図したシーケンスか」をより詳細にチェック可能です。

---

#### **Q3. RTL に書く vs テストベンチ側に書く、どちらが正解？**

A. 一般的には **「検証者が管理する」→ テストベンチ側**、**「設計仕様そのもの」→ RTL 内** という住み分けが多いです。  
ただし、プロジェクトによっては「RTL をクリーンな状態に保ちたい」方針の場合、アサーションはすべて外部ファイルや TB 側にまとめることもあります。  
**チームポリシー**や**設計者との連携**次第で柔軟に決めるのが良いでしょう。

---

#### **Q4. SVA と PSL (Property Specification Language) の違いは？**

A. **SVA** は SystemVerilog 言語標準の一部として定義されたアサーションで、Verilog/SystemVerilog 設計との親和性が高いのが特徴です。  
一方の **PSL** は、VHDL や Verilog 等、複数の HDL で使えるプロパティ記述言語として策定されました。  
現在は多くのプロジェクトで SystemVerilog を使うことが増え、SVA が主流になりつつありますが、VHDL ベースの設計では PSL を使うこともあります。  
基本的な時相的記述の考え方は似ていますが、**ツールや合成フローとの連携**は SVA の方が進んでいるケースが多いです。

---

#### **Q5. SystemC のテスト環境だけで検証するのは難しいのでしょうか？**

A. SystemC は高位合成やシステムレベルモデリング向けに強みがありますが、**大規模な RTL レベルの検証**を完結させるには機能が不足しがちです。  
特に**カバレッジ解析や時相的アサーション**などは、SystemVerilog の方がツールサポート・実績ともに充実しています。  
そのため、**SystemC モデル→最終的な RTL** へ落とし込む段階では、SystemVerilog 環境（UVM、SVA など）を使うのが一般的な流れです。

---

#### **Q6. フォーマル検証だけで十分ですか？ シミュレーションは不要？**

A. フォーマル検証は**バグを網羅的に探せる**一方、設計規模が大きいと処理が爆発的に増え、解析に時間やリソースがかかりすぎる場合があります。  
また、外部 I/O や複雑なソフトウェア連携など、**テストベンチでシステムレベルの動作を確認する**のにはシミュレーションが適しています。  
**フォーマル と シミュレーション**を組み合わせることで、お互いの弱点を補い合うのが現実的なアプローチです。

---

#### **Q7. アサーションのカバレッジ（cover property）だけで機能カバレッジは十分でしょうか？**

A. `cover property` は**時相的シナリオ**を観測できる便利な機能ですが、  
システム全体の機能やパラメータパターン、レジスタ設定の組み合わせなどを**網羅的に測る**には、  
**covergroup (SystemVerilog)** や **UVM のシーケンスカバレッジ**など、より広範な機能カバレッジも検討が必要です。  
アサーションは **「今起きたイベントが正しかったか」** を細かく見張る役割、  
機能カバレッジは **「さまざまな入力パターンや状態遷移を試せているか」** を俯瞰する役割、  
それぞれ得意分野が異なるので併用すると効果的です。

---

#### **Q8. Assertions はゲートレベル (GLS) でも使えますか？**

A. 一般的には、**ゲートレベルシミュレーション (GLS)** では複雑な時相チェックやアサーションの大半が非効率になりがちです。  
   - 最適化やゲーティングで信号名が変わり、アサーションと合わない場合が多いため、通常は**RTL シミュレーションでアサーションを十分に活用**し、  
     必要であれば GLS では最低限のアサーション (リセット期間の波形チェック程度) だけを残すことが多いです。  
   - ただし、ツールやプロジェクト要件によってはゲートレベルで簡易アサーションを走らせることもありますが、時間やメモリ負荷が大きくなる点に注意が必要です。

---

## 12. まとめ

- **SystemVerilog Assertions (SVA)** は「設計の仕様やルールをコード化し、自動チェックする」ための強力な仕組み。  
- `assert property` / `assume property` / `cover property` の 3 つを理解するだけでも、**ずっと広い検証範囲**をカバーできるようになります。  
- 構造的カバレッジ（ステートメント、ブランチ、トグルなど）と組み合わせることで、**網羅度**と**動作の正しさ**の両面を補完できるのも魅力です。  
- また、**SystemC だけで大規模 SoC を検証しきるのは難しく、最終的には SVA を活用した SystemVerilog ベースの検証フローがほぼ必須**になる場面が多々あります。

**最も大切なのは、アサーションが“本当に仕様を表しているか”**をレビューやトレーサビリティマトリクスで管理すること。  
自然言語の仕様書と SVA を丁寧に照合し、抜け漏れや解釈ミスを防ぐのがポイントです。

まずは小さなサンプルで試してみて、波形ログを見ながらアサーション違反が出る様子を体感してみてください。  
**「自分が波形を目視せずとも、アサーションが細かいバグを教えてくれる！」** その便利さを一度知ると、もうアサーションなしの検証には戻れなくなるかもしれません。

---

## 13. LLM を使って仕様→アサーション化・整合性チェックを試みる

近年の **LLM (Large Language Model)**、例えば ChatGPT や GPT-4 などを活用すれば、  
自然言語の文章からある程度のコードを生成したり、文章同士の対応関係を分析してもらうことが期待できそうです。  
ただし、次のような**メリット・デメリット**を理解したうえで使う必要があります。

### 13.1 LLM 活用のメリット

1. **自然言語の仕様からアサーション用の下地コードを自動生成**  
   - 仕様書にある「start→busy への遷移」「N サイクル以内に ack を返す」といった記述を要約させ、SVA の skeleton（ひな形）を作らせる。  
   - 人手で一から書くよりも、初期段階の下地づくりが高速化する可能性がある。

2. **文章同士の対応チェック**  
   - 仕様書とアサーションが「どの部分で対応しているか」をある程度タグ付けさせ、  
     LLM に「仕様の段落 x.y は property foo で検証？」といった問い合わせをすると、  
     テキストマッチング的に関連性を示してくれることがある。

3. **コードレビュー支援**  
   - LLM は大まかな論理的矛盾や単純なスペルミス・構文ミスを指摘するのが得意。  
   - 「sequence の指定範囲がおかしくないか」など簡易チェックには役立つ。

### 13.2 注意点・デメリット

1. **専門的な仕様解釈はまだ苦手**  
   - LLM は自然言語パターンを元に提案するため、**ハードウェア特有のクロックドメインや非同期リセット**などの正確な扱いは不得意。  
   - あくまで補助ツールと割り切り、最終的なロジックは人間が検証する必要がある。

2. **“ハルシネーション”のリスク**  
   - LLM は根拠なく説得力のある回答を作り出す場合がある（ハルシネーション）。  
   - **実は仕様にない条件を勝手に追加**したり、逆に削除してしまう可能性がある。  
   - 必ず**人的レビュー**で確かめる必要がある。

3. **プライバシー・セキュリティの懸念**  
   - 社内秘の仕様書やソースコードを直接 LLM に入力すると情報漏洩のリスクがある。  
   - オンプレミスの LLM 環境や、セキュアなプライベートサービスを使うなど対策が必須。

### 13.3 LLM の活用例: 手順イメージ

1. **仕様書を分割 & テンプレート化**  
   - 「start→busy の動作は N サイクル以内」「リセット中は start=0 である」など箇条書きにし、LLM に供給。
2. **LLM に“時相的ルール”としてどう表現するかを質問**  
   - 「以下の要件を SystemVerilog Assertions (SVA) で書いてほしい」など。  
   - 返ってきた案を受け取り、目視で修正・整理。
3. **生成されたアサーションを設計者や検証リーダーがレビュー**  
   - 「N サイクル以内という定義はリセット解除直後も含むか？」など突っ込んだ確認を行う。  
4. **LLM に再度フィードバックして細かい修正を繰り返す**  
   - 大枠ができたら、`disable iff (!rst_n)` などの細部を詰める。
5. **最終的に人間が統合し、シミュレーションやフォーマルにかける**  
   - LLM だけでは対応しきれない微妙な仕様があるため、実際にコンパイルして問題点を確認。

### 13.4 まとめ: LLM は補助ツールに留まる

- LLM は、**自然言語からアサーションコードを書く“最初の一手”** や、仕様とアサーションの対応をざっくり整理する用途には有用。  
- しかし、**アサーションがハードウェア仕様と正確に一致しているか** の最終確認は、人間によるレビューが不可欠です。  
- ASIC/FPGA 設計のように「複数クロックドメイン」「特殊なリセットシーケンス」が絡む領域では、  
  **LLM の提案をそのまま鵜呑みにできない**ことに注意。  
- うまく組み合わせれば、ドキュメント作成やコード生成の手間を軽減し、検証者がより本質的な部分に注力する体制を作れるかもしれません。

---

## 14. 注意点: IMC などのカバレッジツールとカバープロパティのカバー率は別物

以下の図は、**構造的カバレッジ** と**機能的カバレッジ（カバープロパティ）** の位置づけをざっくり示しています。

```mermaid
flowchart LR
    A[構造的カバレッジ<br>IMC/VCSなど] --- B[RTL行/分岐<br>トグルの網羅度]
    A --> D[自動解析で計測]
    A --> E[テスト不足箇所<br>の洗い出し]

    F[機能的カバレッジ<br>cover property] --- G[意図したイベント<br>シナリオの発生確認]
    F --> H[ユーザー定義の<br>property/sequence]
    F --> I[イベントが一度でも<br>起きればCovered]

    B --> J[数値は<br>構造視点]
    G --> K[数値は<br>時相/機能視点]

```

一般的に、**Cadence IMC で見るカバー率（いわゆる構造的カバレッジ）** と、**SVA の `cover property` で得られるカバレッジ（いわゆる機能的／プロパティベースのカバレッジ）** は、それぞれ意味合いや計算方法が異なるため、同じ「カバー率」という言葉でも数値や観点が変わってきます。Synopsys 環境では、**Verdi** や **VCS** が同様の解析を行います。

すなわち、**IMC で得られるカバレッジ数値とカバープロパティで得られるカバレッジ数値は、元々まったく異なる視点を扱っています。**

---

### 1. IMC のカバー率（構造的カバレッジ）

Cadence **IMC (Incisive Metrics Center)** などのカバレッジ解析ツールでは、**構造的カバレッジ**を主に扱います。具体的には

- **ステートメント・行 (Statement) カバレッジ**  
- **ブランチ・条件式 (Branch / Expression) カバレッジ**  
- **トグル (Toggle) カバレッジ**  
- **FSM (状態遷移) カバレッジ**  

など、**RTL コードのどこまで実行・通過したか**を測定する指標をまとめてレポートします。  
こうした構造的カバレッジは、**「コードベースの網羅度」** を可視化するのが目的です。

**特徴**
- 「(Coveredポイント数) / (Totalポイント数)」という形で百分率を算出  
- RTL の構造をベースに自動で検出・計測するため、テストベンチから特別な指示がなくてもある程度計測可能  
- 「このブロックの行が何％通ったか」「この分岐が true/false を何回通ったか」を確認することで、**テスト不足の箇所**を洗い出す

---

### 2. カバープロパティ (cover property) のカバー率

一方、SystemVerilog Assertions (SVA) の **`cover property`** 構文を使うと、**特定の時相的・機能的イベントが実際に起きたかどうか**を検出できます。これは、

- **ある信号シーケンスが起きたか** (例: `start` → 数サイクル後 → `ack`)  
- **特定の条件が成立したか** （状態が A から B に遷移した上でフラグが立つ、など）

をカバレッジとして取りたい場合に使われるもので、**機能的カバレッジ**に近い考え方です。

**特徴**
- `property` / `sequence` で書かれた**時相的ルール**が実行中に一度でも成立すれば「Covered」とカウント  
- 「起きたか／起きないか」という形で最終的なカバレッジを % で報告することも可能  
- **アサーション (SVA) のレポート**と一緒に管理されるため、IMC 上では “Covergroup / Cover Properties” として別枠で表示されることが多い  
- **ユーザーが明示的に「観測したい事象」をコーディング**する必要があり、構造的カバレッジのように RTL を自動解析してくれるわけではない

---

### 3. なぜ「違うカバー率」になるのか

1. **測定対象が違う**  
   - IMC がメインで扱うのは**構造（コード）ベース**のカバレッジ  
   - `cover property` は**機能的・時相的イベント**が起きたかどうかにフォーカス  
   - そのため、同じテストを走らせても、「実際に到達した RTL の行数」と「指定した時相条件が満たされたか」では数字が異なりがちです。

2. **分母の捉え方が違う**  
   - 構造的カバレッジは「分岐点が何個あって、そのうち何個を通過したか」といった**ポイント総数**が分母  
   - カバープロパティでは「定義した各 property (sequence) が Covered か Uncovered か」で分母が決まる  
   - 定義した property が少なければ 1 つ達成するだけで高い％に見えるし、多ければ低く出ることもある

3. **目的が違う**  
   - 構造的カバレッジ → **テストベンチが十分網羅しているか、どの論理が未到達なのかを知る**  
   - カバープロパティ → **意図した機能シナリオが本当に起きたか**を検証し、機能カバレッジを補完する  

結果的に、IMC のカバレッジレポートと `cover property` のカバレッジは、「同じカバー率」の指標ではなく、全く別物なのです。

---

### 4. まとめ

- **IMC で見るカバー率 (構造的カバレッジ)** と **SVA のカバープロパティ** は、**測定対象や計算方法が異なる**ため、数値や評価基準も異なる。  
- 構造的カバレッジは **「テストが RTL コードのどこまで到達したか」** を示し、  
- カバープロパティ (cover property) は **「時相的・機能的なシナリオが発生したか」** を示す。  
- それぞれ役割が異なるため、**両方を併用して“網羅度”と“正しいシナリオの発生”をカバーする**のが一般的です。  
- レポート上も IMC では構造カバレッジがメイン表示になりますが、`cover property` の結果は “Functional Coverage” や “Assertions Coverage” のタブとして別枠で表示される場合が多く、**同列で比較するわけではありません**。

---

## 15. 参考文献


1. **SystemVerilog Assertions and Functional Coverage: Guide to Language, Methodology and Applications**  
   - **著者**: Ashok B. Mehta  
   - **概要**: アサーション言語の解説から、機能カバレッジとの連携方法、実践的な検証フローまで広範囲を網羅。SVA の習得にとても役立つ一冊。

2. **SystemVerilog for Verification: A Guide to Learning the Testbench Language Features**  
   - **著者**: Chris Spear, Greg Tumbush  
   - **概要**: SystemVerilog による検証（特にクラスベースのテストベンチやランダム化など）に焦点を当てた解説書。アサーションの話題もある程度カバーしている。

3. **Writing Testbenches in SystemVerilog (Second Edition)**  
   - **著者**: Janick Bergeron (一部リソースでは “Writing Testbenches Using SystemVerilog” というタイトル)  
   - **概要**: もともと VERA/UVM 系統をルーツにする検証メソドロジを扱いつつ、SystemVerilog の機能検証機能全般を解説。アサーションに関しては基礎的な使い方を紹介している。

4. **SystemVerilog for Design: A Guide to Using SystemVerilog for Hardware Design and Modeling (Third Edition)**  
   - **著者**: Stuart Sutherland, Simon Davidmann, Peter Flake  
   - **概要**: デザイン寄りの観点が強いが、アサーションの基礎や言語仕様についても一定の説明がある。検証というより RTL 設計面で SystemVerilog を活用したい人に有用。

5. **Assertion-Based Design (Second Edition)**  
   - **著者**: Harry D. Foster, Adam C. Krolnik, David J. Lacey  
   - **概要**: PSL/SVA 含むアサーションベース設計の概念を幅広く紹介。フォーマルやシミュレーションにおけるアサーション活用手法がまとまっている。

6. **IEEE 1800: SystemVerilog Language Reference Manual**  
   - **発行**: IEEE  
   - **概要**: 標準の言語仕様書（LRM）。教科書ではなく公式リファレンスだが、SVA の正確な仕様を調べる際に必須のドキュメント。
---

以上