From f295b900bcb7e67eb2f767defa5aba6a9effce4c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 27 May 2017 19:58:44 +0200 Subject: [PATCH] Add RVFI to AXI and WB wrappers modules, Add RVFI monitor support to test bench --- Makefile | 6 ++-- picorv32.v | 80 +++++++++++++++++++++++++++++++++++++++++++++++++++++ testbench.v | 63 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 146 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 1655bdf..00f4cc7 100644 --- a/Makefile +++ b/Makefile @@ -47,15 +47,15 @@ test_synth: testbench_synth.vvp firmware/firmware.hex vvp -N $< testbench.vvp: testbench.v picorv32.v - iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DRISCV_FORMAL $^ + iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^ chmod -x $@ testbench_wb.vvp: testbench_wb.v picorv32.v - iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DRISCV_FORMAL $^ + iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^ chmod -x $@ testbench_sp.vvp: testbench.v picorv32.v - iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DRISCV_FORMAL -DSP_TEST $^ + iverilog -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) -DSP_TEST $^ chmod -x $@ testbench_synth.vvp: testbench.v synth.v diff --git a/picorv32.v b/picorv32.v index 8c7b5b8..a1eebbd 100644 --- a/picorv32.v +++ b/picorv32.v @@ -2386,6 +2386,26 @@ module picorv32_axi #( input [31:0] irq, output [31:0] eoi, +`ifdef RISCV_FORMAL + output rvfi_valid, + output [ 7:0] rvfi_order, + output [31:0] rvfi_insn, + output rvfi_trap, + output [ 4:0] rvfi_rs1_addr, + output [ 4:0] rvfi_rs2_addr, + output [31:0] rvfi_rs1_rdata, + output [31:0] rvfi_rs2_rdata, + output [ 4:0] rvfi_rd_addr, + output [31:0] rvfi_rd_wdata, + output [31:0] rvfi_pc_rdata, + output [31:0] rvfi_pc_wdata, + output [31:0] rvfi_mem_addr, + output [ 3:0] rvfi_mem_rmask, + output [ 3:0] rvfi_mem_wmask, + output [31:0] rvfi_mem_rdata, + output [31:0] rvfi_mem_wdata, +`endif + // Trace Interface output trace_valid, output [35:0] trace_data @@ -2478,6 +2498,26 @@ module picorv32_axi #( .irq(irq), .eoi(eoi), +`ifdef RISCV_FORMAL + .rvfi_valid (rvfi_valid ), + .rvfi_order (rvfi_order ), + .rvfi_insn (rvfi_insn ), + .rvfi_trap (rvfi_trap ), + .rvfi_rs1_addr (rvfi_rs1_addr ), + .rvfi_rs2_addr (rvfi_rs2_addr ), + .rvfi_rs1_rdata(rvfi_rs1_rdata), + .rvfi_rs2_rdata(rvfi_rs2_rdata), + .rvfi_rd_addr (rvfi_rd_addr ), + .rvfi_rd_wdata (rvfi_rd_wdata ), + .rvfi_pc_rdata (rvfi_pc_rdata ), + .rvfi_pc_wdata (rvfi_pc_wdata ), + .rvfi_mem_addr (rvfi_mem_addr ), + .rvfi_mem_rmask(rvfi_mem_rmask), + .rvfi_mem_wmask(rvfi_mem_wmask), + .rvfi_mem_rdata(rvfi_mem_rdata), + .rvfi_mem_wdata(rvfi_mem_wdata), +`endif + .trace_valid(trace_valid), .trace_data (trace_data) ); @@ -2628,6 +2668,26 @@ module picorv32_wb #( input [31:0] irq, output [31:0] eoi, +`ifdef RISCV_FORMAL + output rvfi_valid, + output [ 7:0] rvfi_order, + output [31:0] rvfi_insn, + output rvfi_trap, + output [ 4:0] rvfi_rs1_addr, + output [ 4:0] rvfi_rs2_addr, + output [31:0] rvfi_rs1_rdata, + output [31:0] rvfi_rs2_rdata, + output [ 4:0] rvfi_rd_addr, + output [31:0] rvfi_rd_wdata, + output [31:0] rvfi_pc_rdata, + output [31:0] rvfi_pc_wdata, + output [31:0] rvfi_mem_addr, + output [ 3:0] rvfi_mem_rmask, + output [ 3:0] rvfi_mem_wmask, + output [31:0] rvfi_mem_rdata, + output [31:0] rvfi_mem_wdata, +`endif + // Trace Interface output trace_valid, output [35:0] trace_data, @@ -2698,6 +2758,26 @@ module picorv32_wb #( .irq(irq), .eoi(eoi), +`ifdef RISCV_FORMAL + .rvfi_valid (rvfi_valid ), + .rvfi_order (rvfi_order ), + .rvfi_insn (rvfi_insn ), + .rvfi_trap (rvfi_trap ), + .rvfi_rs1_addr (rvfi_rs1_addr ), + .rvfi_rs2_addr (rvfi_rs2_addr ), + .rvfi_rs1_rdata(rvfi_rs1_rdata), + .rvfi_rs2_rdata(rvfi_rs2_rdata), + .rvfi_rd_addr (rvfi_rd_addr ), + .rvfi_rd_wdata (rvfi_rd_wdata ), + .rvfi_pc_rdata (rvfi_pc_rdata ), + .rvfi_pc_wdata (rvfi_pc_wdata ), + .rvfi_mem_addr (rvfi_mem_addr ), + .rvfi_mem_rmask(rvfi_mem_rmask), + .rvfi_mem_wmask(rvfi_mem_wmask), + .rvfi_mem_rdata(rvfi_mem_rdata), + .rvfi_mem_wdata(rvfi_mem_wdata), +`endif + .trace_valid(trace_valid), .trace_data (trace_data) ); diff --git a/testbench.v b/testbench.v index 9380445..1eb2e01 100644 --- a/testbench.v +++ b/testbench.v @@ -135,6 +135,26 @@ module picorv32_wrapper #( .tests_passed (tests_passed ) ); +`ifdef RISCV_FORMAL + wire rvfi_valid; + wire [7:0] rvfi_order; + wire [31:0] rvfi_insn; + wire rvfi_trap; + wire [4:0] rvfi_rs1_addr; + wire [4:0] rvfi_rs2_addr; + wire [31:0] rvfi_rs1_rdata; + wire [31:0] rvfi_rs2_rdata; + wire [4:0] rvfi_rd_addr; + wire [31:0] rvfi_rd_wdata; + wire [31:0] rvfi_pc_rdata; + wire [31:0] rvfi_pc_wdata; + wire [31:0] rvfi_mem_addr; + wire [3:0] rvfi_mem_rmask; + wire [3:0] rvfi_mem_wmask; + wire [31:0] rvfi_mem_rdata; + wire [31:0] rvfi_mem_wdata; +`endif + picorv32_axi #( `ifndef SYNTH_TEST `ifdef SP_TEST @@ -170,10 +190,53 @@ module picorv32_wrapper #( .mem_axi_rready (mem_axi_rready ), .mem_axi_rdata (mem_axi_rdata ), .irq (irq ), +`ifdef RISCV_FORMAL + .rvfi_valid (rvfi_valid ), + .rvfi_order (rvfi_order ), + .rvfi_insn (rvfi_insn ), + .rvfi_trap (rvfi_trap ), + .rvfi_rs1_addr (rvfi_rs1_addr ), + .rvfi_rs2_addr (rvfi_rs2_addr ), + .rvfi_rs1_rdata (rvfi_rs1_rdata ), + .rvfi_rs2_rdata (rvfi_rs2_rdata ), + .rvfi_rd_addr (rvfi_rd_addr ), + .rvfi_rd_wdata (rvfi_rd_wdata ), + .rvfi_pc_rdata (rvfi_pc_rdata ), + .rvfi_pc_wdata (rvfi_pc_wdata ), + .rvfi_mem_addr (rvfi_mem_addr ), + .rvfi_mem_rmask (rvfi_mem_rmask ), + .rvfi_mem_wmask (rvfi_mem_wmask ), + .rvfi_mem_rdata (rvfi_mem_rdata ), + .rvfi_mem_wdata (rvfi_mem_wdata ), +`endif .trace_valid (trace_valid ), .trace_data (trace_data ) ); +`ifdef RISCV_FORMAL + riscv_formal_monitor_rv32ic rvfi_monitor ( + .clock (clk ), + .reset (!resetn ), + .rvfi_valid (rvfi_valid ), + .rvfi_order (rvfi_order ), + .rvfi_insn (rvfi_insn ), + .rvfi_trap (rvfi_trap ), + .rvfi_rs1_addr (rvfi_rs1_addr ), + .rvfi_rs2_addr (rvfi_rs2_addr ), + .rvfi_rs1_rdata(rvfi_rs1_rdata), + .rvfi_rs2_rdata(rvfi_rs2_rdata), + .rvfi_rd_addr (rvfi_rd_addr ), + .rvfi_rd_wdata (rvfi_rd_wdata ), + .rvfi_pc_rdata (rvfi_pc_rdata ), + .rvfi_pc_wdata (rvfi_pc_wdata ), + .rvfi_mem_addr (rvfi_mem_addr ), + .rvfi_mem_rmask(rvfi_mem_rmask), + .rvfi_mem_wmask(rvfi_mem_wmask), + .rvfi_mem_rdata(rvfi_mem_rdata), + .rvfi_mem_wdata(rvfi_mem_wdata) + ); +`endif + reg [1023:0] firmware_file; initial begin if (!$value$plusargs("firmware=%s", firmware_file))