アサーションを用いたシミュレーションによる検証はアサーションベース検証（assertion based verification），略してABVと言われます．アサーションとは当該設計の特定の状況下で成り立つことが期待される性質の記述です．成り立っては困ることを記述して，問題が起こることがないかを調べることにも利用出来ます．
ABVを行うと短期間に設計品質を向上させることが出来るのは，問題の起こりやすい状況を試すようにテストベンチを調整して早期にバグを見出せるからです．漫然とシミュレーションしていては，問題の起こらない動作だけしか調べていない場合，バグを見逃すことになります．無論，アサーションを書くことは負担にもなります．効果的なアサーションの書き方を工夫する必要があります．ABVを行うかは，時間を掛けてもABVを行う価値があるかの「投資対効果」で判断します．
SystemVerilogで記述するアサーションはSystemVerilogアサーション（SystemVerilog assertion），略してSVAと言われます．SystemVerilogはハードエア記述言語Verilog HDLに完全上位互換な拡張で，アサーションを記述出来ます．SVAはVerilog HDLの記述とは別ファイルに記述出来ます．"bind.sv"というSystemVerilogファイルでアサーションとVerilogのモジュールをバインドします．
SVAについてはSystemVerilogアサーション（SVA）の書き方をご覧下さい．
ここではCadence社のIncisive Unified Simulator(IUS)のLinux版上でのSVAを用いたABVについて概説します．
IUS(Linux版)は様々な言語による記述を扱えますが，ここではVerilog HDLによる3段パイプラインRISCの記述にSystemVerilogによるアサーションを加えた記述"Computer_RISC_3BV"を例にIUS(Linux版)によるABVを概説します．
"Computer_RISC_3BV"はこのページの上の「Verilog HDLによるシステム開発と設計」のWEBサイトで"Verilog_SSMD_Ver1.31.zip"をダウンロードして展開すれば入手いただけます．
IUSをGUI環境で起動します．今いるディレクトリに,シミュレーションしようとするファイルだけしかないなら以下で良かったりします：
% irun -assert -sv *.v *.sv -access rwc -gui
何をしてほしいかを書いた"run.tcl"があるときは下記とします：
% irun -assert -sv *.v *.sv -input run.tcl -access rwc -gui
IUSが起動したところです：
SimVisionのConsoleで下記のコマンドを入力します：
ncsim> assertion -summary -show all
プリフェッチユニット（pfu）とバインドしたアサーション"pfu_checker"を選択して赤い楕円で示した"Send selected object(s) to target waveform window"をクリックします．"Design Browser"を小さくしていると"Send selected object(s) to target waveform window"は隠れていることもあります．適宜広げるなどしてみて下さい．
SimVisionが立ち上がります：
走らせるには赤い楕円で示したプレイボタンを押します．
ズームイン(ZoomInX)するには赤い楕円で示した「＋」印（Zoom in along the x-axis）を押します．
見る位置を移動させるには赤い楕円で示した下のバーを左右にスライドさせます．
検証したアサーションは下記です：
module pfu_prop(CLOCK1,STATE,FR);
input CLOCK1;
input [1:0] STATE,FR;
core_pfu_flag_forward: assert property
( @(posedge CLOCK1)
(STATE==2)##1(STATE==1)|->$past(FR)==FR );
endmodule
プリフェッチユニットがパイプライン・インターロックのための"WAIT"（STATE==2）から"FETCH"（STATE==1）に遷移したとき，1クロック前にフォワーディングされたフラグレジスタ"FR"の値は，このときの値に等しいという記述です．
プリフェッチユニットが"WAIT"（STATE==2）から"FETCH"（STATE==1）に遷移したとき，アサーションの前提が"active"になり，1クロック前のフラグの値"$past(FR)"とこの時点のフラグの値"FR"が一致しているため"finish"（成立）していることをSimVisionは示しています．ABVによって，正しくフォワーディングが行われていることが確認出来ました．
パイプライン・インターロックやフォワーディングについては拙著「Verilog HDLによるシステム開発と設計」をご覧下さい：
| 