RTLでデジタル回路を設計するときに、そのデジタル回路が正しく動作しているかどうかを検証するためには様々な方法がある。

知っているものを一覧でまとめてみた。

検証手法	特徴
セルフチェック検証	検証パタンそのものに、RTLが正しく動作したかどうかを検証する機構が入っている
Step-by-Step検証	検証パタンをRTLと別の検証ツール(ソフトウェアなど)で流し、ログが一致するかを確認する
静的検証	回路が仕様と一致しているかどうか、検証パタンを使わず静的に調査する

上記の一覧では、どちらかというとCPUの検証のようなものを想定しているが、別にCPUでないIPでも構わない。

セルフチェック検証

セルフチェック検証とは、パタンそのものが回路が正しく動作しているかどうかをチェックすることができる。例えば、以下のような機構を搭載する。

total = 0;
for(i = 1; i < 10; i++) {
  total = total + i;
}
if (total == 55) {
  Pass();
} else {
  Fail();
}

普通に実行するとPass以外になる訳が無いのだが、開発中のCPUでは計算を誤ることもあり、これをセルフチェックで確認する。ただし、セルフチェックする機構も設計し間違えていれば、誤ってPassと判定されることもあり、これが万全ではない。

次に、Step-by-Step検証とは、別のツールを用いて回路検証を行う方法である。例えばCPUの場合、RTLの出力した汎用レジスタへの書き込み記録と、ソフトウェア(命令セットシミュレータ:ISS)の汎用レジスタへの書き込み記録を一つ一つ比較していく。

Step-by-Step検証

RTLの書き込み記録

           235000000         0 [00000200] 00008197 : AUIPC     r 3,0x00008         ( 0,34) : R 3<=00008200
           255000000         1 [00000204] e1018193 : ADDI      r 3,r 3,0xe10       ( 1, 0) : R 3<=00008010
           255000000         2 [00000208] 0000c117 : AUIPC     r 2,0x0000c         ( 2,33) : R 2<=0000c208
           265000000         3 [0000020c] e0010113 : ADDI      r 2,r 2,0xe00       ( 3, 2) : R 2<=0000c008
           265000000         4 [00000210] 000000b3 : ADD       r 1,r 0,r 0         ( 4,32) : R 1<=00000000
           275000000         5 [00000214] 00000233 : ADD       r 4,r 0,r 0         ( 5,35) : R 4<=00000000
           275000000         6 [00000218] 000002b3 : ADD       r 5,r 0,r 0         ( 6,36) : R 5<=00000000

ISSの書き込み記録

         0:M:MBar:[00000200][P00000200] 00008197 : auipc      r03,0x00008          ( 0,34) r03<=00008200
         1:M:MBar:[00000204][P00000204] e1018193 : addi       r03,r03,0xe10        ( 1, 0) r03=>00008200 r03<=00008010
         2:M:MBar:[00000208][P00000208] 0000c117 : auipc      r02,0x0000c          ( 2,33) r02<=0000c208
         3:M:MBar:[0000020c][P0000020c] e0010113 : addi       r02,r02,0xe00        ( 3, 2) r02=>0000c208 r02<=0000c008
         4:M:MBar:[00000210][P00000210] 000000b3 : add        r01,r00,r00          ( 4,32) r00=>00000000 r00=>00000000 r01<=00000000
         5:M:MBar:[00000214][P00000214] 00000233 : add        r04,r00,r00          ( 5,35) r00=>00000000 r00=>00000000 r04<=00000000
         6:M:MBar:[00000218][P00000218] 000002b3 : add        r05,r00,r00          ( 6,36) r00=>00000000 r00=>00000000 r05<=00000000

これを比較して、全ての汎用レジスタへの書き込み記録が一致するかを検証する。