---
title: Questa FSEでアサーション検証やってみた！
tags:  #fpga #verilog #systemverilog #altera #questa #systemverilog assertion #sva  
author: [AUDIY](https://www.docswell.com/user/AUDIY)
site: [Docswell](https://www.docswell.com/)
thumbnail: https://bcdn.docswell.com/page/YJ6LRD29EV.jpg?width=480
description: Questa - Altera FPGA Starter Editionにてアサーションを用いた検証が可能になったのでやってみました。
published: November 02, 25
canonical: https://www.docswell.com/s/AUDIY/KYVJD3-2025-11-02-193838
---
# Page. 1

![Page Image](https://bcdn.docswell.com/page/YJ6LRD29EV.jpg)

Questa FSEで
アサーション検証やってみた！
2025/11/8
RTLを語る会 (18) 発表資料
AUDIY (X: @AUDIY14)


# Page. 2

![Page Image](https://bcdn.docswell.com/page/GJ51832D74.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 3

![Page Image](https://bcdn.docswell.com/page/LE31861Q75.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 4

![Page Image](https://bcdn.docswell.com/page/8EDXMVXWJG.jpg)

自己紹介
• ハンドルネーム
AUDIY (X: @AUDIY14)
• 職業
とある企業の電子回路設計部門
• FPGA遍歴
Altera: MAX 10/Cyclone IV E/Cyclone 10 LP
AMD: Spartan-7/Artix-7/KRIA KR260
Efinix: Trion T20
Gowin: Arora GW2A-LV18
• 最近の活動
2倍オーバーサンプリングデジタルフィルタIP（GitHub: FIR_x2）
Questa本（仮称、準備中）
• 悩み・連絡事項
プロフィール画像・Questa本（仮称）表紙の
イラストレーター募集中です
現在のプロフィール画像


# Page. 5

![Page Image](https://bcdn.docswell.com/page/V7PPRVPX78.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 6

![Page Image](https://bcdn.docswell.com/page/2JV2RZ23JQ.jpg)

こんにちのRTL検証
増える要求仕様・機能ブロック
増えるコード行数
「やってられるかぁぁぁぁぁぁ！！！！！！！」
増える確認波形


# Page. 7

![Page Image](https://bcdn.docswell.com/page/5EGRM4RYJL.jpg)

こんにちのRTL検証
スケジュールの半分以上が検証なのに…[1]
市場流出するバグは増加傾向[1]
「効率的」かつ「抜け漏れのない」検証手法が
求められている


# Page. 8

![Page Image](https://bcdn.docswell.com/page/4JQVRGV67P.jpg)

こんにちのRTL検証
取り入れている検証手法とバグ流出割合の関係[1]
「高度な検証」がバグ流出を未然に防ぐ
効果を発揮する(?)


# Page. 9

![Page Image](https://bcdn.docswell.com/page/K74M85MMJ1.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 10

![Page Image](https://bcdn.docswell.com/page/LJ182W8YEG.jpg)

Questa – Altera FPGA Editionについて[2]
• AlteraのFPGA開発ソフトウェアQuartus Primeに付属するSiemens EDA製の
論理シミュレータ（Questa Coreがベース）。
• 2021年10月以降のバージョンにて、それまで付属されていたModelSimから変更された。
• ModelSim FPGA Editionと比較して以下機能が使用可能になった（検証機能が充実した）。
(1). コードカバレッジ
(2). パフォーマンス・プロファイラ
(3). Schematic/Dataflow diagram
(4). 信号追跡
(5). アサーション検証（SVA/PSL）
• 有償版（FPGA Edition）と無償版（FSE: FPGA Starter Edition）がある。
• その他詳細は以下リンク先へ
https://www.altera.com/products/development-tools/quartus-prime/questa
ModelSimからQuestaへの移行


# Page. 11

![Page Image](https://bcdn.docswell.com/page/GJWZR6Z1J2.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 12

![Page Image](https://bcdn.docswell.com/page/4EZ1RY1X73.jpg)

アサーション検証について (1)
• RTLデザインやテストベンチ内に「設計上の期待条件」を
「ある文法に従って」埋め込むことで、シミュレーション時に仕様をチェックする
検証手法（「埋め込む期待条件」を「アサーション」と呼ぶ）[3]。
• 主に使用される言語（アサーション言語）は、以下の3種類ある。
(1). Property Specification Language (PSL)
(2). SystemVerilog Assertion (SVA)
(3). Open Verification Library (OVL)
• 波形確認だけでは見落としがちな内容や、通信規格の違反などを自動監視する。
• 仕様違反をシミュレータが即座に設計者に報告することができる
「reqが立ち上がって3クロックサイクル以内にackが返される」仕様を波形だけで確認できるか？


# Page. 13

![Page Image](https://bcdn.docswell.com/page/Y76LRDLPJV.jpg)

アサーション検証について (2)
• 以下の箇所でのアサーション検証の使用が多い、又は、推奨されている[4]。
(1). ブロック間インタフェース（AMBA AXIなど）
(2). ブロック内のインタフェース（ハンドシェークなど）
(3). コントロール・ロジック（非同期FIFOのアービタなど）
(4). ステートマシン
• 以下のような箇所でのアサーションの挿入はメリットが小さいとされる[4]。
(1). 非同期信号に対するアサーション
(2). RTLから仕様が容易にわかるようなアサーション
（フリップフロップの縦続接続で作られたシフトレジスタなど）
(3). 即時アサーション
(4). チップ間インタフェース（PCIeなど）
• 無償ツールでは以下で検証可能
(1). Questa FSE（今回使用するツール）
(2). Dsim Desktop
(3). Vivado
(4). Verilator ※単一サイクルのみ


# Page. 14

![Page Image](https://bcdn.docswell.com/page/G751831PE4.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 15

![Page Image](https://bcdn.docswell.com/page/9J21KZ1Z7R.jpg)

アサーション検証の利点
1. デバッグ効率の向上
違反発生箇所やタイミングを即座に特定できる。
2. 検証カバレッジの向上
テストベンチだけでは捕捉困難な条件も監視可能。
3. 再利用性
IPごとにプロパティを定義して再利用可能。
4. フォーマル検証との親和性
アサーションの記述をもとに数学的な解析・検証を行う「フォーマル検証」という
手法がある。


# Page. 16

![Page Image](https://bcdn.docswell.com/page/DEYZNRZN7M.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 17

![Page Image](https://bcdn.docswell.com/page/VJN3XD3VJ8.jpg)

アサーション検証実演
• 対象とするデザイン：
ALTPLL (Altera FPGA内蔵PLLの一種)のクロック切り替え制御
ステートマシン
• 概要：PLLの入力クロック切り替えシーケンスを実行する
• サンプルプロジェクト：
https://github.com/AUDIY/Questa_Verification_Tutorials/tree/m
ain/05_Assertion
aresetとclkswitchを
ステートマシンで操作する
ALTPLLブロック （MAX 10用）
ALTPLLのマニュアル・クロック・スイッチオーバーのシーケンス概略図


# Page. 18

![Page Image](https://bcdn.docswell.com/page/YE998G9VE3.jpg)

アサーション検証実演
• マニュアルクロックスイッチオーバーのシーケンス[5, 6]：
1. PLL入力切替スタート時にclkswitch信号をLow→Highに遷移
させる。
2. clkswitch信号のHighを「PLL入力の周波数が低いクロック」
3サイクル分以上維持する。
3. clkswitch信号を3サイクル以上維持したら、areset信号を
Low→Highに遷移させる。
4. areset信号を10ns以上Highに維持したらシーケンス完了。
5. 「PLLからのactiveclk出力が所望の入力に対応している」かつ
「PLLからのlocked出力がHighになっている」状態で成功。
ALTPLLブロック （MAX 10用）
ALTPLLのマニュアル・クロック・スイッチオーバーのシーケンス概略図


# Page. 19

![Page Image](https://bcdn.docswell.com/page/GE898V947D.jpg)

アサーション検証実演
作成したモジュールのブロック図
ALTPLLのマニュアル・クロック・スイッチオーバーのシーケンス概略図


# Page. 20

![Page Image](https://bcdn.docswell.com/page/LELWR5WVJR.jpg)

アサーション検証実演
• モジュールの詳細シーケンス・仕様：
1. clksel信号とactiveclk信号が不一致になったら、clkswitch信号をLow→Highに
遷移させる。
2. clkswitch信号は3クロックサイクル以上Highを維持する。
この間、aresetはLowを維持する。
3. clkswitch信号をHigh→Lowに、areset信号をLow→Highに遷移させる。
4. aresetを10ns以上（パラメータでクロックサイクル指定）Highに維持したら、
High→Lowに遷移させる。
5. 数クロックサイクル（パラメータで指定）待ち、locked信号がHighかつ
activeclkとclkselの論理が一致していれば完了。
いずれかの条件を満たしていなければもう一度aresetのみトグルする。
ALTPLLのマニュアル・クロック・スイッチオーバーのシーケンス概略図


# Page. 21

![Page Image](https://bcdn.docswell.com/page/4JM9R39NEW.jpg)

アサーション検証実演
• 仕様からアサーション（SVA）を書き起こす[4, 7]。
1. clksel信号とactiveclk信号が不一致になったら、clkswitch信号をLow→Highに
遷移させる。
Low→Highへの遷移を監視する


# Page. 22

![Page Image](https://bcdn.docswell.com/page/PJRGRQG4E9.jpg)

アサーション検証実演
• 仕様からアサーション（SVA）を書き起こす[4, 7]。
2. clkswitch信号は3クロックサイクル以上Highを維持する。
clkswitch信号のLow→High遷移を
トリガに監視を開始する。


# Page. 23

![Page Image](https://bcdn.docswell.com/page/PEXXR5XZEX.jpg)

アサーション検証実演
• 仕様からアサーション（SVA）を書き起こす[4, 7]。
3. clkswitch信号がHighの間、areset信号はLowを維持する。


# Page. 24

![Page Image](https://bcdn.docswell.com/page/3EKWR6WVED.jpg)

アサーション検証実演
• 仕様からアサーション（SVA）を書き起こす[4, 7]。
4. clkswitch信号をHigh→Lowに、areset信号をLow→Highに遷移させる。


# Page. 25

![Page Image](https://bcdn.docswell.com/page/L73186WQJ5.jpg)

アサーション検証実演
• 仕様からアサーション（SVA）を書き起こす[4, 7]。
5. aresetを10ns以上（パラメータでクロックサイクル指定）Highに維持する。
誤発火の防止
10ns以上の
サイクルで代用
※誤発火：シミュレーション開始直後等に意図せずにアサーションが開始・FAILすること


# Page. 26

![Page Image](https://bcdn.docswell.com/page/87DXMVKWEG.jpg)

アサーション検証実演
• バッチファイル&マクロファイル準備[8]
Questaの起動から一連のシミュレーションの実行までを行うバッチファイルおよび
マクロファイルを準備する。


# Page. 27

![Page Image](https://bcdn.docswell.com/page/VJPPRVKXJ8.jpg)

アサーション検証実演
• シミュレーション実行
必要なファイル一式を任意のディレクトリに格納し、シミュレーション用の
バッチファイルを実行する。


# Page. 28

![Page Image](https://bcdn.docswell.com/page/2EV2RZV3EQ.jpg)

アサーション検証実演
• シミュレーション結果確認
一般的なRTL波形確認と合わせて、アサーション結果を確認する。
アサーション結果概要


# Page. 29

![Page Image](https://bcdn.docswell.com/page/57GRM4LYEL.jpg)

アサーション検証実演
• シミュレーション結果確認
一般的なRTL波形確認と合わせて、アサーション結果を確認する。
波形ウィンドウ上のアサーション結果
アサーション結果
（波形）


# Page. 30

![Page Image](https://bcdn.docswell.com/page/4EQVRGY6JP.jpg)

アサーション検証実演
• シミュレーション結果確認
一般的なRTL波形確認と合わせて、アサーション結果を確認する。
Assertion Thread Viewer


# Page. 31

![Page Image](https://bcdn.docswell.com/page/KJ4M85WME1.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 32

![Page Image](https://bcdn.docswell.com/page/LE182WYY7G.jpg)

少し宣伝
Questa本（仮称）、出します！
以下、主な構成
1. Questa – Altera FPGA Starter Editionの導入
2. RTLシミュレーションの方法（GUI & バッチファイル）
3. X/Z追跡
4. コードカバレッジ
5. アサーション検証 （←今回はこの内容を紹介）
現時点ではZennでの公開を予定。紙は需要があれば同人誌として出すかも？


# Page. 33

![Page Image](https://bcdn.docswell.com/page/GEWZR6G1E2.jpg)

アジェンダ
1.自己紹介
2.こんにちのRTL検証
3.Questa – Altera FPGA Editionについて
4.アサーション検証について
5.アサーション検証の利点
6.アサーション検証実演
7.少し宣伝
8.まとめ


# Page. 34

![Page Image](https://bcdn.docswell.com/page/47Z1RYLXJ3.jpg)

まとめ
1. デザインの複雑化に伴う今日の検証の実態について紹介
2. Questa – Altera FPGA EditionとModelSim – Intel FPGA Editionとの差異を
紹介
3. アサーション検証の概要を紹介
4. Questa FSEを用いた実際のアサーション検証の一例を紹介
5. Questa本（仮称）の予告
いい加減
KR260
シバきたい


# Page. 35

![Page Image](https://bcdn.docswell.com/page/YJ6LRDWPEV.jpg)

参考文献
1. Siemens EDA. 2024 Wilson Research Group FPGA Functional Verification Trend Report. Siemens
Software, 2024. Available online: https://resources.sw.siemens.com/en-US/white-paper-2024wilson-research-group-fpga-functional-verification-trend-report/
2. Altera, 「Questa* – Altera® FPGA Edition」, https://www.altera.com/products/developmenttools/quartus-prime/questa（参照日：2025年10月26日）
3. PALTEK, 「アサーションベース検証とは」, PALTEK公式ウェブサイト,
https://www.paltek.co.jp/semiconductor/maker/mentor/assertion/index.html （参照日：2025
年10月26日）
4. 東野輝夫・岡野浩三・中田明夫（監訳）, 「アサーションベース設計 原書第2版」, 丸善出版, 2004
年, ISBN: 978-4-621-07449-7.
5. インテル株式会社, 「Manual Clock Switchover」, Intel® FPGA Handbook, 第16.0版,
https://www.intel.co.jp/content/www/jp/ja/docs/programmable/683047/16-0/manual-clockswitchover.html （参照日: 2025年10月26日）
6. インテル株式会社, 「Guidline: Clock Switchover」, Intel® FPGA Handbook, 第16.0版,
https://www.intel.co.jp/content/www/jp/ja/docs/programmable/683047/16-0/guidelineclock-switchover.html （参照日: 2025年10月26日）


# Page. 36

![Page Image](https://bcdn.docswell.com/page/GJ5183MP74.jpg)

参考文献
7. proty, 「SVA（SystemVerilog Assertion）簡単なサンプル集」, 平凡なる好奇,
https://www.progresstype.com/search/label/SVA （参照日: 2025年10月26日）
8. PALTEK, 「【入門】ModelSimの使い方 ＜バッチスクリプト実行＞ ～ModelSim 2021.1
ModelSim Intel Edition, Microsemi Edition, ModelSim DE/PE/SE, QuestaSim対応版 ～」,
PALTEK公式ウェブサイト, https://www.paltek.co.jp/techblog/techinfo/210305_02
（参照日: 2025年11月2日）


# Page. 37

![Page Image](https://bcdn.docswell.com/page/9E21KZ9ZJR.jpg)

Thank you!