colin
/
picorv32
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add RVFI to AXI and WB wrappers modules, Add RVFI monitor support to test bench

This commit is contained in:
Clifford Wolf 2017-05-27 19:58:44 +02:00
parent bb9ebeb9e3
commit f295b900bc
3 changed files with 146 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile
View File

@ -47,15 +47,15 @@ test_synth: testbench_synth.vvp firmware/firmware.hex
vvp -N $< vvp -N $<
testbench.vvp: testbench.v picorv32.v 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 $@ chmod -x $@
testbench_wb.vvp: testbench_wb.v picorv32.v 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 $@ chmod -x $@
testbench_sp.vvp: testbench.v picorv32.v 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 $@ chmod -x $@
testbench_synth.vvp: testbench.v synth.v testbench_synth.vvp: testbench.v synth.v

80
picorv32.v
View File

@ -2386,6 +2386,26 @@ module picorv32_axi #(
input [31:0] irq, input [31:0] irq,
output [31:0] eoi, 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 // Trace Interface
output trace_valid, output trace_valid,
output [35:0] trace_data output [35:0] trace_data
@ -2478,6 +2498,26 @@ module picorv32_axi #(
.irq(irq), .irq(irq),
.eoi(eoi), .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_valid(trace_valid),
.trace_data (trace_data) .trace_data (trace_data)
); );
@ -2628,6 +2668,26 @@ module picorv32_wb #(
input [31:0] irq, input [31:0] irq,
output [31:0] eoi, 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 // Trace Interface
output trace_valid, output trace_valid,
output [35:0] trace_data, output [35:0] trace_data,
@ -2698,6 +2758,26 @@ module picorv32_wb #(
.irq(irq), .irq(irq),
.eoi(eoi), .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_valid(trace_valid),
.trace_data (trace_data) .trace_data (trace_data)
); );

63
testbench.v
View File

@ -135,6 +135,26 @@ module picorv32_wrapper #(
.tests_passed (tests_passed ) .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 #( picorv32_axi #(
`ifndef SYNTH_TEST `ifndef SYNTH_TEST
`ifdef SP_TEST `ifdef SP_TEST
@ -170,10 +190,53 @@ module picorv32_wrapper #(
.mem_axi_rready (mem_axi_rready ), .mem_axi_rready (mem_axi_rready ),
.mem_axi_rdata (mem_axi_rdata ), .mem_axi_rdata (mem_axi_rdata ),
.irq (irq ), .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_valid (trace_valid ),
.trace_data (trace_data ) .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; reg [1023:0] firmware_file;
initial begin initial begin
if (!$value$plusargs("firmware=%s", firmware_file)) if (!$value$plusargs("firmware=%s", firmware_file))