Questa FSEでアサーション検証やってみた！
3.7K Views
November 02, 25
スライド概要
Questa - Altera FPGA Starter Editionにてアサーションを用いた検証が可能になったのでやってみました。
（ダウンロード不可）
関連スライド
各ページのテキスト
Questa FSEで アサーション検証やってみた！ 2025/11/8 RTLを語る会 (18) 発表資料 AUDIY (X: @AUDIY14)
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
自己紹介 • ハンドルネーム 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本（仮称）表紙の イラストレーター募集中です 現在のプロフィール画像
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
こんにちのRTL検証 増える要求仕様・機能ブロック 増えるコード行数 「やってられるかぁぁぁぁぁぁ！！！！！！！」 増える確認波形
こんにちのRTL検証 スケジュールの半分以上が検証なのに…[1] 市場流出するバグは増加傾向[1] 「効率的」かつ「抜け漏れのない」検証手法が 求められている
こんにちのRTL検証 取り入れている検証手法とバグ流出割合の関係[1] 「高度な検証」がバグ流出を未然に防ぐ 効果を発揮する(?)
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
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への移行
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
アサーション検証について (1) • RTLデザインやテストベンチ内に「設計上の期待条件」を 「ある文法に従って」埋め込むことで、シミュレーション時に仕様をチェックする 検証手法（「埋め込む期待条件」を「アサーション」と呼ぶ）[3]。 • 主に使用される言語（アサーション言語）は、以下の3種類ある。 (1). Property Specification Language (PSL) (2). SystemVerilog Assertion (SVA) (3). Open Verification Library (OVL) • 波形確認だけでは見落としがちな内容や、通信規格の違反などを自動監視する。 • 仕様違反をシミュレータが即座に設計者に報告することができる 「reqが立ち上がって3クロックサイクル以内にackが返される」仕様を波形だけで確認できるか？
アサーション検証について (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 ※単一サイクルのみ
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
アサーション検証の利点 1. デバッグ効率の向上 違反発生箇所やタイミングを即座に特定できる。 2. 検証カバレッジの向上 テストベンチだけでは捕捉困難な条件も監視可能。 3. 再利用性 IPごとにプロパティを定義して再利用可能。 4. フォーマル検証との親和性 アサーションの記述をもとに数学的な解析・検証を行う「フォーマル検証」という 手法がある。
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
アサーション検証実演 • 対象とするデザイン： ALTPLL (Altera FPGA内蔵PLLの一種)のクロック切り替え制御 ステートマシン • 概要：PLLの入力クロック切り替えシーケンスを実行する • サンプルプロジェクト： https://github.com/AUDIY/Questa_Verification_Tutorials/tree/m ain/05_Assertion aresetとclkswitchを ステートマシンで操作する ALTPLLブロック （MAX 10用） ALTPLLのマニュアル・クロック・スイッチオーバーのシーケンス概略図
アサーション検証実演 • マニュアルクロックスイッチオーバーのシーケンス[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のマニュアル・クロック・スイッチオーバーのシーケンス概略図
アサーション検証実演 作成したモジュールのブロック図 ALTPLLのマニュアル・クロック・スイッチオーバーのシーケンス概略図
アサーション検証実演 • モジュールの詳細シーケンス・仕様： 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のマニュアル・クロック・スイッチオーバーのシーケンス概略図
アサーション検証実演 • 仕様からアサーション（SVA）を書き起こす[4, 7]。 1. clksel信号とactiveclk信号が不一致になったら、clkswitch信号をLow→Highに 遷移させる。 Low→Highへの遷移を監視する
アサーション検証実演 • 仕様からアサーション（SVA）を書き起こす[4, 7]。 2. clkswitch信号は3クロックサイクル以上Highを維持する。 clkswitch信号のLow→High遷移を トリガに監視を開始する。
アサーション検証実演 • 仕様からアサーション（SVA）を書き起こす[4, 7]。 3. clkswitch信号がHighの間、areset信号はLowを維持する。
アサーション検証実演 • 仕様からアサーション（SVA）を書き起こす[4, 7]。 4. clkswitch信号をHigh→Lowに、areset信号をLow→Highに遷移させる。
アサーション検証実演 • 仕様からアサーション（SVA）を書き起こす[4, 7]。 5. aresetを10ns以上（パラメータでクロックサイクル指定）Highに維持する。 誤発火の防止 10ns以上の サイクルで代用 ※誤発火：シミュレーション開始直後等に意図せずにアサーションが開始・FAILすること
アサーション検証実演 • バッチファイル&マクロファイル準備[8] Questaの起動から一連のシミュレーションの実行までを行うバッチファイルおよび マクロファイルを準備する。
アサーション検証実演 • シミュレーション実行 必要なファイル一式を任意のディレクトリに格納し、シミュレーション用の バッチファイルを実行する。
アサーション検証実演 • シミュレーション結果確認 一般的なRTL波形確認と合わせて、アサーション結果を確認する。 アサーション結果概要
アサーション検証実演 • シミュレーション結果確認 一般的なRTL波形確認と合わせて、アサーション結果を確認する。 波形ウィンドウ上のアサーション結果 アサーション結果 （波形）
アサーション検証実演 • シミュレーション結果確認 一般的なRTL波形確認と合わせて、アサーション結果を確認する。 Assertion Thread Viewer
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
少し宣伝 Questa本（仮称）、出します！ 以下、主な構成 1. Questa – Altera FPGA Starter Editionの導入 2. RTLシミュレーションの方法（GUI & バッチファイル） 3. X/Z追跡 4. コードカバレッジ 5. アサーション検証 （←今回はこの内容を紹介） 現時点ではZennでの公開を予定。紙は需要があれば同人誌として出すかも？
アジェンダ 1.自己紹介 2.こんにちのRTL検証 3.Questa – Altera FPGA Editionについて 4.アサーション検証について 5.アサーション検証の利点 6.アサーション検証実演 7.少し宣伝 8.まとめ
まとめ 1. デザインの複雑化に伴う今日の検証の実態について紹介 2. Questa – Altera FPGA EditionとModelSim – Intel FPGA Editionとの差異を 紹介 3. アサーション検証の概要を紹介 4. Questa FSEを用いた実際のアサーション検証の一例を紹介 5. Questa本（仮称）の予告 いい加減 KR260 シバきたい
参考文献 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日）
- https://resources.sw.siemens.com/en-US/white-paper-2024-wilson-research-group-fpga-functional-verification-trend-report/
- https://www.altera.com/products/development-tools/quartus-prime/questa
- https://www.paltek.co.jp/semiconductor/maker/mentor/assertion/index.html
- https://www.intel.co.jp/content/www/jp/ja/docs/programmable/683047/16-0/manual-clock-switchover.html
- https://www.intel.co.jp/content/www/jp/ja/docs/programmable/683047/16-0/guideline-clock-switchover.html
参考文献 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日）
Thank you!