Verification procedure

RISC-V Formalのテストは、ISA準拠性を検証するために実行されるものである。

コア全体の複雑さ及び対象アプリの検証要件にといった側面に応じて、2種類のテストとして分類される。

RISC-V Formalを実行するもっとも単純な方法は、ラッパーのHDLモジュールと、 checks.cfg ファイルを作成して、 genchecks.py スクリプトを用いて形式的なチェック環境を生成する、というものである。

このとき、 genchecks.py により生成されるチェックは有界モデル検査である。検証には、 sby が用いられる。

Configuring check generation

まずは、 .cfg 設定ファイルを用いて genchecks.py を構成し、チェック環境を生成する。

genchecks.py は cores フォルダのサブディレクトリから呼び出されることを前提としている。

checks.cfg に記述すべき内容を以下に説明する：

本セクションは主としてテスト対象のコアの属性を記述する。

Option / Value / Description
- isa / String / ISA 拡張(例：RV64IMAFD, rv32i)。詳細は下記 Supported ISAs を参照。
- nret / Integer / RVFI ポートのチャネル数。既定値は 1。
- blackbox / None / レジスタファイルおよび ALU をブラックボックス化する指定である。
- solver / String / ソルバ名。既定は boolector。
- dumpsmt2 / None / smtbmc エンジンに SMT2 トレース出力を指示する。
- abspath / None / 生成 Makefile が生成物への絶対パスを用いる。
- mode / String / ソルバモード。bmc もしくは prove をサポートし、既定は bmc である。

以下の RISC-V ISA モジュールをテスト対象としてサポートする：

rv32i(Version 2.1) — 基本整数命令セット(32bit)。
rv64i(Version 2.1) — 基本整数命令セット(64bit)。
c(Version 2.0) — 圧縮命令拡張。
m(Version 2.0) — 整数乗算・除算拡張。
Zicsr(Version 2.0) — CSR は別扱いであり、isa 文字列に “Zicsr” を含めないこと(CSR チェックを参照)。
b(Version 1.0) — Zba/Zbb/Zbs によるビット操作命令群の集合。
Zba(1.0) — アドレス生成。
Zbb(1.0) — 基本ビット操作。
Zbc(1.0) — キャリーレス乗算。
Zbs(1.0) — 単一ビット命令。
Zbkb(1.0) — 暗号向けビット操作。
Zbkc(1.0) — 暗号向けキャリーレス乗算。
Zbkx(1.0) — クロスバー置換。

各拡張に対する命令テストは、rv32i と rv64i の両ベースに対して利用可能である(例：isa rv32iZbc)。同一設定ファイルでの複数拡張の同時指定は現状限定的であり、既定で利用可能な組み合わせは以下である：

Warning

isa 文字列は大文字小文字を区別し、上表の値と完全一致させる必要がある(命令テスト生成のため)。

必要に応じて insns/generate.py スクリプトにより追加の組み合わせをローカル生成できる。まず次のコード箇所を見つける：

## Additional ISA combinations
isa_propagate("Zba_Zbb_Zbc_Zbs")
isa_propagate("Zbkb_Zbkc_Zbkx")

上記の実装に対して、 isa_propagate("mcb")を追加することによって、各組合せに対して、テストとのための環境が生成される。

ソルバが用いる実行深度を与える。

[depth]
insn            20
reg       15    30
pc_fwd    10    30
pc_bwd    10    30
liveness  1  10 30
unique    1  10 30
causal    10    30

チェック名の前に付与するグループ名を定義する。

複数チェックをグルーピングし、複数の深度でテストすることができる。

例：groups a b かつ深度設定が a_insn <x>, b_insn_bne <y> の場合、全命令が深度 x でテストされ、bne 命令は深度 x と y の両方でテストされる。

本オプションが定義されると、列挙されたチェックは記述順に実行され、未記載のチェックよりも先に実行される。

[sort]
reg_ch0  # reg_ch0が最も最初に実行され、それ以外が次に実行される

このソートは、Makefile におけるチェック生成順も規定する。Make により起動順は保持されるべきであるが、並列化が有効な場合、完了順がこの順序と一致する保証はない。

+ または - に続けて空白とチェック名(正規表現可)を列挙することで、個別のチェックを有効／無効にできる。最初にマッチした規則が適用される点に注意すること。

例：+ insn_(mul|div)_ch1 を - insn_.*_ch1 より先に置けば、チャネル 1 では mul と div のみが有効となり、他の命令は無効になる。

各行は 2 値のタプルとなっている：

第 1 値は現在のチェック名にマッチさせる正規表現パターン
- ! で始まる場合、そのコードはマッチしないすべてのチェックに適用される。
- そうでなければ、マッチするすべてのチェックに適用される。
第 2 値は assume_stmts.vh に挿入されるコードである。