1990年代にはVerilog HDLで仕様を記述して，超高速論理シミュレータで動作を確認し，論理合成で回路を合成するという設計スタイルが日常化しました．「次の大きな変革は設計検証だ」と言われるようになりました．
論文が受理された教育についての国際会議Microelectronic Systems Education (MSE)と併催だったため，2005年のDesign Automation Conference(DAC)の会場を訪れることが出来ました．Cadence様，Synopsys様，Mentor様による「次の大きな変革は設計検証だ」というパネルディスカッションの様子です：
設計検証を行うEDAツールでは，特定の状況下で成り立つことが期待される性質をアサーションによって記述します．通常はシミュレーションを行い，注目する状況下で当該アサーションが成立するかを確認します．アサーションは成り立っては困ることを記述することにも利用出来ます．
アサーションを用いたシミュレーションによる検証はアサーションベース検証（assertion based verification），略してABVと言われます．アサーションを用いないシミュレーションでは見逃していたバグも，アサーションを試す方向でテストベンチを調整することで早期に見出せることが期待されます．
ABVによって，設計期間の短縮と設計品質の向上が期待できます．テストベンチを調整することでバグを早期に見出せるため，同じ開発期間ならABVを用いない場合より数多くのバグを見出すことが期待出来ます．同じ数のバグを見出すために必要な開発期間はABVを用いない場合より短くて済むことが期待されます．バグを見出し易いという意味で，良いアサーションを書けていることが前提になります．
SystemVerilogで記述するアサーションはSystemVerilogアサーション（SystemVerilog assertion），略してSVAと言われます．SystemVerilogはハードウェア記述言語Verilog HDLに完全上位互換な拡張で，アサーションを記述出来ます．
SVAは設計を書いているVerilog HDLの記述とは別ファイルに記述出来ます．"bind.sv" というSystemVerilogファイルでアサーションとVerilogのモジュールをバインドします．バインド（bind）はSystemVerilogで別ファイルに記述したアサーションを注目するVerilog HDLのモジュール内に記述したのと同じ扱いにする技術です．アサーションを注目するモジュールに置いたことにする技術はバインディングと言われます．
ここではSystemVerilogアサーション（SVA）の書き方を概説します．
時間の概念がなく，真か偽かだけを問題にする論理は命題論理と言われます．時間の概念を有し，どのような可能世界（possible world）があるかを考えて，それぞれの可能世界での論理式の真偽を問題にする論理は様相論理（modal logic）と言われます．
「Aさんはお腹が空いている」が仮に真だったとしても，食事をすれば満腹になります．食事をしていない世界，食事をした世界が可能世界の例です．「Aさんはお腹が空いている」は食事をする前の世界でしか成り立たない論理式の例です．時間が経ってまたお腹が空くことなどを思えば可能世界はたくさん考えられます．BさんやCさんの存在を考えても可能世界は増えます．
様相論理の中でも特にコンピュータの状態変化を扱う論理は時相論理（temporal logic）と言われます．ソフトウエアの場合はi=i+1を実行することで別の可能世界に遷移したりします．i<7という条件での繰り返し文があったとしましょう．iが7未満の可能世界とｉが7以上という可能世界が考えられます．i<7は前者で真となる論理式です．
不等式が他にもあったり，変数が多ければ状態数（可能世界の数）はすぐ凄まじい数に増えます．そもそも，32ビットレジスタが1個あるだけで，そのままでは2の32乗個の状態があるわけです．「状態爆発」として知られる問題です．
EDAベンダーが供給しているフォーマルなベリファイアがCPU内部を対象にしてはアサーションを検証出来ない理由です．
状態爆発の問題を解決するために各変数の個々の具体的な値ではなく，負の数，零，正の数のように扱う工夫は「抽象化」と言われます．
様相論理式を解釈するための構造をクリプキ構造（Kripke structure）といいます．Wを可能世界の集合，Rを可能世界間の到達可能性関係（reachability relation），Vを論理記号に対する各可能世界での真偽の割り当て（assignment）としたとき，クリプキ構造はS=(W,R,V)という組みとして定義されます．
SVAでは命題論理と時相論理の両者を扱えます．
セレクタの出力はどんな時点にも，どれか1つの信号線だけが1になっていないと困ります．すべて0でも構いません．16ビット幅のselect信号は多くてもどれか1つしか1にならないことをSVAでは以下のように表現します：
assert property ($onehot0(select[15:0]);
SVAでは「コンディション」と言われます．時間の指定がなく，常時成り立っていることを要求する命題論理の記述です．
AとBの値が等しかったら次のクロックでCが1になり，その次のクロックではDが1になることをSVAでは以下のように表現します：
assert property (A==B |=> C ##1 D);
SVAでは「レスポンス」と言われます．特定の状態でのみ1になる信号を扱っているので時相論理の記述だと考えられます．
"|=>"はノン・オーバーラップインプリケーションと言われ，右側には次のクロックで成立が期待される事柄を記述します．Cが1になったあと2クロックでDが1になるなら，"C ##2 D"と書きます．
同じ時刻に成立が期待される事柄は"|->"で表現します．オーバーラップインプリケーションと言われます．
assert property (A==B |-> C ##3 D);
はAとBの値が等しかったら同じクロックでCは1であり，3クロック後にDが1になるという記述です．
「レスポンス」は，if文で条件を指定して動作を記述するVerilog HDLと似ており，調べる意味のないアサーションに成りがちです．SVAには「レスポンス」とは逆の，「こうなったらこうだった筈だ」という記述方法もあって，「スティミュラス」と言われます．
具体的に，データメモリにストア（格納）されたデータを覚えておく設計で，覚えておいたデータが新たなオペランドとしてそのまま使われたなら，読みだそうとしたデータのアドレスは先行するストア命令のアドレスと同じだった筈だというSVAは以下のように表現されます：
assert property
(@(posedge(CLOCK1) $past(STORE_DATA)==OPERAND_BUFER
|->$past(INSTRUCTION_BUFFER[7:0],2)==$past(STORE_ADDRESS));
ここに"$past(STORE_DATA)"はストアされたデータSTORE_DATAの1クロック前の値で，覚えておいたデータを意味します．"$past"は過去に遡って値を参照する手段です．STORE_DATAの1クロック前の値がそのまま次の計算のオペランドとしてバッファに置かれたら，2クロック前のINSTRUCTION_BUFFER[7:0]の値は直前のストア命令のアドレスと等しかった筈だというアサーションです．
上記のアサーションは2011年にサンディエゴで開催された教育についての国際会議MSE2011で紹介しました．「設計に誤りがないかを，スティミュラスを使って，元のVerilog HDL記述とは逆の書き方をして調べる」という工夫は，Cadence社様からも，Mentor社様からも高い評価をいただきました．この年もMSEと併催だった2011年のDACの会場の様子です：
アドレス信号が2クロック変化しないという事柄は
$stable(address)[*2];
のように表現します．
書き込み信号WRITEが立ち上がったらアドレス信号ADRは次のクロックから2クロック安定していなければならないことはSVAでは以下のように表現します：
assert property ($rose(WRITE)|=>$stable(ADR)[*2]);
一定期間成り立つべき性質の記述は「スタビリティ」と言われます．時相論理の記述だと考えられます．
REQが立ち上がったら，いずれGRANTが1になることは以下のように表現されます：
assert property ($rose(REQ)|=> ##[0:$] GRANT);
時相論理には大きく分けて線形時間時相論理LTLと計算木論理CTLがあります．LTLには時相演算子（temporal operator）のU(Until), F(some Future state), G(Globally)そしてX(neXt state)があります．LTLではクリプキ構造における特定の遷移経路上での性質が扱われます．Fpはいずれ命題pが成立することを表しており，上記のSystemVerilog記述はLTLの"F GRANT"に対応していると考えられます．
特定のクリプキ構造で注目する時相論理式が成立するかを形式的に調べることはモデル検査（model checking）と言われます．個々の経路上で成り立つ性質を記述するLTL式はすべての経路において成立する場合に満たされると判定されます．状態爆発を抑えるための抽象化には「もとのクリプキ構造にある遷移関係は抽象化されたクリプキ構造にも存在しなければならない」などの条件を満たす写像が用いられます．
クリプキ構造におけるCTLではLTLの時相演算子の他に経路限定子（path quantifiers）のA(All paths)とE(Exists a path)が 加わります．AXpはどの経路に遷移しても次の状態でpが成り立つという記述になります．CTLでは経路限定子が加わって記述能力が高まったように思えますが，特定の経路上で成立する性質の記述は出来なくなります．他方で，LTLでは何らかの性質を満たす経路が存在するといった記述は出来ません．
「どう遷移しようとハザードは生じない」というマイクロアーキテクチャの性質はCTLで扱われます．
バインドするアサーションは以下のようにモジュールとして記述します：
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）に遷移したとき，正しくフォワーディングが行われているかを検証する記述になっています．"$past(FR)"は1クロック前にフォワーディングされたフラグレジスタFRの内容を表し，"FR"は更新されたフラグレジスタの内容を表しています．このアサーションも2011年にサンディエゴにて開催された教育についての国際会議MSE2011で紹介しました．
この記述がプリフェッチユニットの記述なら"bind.sv"というファイルには以下のように記述します：
bind prefetch_unit pfu_prop pfu_checker(CLOCK1,STATE,FR);
"prefetch_unit"はVerilog HDLでのモジュール名，"pfu_prop"はアサーションを記述した上記のモジュール名，"pfu_checker"という名は任意です．"pfu_checker"という名はSimVisionなどのツールで当該アサーションを選択するとき表示される名になります．
筆者（高橋隆一）は広島市立大学に最初の3年生が誕生した1996年（平成8年）4月以来，コンピュータというたったひとつの装置のためだけに存在していた情報工学科最後の3年生を育てるまでの13年間，全く自由なアーキテクチャ，マイクロアーキテクチャのFPGAコンピュータを一人一台設計し，製作までをさせる情報工学実験City-1をVerilog HDLを使って実施していました．
City-1を履修出来なくなった2010年度以降の4年生には，毎年，筆者を選んだ数名にですが，卒業研究で一人一台マイクロコンピュータを設計してもらうことにしました．思った通りのコンピュータが設計されているかの検証方法を研究してもらっています．City-1のような製作はしない代わりにSystemVerilogアサーションを使ってABVの研究をするという卒業研究を始めたのです．「どうすればバグを見出し易いアサーションを書けるか」という問いを卒業研究の課題にしました．
SVAでABV中の錦織光輝くんです
開発コードmaruCs164のコンピュータは2016年度の卒業研究で錦織光輝くんによって設計された最大マッチング問題向け専用プロセッサ（ASIP）です．以下に錦織光輝くんによる卒業研究のプレゼンテーション資料を示します：
maruCs164の設計検証
"maruCs164"は3段パイプラインRISCの記述"Computer_RISC_3BV"をひな形として設計されたASIPでした．"Computer_RISC_3BV" を入手するにはこのページの上の「Verilog HDLによるシステム開発と設計」のWEBサイトで"Verilog_SSMD_Ver1.31.zip" をダウンロードして展開します．
"Computer_RISC_3BV"は同様に入手いただける3段パイプラインRISCの記述 "Computer_RISC_3" や "Computer_RISC_3A" の実行ユニットに内部バスを置いてレジスタとALUの間の接続を簡単にした記述 "Computer_RISC_3B" にSystemVerilogアサーションの記述を含めたSystemVerilogの記述例です．
ここに掲げた3段パイプラインRISCの記述はすべてVerilog HDLでの状態遷移による筆者が工夫した動作記述になっています．プリフェッチ・ユニットがIDLE，FETCH，WAITという3つの状態を持っています．
以下はInternational Journal of Computer Science and Network Security(IJCSNS), Vol.16 No.10, pp.116-121 (2016)で紹介したVerilog HDLによる状態遷移を用いた動作記述，静的オートマトン記述(SSMD)の記述例です：
「オートマトン記述」は状態単位にレジスタ間転送を列挙して次の状態を指定していることを意味します．オートマトン記述は状態遷移によって手続き的な動作を表現します．この記述例にはIDLE,FETCHという2つ状態が示されています．筆者が指導に使っている3段パイプラインRISCの記述にはIDLEとFETCHの他にパイプライン・インターロックのためのWAITという状態があります．
前述したプリフェッチユニットについてのアサーションは状態がWAITからFETCHに遷移したときフォワーディングが正しく行われていたかを検証するための記述でした．このアサーションをCadence社のIncisive Unified Simulator(IUS)のLinux版を用いて検証する方法がIUS(Linux版)によるアサーションベース検証（ABV）でご覧いただけます．状態の概念を持っていることが問題点の絞り込みを簡単にしています．
問題点の絞り込み以前に，状態遷移を行わせる動作記述を用いれば，RTL記述として知られる構造記述よりずっと簡単にマイクロアーキテクチャを設計出来ます．筆者が指導する卒業研究ではASIPへの改造についても実行ユニットに専用命令のための状態遷移を行わせるステートマシンを加筆するという指導を行っています．
Verilog HDLによるRTLでの状態遷移を用いた動作記述で「ユークリッドの互除法」のアルゴリズムを書き下した例が2008年の拙著
の第2章でご覧いただけます．拙著ではユークリッドの互除法のアルゴリズムを記述した例は「論理合成ツールが扱えない可能性がある」と書いていますが，Synopsys社の方は当たり前のように「何の問題もなく合成出来る」とおっしゃっていました．Synopsys社のツールを使えば，IEEE1364のVerilog HDLで何の問題もなく高位合成が行えるという話です．
ハザードやパイプライン・インターロック，フォワーディングについても拙著でご覧いただけます．
筆者が工夫したとは言ってもVerilog HDLによるRTLでの様態遷移による動作記述，SSMDはIEEE1364標準です．Verilog HDLは非常に広範な記述能力を持ったHDLで，オートマトン記述も仕様の一部だったのです．問題は合成ツールが賢い合成をしてくれるかでした．マイクロコンピュータ設計教育環境City-1で愛用していたSynplifyという合成ツールは期待に応えてくれ，世界最高水準のマイクロコンピュータ設計教育City-1を支えてくれました．
マイクロコンピュータ設計教育環境City-1で愛用していたSynplicity社のSynplify Premierという合成ツールを用いた合成完了の画面を以下に例示します，拙著，第2章のユークリッドの互除法のアルゴリズムを記述したVerilog HDLによる動作記述"EA.v"を合成した結果です：
より一般的なVerilog HDLによる動作記述からのSynplify Proによる高位合成がVerilogによる動作記述(SSMD)からのSynplifyによる合成でご覧いただけます．
関連する話題がVerilog HDLによる動作記述と構造記述：City-1の最終年度でご覧いただけます．高位合成だからといって，妙な動作記述を使う理由は全くありません．Verilog HDLによるオートマトン記述を対象に，RTオペレーションを別の状態（タイミング）に移動させない高位合成を行わせる方が好ましい場合だってあるでしょ．クロック信号に同期した動作を書けるVerilog HDLによる動作記述の方が，クロック信号を書かない動作記述より優れているという話です．
Verilog HDLによる動作記述を工夫した背景についてはNEC主任時代の高橋隆一：オートマトン記述からの高位合成でご覧いただけます．
