VexRiscv におけるriscv-formal の実行方法を調査している。
前回の続き：msyksphinz.hatenablog.com
例えば、 rvfi_insn_addi は以下のようにインスタンス化されている。それぞれのフォーマルの項目に対してインスタンスが作られているようだ。
insns/isa_rv64imc.v
wire spec_insn_addi_valid; wire spec_insn_addi_trap; wire [ 4 : 0] spec_insn_addi_rs1_addr; wire [ 4 : 0] spec_insn_addi_rs2_addr; wire [ 4 : 0] spec_insn_addi_rd_addr; wire [`RISCV_FORMAL_XLEN - 1 : 0] spec_insn_addi_rd_wdata; wire [`RISCV_FORMAL_XLEN - 1 : 0] spec_insn_addi_pc_wdata; wire [`RISCV_FORMAL_XLEN - 1 : 0] spec_insn_addi_mem_addr; wire [`RISCV_FORMAL_XLEN/8 - 1 : 0] spec_insn_addi_mem_rmask; wire [`RISCV_FORMAL_XLEN/8 - 1 : 0] spec_insn_addi_mem_wmask; wire [`RISCV_FORMAL_XLEN - 1 : 0] spec_insn_addi_mem_wdata; `ifdef RISCV_FORMAL_CSR_MISA wire [`RISCV_FORMAL_XLEN - 1 : 0] spec_insn_addi_csr_misa_rmask; `endif rvfi_insn_addi insn_addi ( .rvfi_valid(rvfi_valid), .rvfi_insn(rvfi_insn), .rvfi_pc_rdata(rvfi_pc_rdata), .rvfi_rs1_rdata(rvfi_rs1_rdata), .rvfi_rs2_rdata(rvfi_rs2_rdata), .rvfi_mem_rdata(rvfi_mem_rdata), `ifdef RISCV_FORMAL_CSR_MISA .rvfi_csr_misa_rdata(rvfi_csr_misa_rdata), .spec_csr_misa_rmask(spec_insn_addi_csr_misa_rmask), `endif .spec_valid(spec_insn_addi_valid), .spec_trap(spec_insn_addi_trap), .spec_rs1_addr(spec_insn_addi_rs1_addr), .spec_rs2_addr(spec_insn_addi_rs2_addr), .spec_rd_addr(spec_insn_addi_rd_addr), .spec_rd_wdata(spec_insn_addi_rd_wdata), .spec_pc_wdata(spec_insn_addi_pc_wdata), .spec_mem_addr(spec_insn_addi_mem_addr), .spec_mem_rmask(spec_insn_addi_mem_rmask), .spec_mem_wmask(spec_insn_addi_mem_wmask), .spec_mem_wdata(spec_insn_addi_mem_wdata) );
そして実体がこれだ。これ自体は、信号を集約しているだけだ。VexRiscvからの rvfi_xxx の信号を読み取って spec_xxx に入れ直しているように見える。
module rvfi_insn_addi ( input rvfi_valid, input [`RISCV_FORMAL_ILEN - 1 : 0] rvfi_insn, input [`RISCV_FORMAL_XLEN - 1 : 0] rvfi_pc_rdata, input [`RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs1_rdata, input [`RISCV_FORMAL_XLEN - 1 : 0] rvfi_rs2_rdata, input [`RISCV_FORMAL_XLEN - 1 : 0] rvfi_mem_rdata, `ifdef RISCV_FORMAL_CSR_MISA input [`RISCV_FORMAL_XLEN - 1 : 0] rvfi_csr_misa_rdata, output [`RISCV_FORMAL_XLEN - 1 : 0] spec_csr_misa_rmask, `endif output spec_valid, output spec_trap, output [ 4 : 0] spec_rs1_addr, output [ 4 : 0] spec_rs2_addr, output [ 4 : 0] spec_rd_addr, output [`RISCV_FORMAL_XLEN - 1 : 0] spec_rd_wdata, output [`RISCV_FORMAL_XLEN - 1 : 0] spec_pc_wdata, output [`RISCV_FORMAL_XLEN - 1 : 0] spec_mem_addr, output [`RISCV_FORMAL_XLEN/8 - 1 : 0] spec_mem_rmask, output [`RISCV_FORMAL_XLEN/8 - 1 : 0] spec_mem_wmask, output [`RISCV_FORMAL_XLEN - 1 : 0] spec_mem_wdata ); // I-type instruction format wire [`RISCV_FORMAL_ILEN-1:0] insn_padding = rvfi_insn >> 16 >> 16; wire [`RISCV_FORMAL_XLEN-1:0] insn_imm = $signed(rvfi_insn[31:20]); wire [4:0] insn_rs1 = rvfi_insn[19:15]; wire [2:0] insn_funct3 = rvfi_insn[14:12]; wire [4:0] insn_rd = rvfi_insn[11: 7]; wire [6:0] insn_opcode = rvfi_insn[ 6: 0]; `ifdef RISCV_FORMAL_CSR_MISA wire misa_ok = (rvfi_csr_misa_rdata & `RISCV_FORMAL_XLEN'h 0) == `RISCV_FORMAL_XLEN'h 0; assign spec_csr_misa_rmask = `RISCV_FORMAL_XLEN'h 0; `else wire misa_ok = 1; `endif // ADDI instruction wire [`RISCV_FORMAL_XLEN-1:0] result = rvfi_rs1_rdata + insn_imm; assign spec_valid = rvfi_valid && !insn_padding && insn_funct3 == 3'b 000 && insn_opcode == 7'b 0010011; assign spec_rs1_addr = insn_rs1; assign spec_rd_addr = insn_rd; assign spec_rd_wdata = spec_rd_addr ? result : 0; assign spec_pc_wdata = rvfi_pc_rdata + 4; // default assignments assign spec_rs2_addr = 0; assign spec_trap = !misa_ok; assign spec_mem_addr = 0; assign spec_mem_rmask = 0; assign spec_mem_wmask = 0; assign spec_mem_wdata = 0; endmodule
これらの信号はこれらのモジュールの外で集約されていく：
assign spec_valid = spec_insn_add_valid ? spec_insn_add_valid : spec_insn_addi_valid ? spec_insn_addi_valid : spec_insn_addiw_valid ? spec_insn_addiw_valid : spec_insn_addw_valid ? spec_insn_addw_valid : spec_insn_and_valid ? spec_insn_and_valid : spec_insn_andi_valid ? spec_insn_andi_valid : spec_insn_auipc_valid ? spec_insn_auipc_valid : spec_insn_beq_valid ? spec_insn_beq_valid : spec_insn_bge_valid ? spec_insn_bge_valid : ... assign spec_trap = spec_insn_add_valid ? spec_insn_add_trap : spec_insn_addi_valid ? spec_insn_addi_trap : spec_insn_addiw_valid ? spec_insn_addiw_trap : spec_insn_addw_valid ? spec_insn_addw_trap : ...
これらのフォーマルは、個別の環境で実行されるのか。
insn_addi_ch0.sby
[options] mode bmc expect pass,fail append 0 depth 21 skip 20 [engines] smtbmc boolector [script] read -sv insn_addi_ch0.sv /home/kimura/work/formal/riscv-formal/cores/VexRiscv/../../cores/VexRiscv/wrapper.sv /home/kimura/work/formal/riscv-formal/cores/VexRiscv/../../cores/VexRiscv/VexRiscv.v prep -flatten -nordff -top rvfi_testbench chformal -early [files] /home/kimura/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_macros.vh /home/kimura/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_channel.sv /home/kimura/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_testbench.sv /home/kimura/work/formal/riscv-formal/cores/VexRiscv/../../checks/rvfi_insn_check.sv /home/kimura/work/formal/riscv-formal/cores/VexRiscv/../../insns/insn_addi.v [file defines.sv] `define RISCV_FORMAL `define RISCV_FORMAL_NRET 1 `define RISCV_FORMAL_XLEN 32 `define RISCV_FORMAL_ILEN 32 `define RISCV_FORMAL_RESET_CYCLES 1 `define RISCV_FORMAL_CHECK_CYCLE 20 `define RISCV_FORMAL_CHANNEL_IDX 0 `define RISCV_FORMAL_CHECKER rvfi_insn_check `define RISCV_FORMAL_INSN_MODEL rvfi_insn_addi `define RISCV_FORMAL_ALIGNED_MEM `define RISCV_FORMAL_ALTOPS `define DEBUGNETS `include "rvfi_macros.vh" [file insn_addi_ch0.sv] `include "defines.sv" `include "rvfi_channel.sv" `include "rvfi_testbench.sv" `include "rvfi_insn_check.sv" `include "insn_addi.v"
じゃあ実際の演算のモデルはどこにあるのか：このときの RISCV_FORMAL_INSN_MODEL は sby によって rvfi_insn_addi として定義されている。
checks/rvfi_insn_check.sv
`RISCV_FORMAL_INSN_MODEL insn_spec ( .rvfi_valid (valid ), .rvfi_insn (insn ), .rvfi_pc_rdata (pc_rdata ), .rvfi_rs1_rdata (rs1_rdata_or_zero ), .rvfi_rs2_rdata (rs2_rdata_or_zero ), .rvfi_mem_rdata (mem_rdata ), `ifdef RISCV_FORMAL_CSR_MISA .rvfi_csr_misa_rdata (csr_misa_rdata ), .spec_csr_misa_rmask (spec_csr_misa_rmask), `endif .spec_valid (spec_valid ), .spec_trap (spec_trap ), .spec_rs1_addr (spec_rs1_addr ), .spec_rs2_addr (spec_rs2_addr ), .spec_rd_addr (spec_rd_addr ), .spec_rd_wdata (spec_rd_wdata ), .spec_pc_wdata (spec_pc_wdata ), .spec_mem_addr (spec_mem_addr ), .spec_mem_rmask (spec_mem_rmask ), .spec_mem_wmask (spec_mem_wmask ), .spec_mem_wdata (spec_mem_wdata ) );
ハードウェアの結果は以下で取得する。
(* keep *) wire [`RISCV_FORMAL_XLEN - 1 : 0] rd_wdata = rvfi_rd_wdata [channel_idx*`RISCV_FORMAL_XLEN +: `RISCV_FORMAL_XLEN];
これをアサーションで比べている、という訳か。
if (!spec_trap) begin if (spec_rs1_addr != 0) assert(spec_rs1_addr == rs1_addr); if (spec_rs2_addr != 0) assert(spec_rs2_addr == rs2_addr); assert(spec_rd_addr == rd_addr); assert(spec_rd_wdata == rd_wdata); assert(`rvformal_addr_eq(spec_pc_wdata, pc_wdata));
