前回の続きだ。メモリアクセスの検証用インタフェースについて見てみよう。
外部メモリバスの処理
RISC-V Formalの仕様では、RVFI経由で観測されるコアが生じさせるメモリアクセスと、それに伴って発生するデータバス上で観測されるメモリアクセスとの整合性を検証するチェック機能が含まれている。このための専用のインタフェースであるRVFI_BUSが定義されている。
例えば、コアのメモリアクセスに伴いリクエストがバス上に現れ、その数サイクル後にコアがその応答を受け取ってコアとしてのメモリアクセスが完了する場合、まずRVFI_BUSがバスのアクセスを出力しておく必要がある。この場合、バスアクセスの記録と、実際のコアのアクセスの記録がどれくらい離れるかによっては適切に制約が行えなくなり、誤検知が発生する可能性がある。
RVFI_BUSは以下の信号を追加する。
output [NBUS * 1 - 1 : 0] rvfi_bus_valid output [NBUS * 1 - 1 : 0] rvfi_bus_insn output [NBUS * 1 - 1 : 0] rvfi_bus_data output [NBUS * 1 - 1 : 0] rvfi_bus_fault output [NBUS * XLEN - 1 : 0] rvfi_bus_addr output [NBUS * BUSLEN/8 - 1 : 0] rvfi_bus_rmask output [NBUS * BUSLEN/8 - 1 : 0] rvfi_bus_wmask output [NBUS * BUSLEN - 1 : 0] rvfi_bus_rdata output [NBUS * BUSLEN - 1 : 0] rvfi_bus_wdata
RVFI_BUS では、 NBUSを使って 拡張は複数のバスを監視することができる。これは、命令バストデータバスの分離も含まれている。観測対象のバスの幅は BUSLEN を使って指定される。
rvfi_bus_valid(1-bit) : 観測可能なメモリアクセスが存在するとみなされる。rvfi_bus_insn/rvfi_bus_data(1-bit): アクセスが命令フェッチかデータアクセスかを示すために使用される。- これらを区別しないコアやバスの場合、両方を設定する必要がある。
rvfi_bus_addr(XLEN-bit): アクセスのアドレスrvfi_bus_rmask/rvfi_bus_wmask(BUSLEN/8-bit):rvfi_bus_addrから始まるどのバイトがアクセスされるかを示す。rvfi_bus_rdata/rvfi_bus_wdata(BUSLEN-bit): 読み出しデータおよび書き込みデータである。
RVFI_BUS を使用して観測されるすべてのアクセスはインオーダであると仮定される。これには、RVFI_BUS チャネルインデックスの昇順で順序付けられる同一サイクル内のアクセスも含まれる。これは将来の拡張によって緩和される可能性がある。
標準インターフェース用 RVFI_BUS オブザーバ
busディレクトリには、標準インターフェース用の RVFI_BUS オブザーバの実装が含まれている。
例えば、AXI4オブザーバはbus/rvfi_bus_axi4.svに用意されている。このファイルには、AXI4をRVFI_BUS信号に変換する際のタイミングに関する注記も含まれている。
