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

Remove RISCV_FORMAL.

This commit is contained in:
colin.liang 2023-01-09 13:26:32 +08:00
parent 3bda5c9e63
commit c676992a07
4 changed files with 6 additions and 439 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -35,3 +35,4 @@
/synth.log
/synth.v
.*.swp
.vscode

9
Makefile
View File

@ -27,9 +27,6 @@ test: testbench.vvp firmware/firmware.hex
test_vcd: testbench.vvp firmware/firmware.hex
$(VVP) -N $< +vcd +trace +noerror
test_rvf: testbench_rvf.vvp firmware/firmware.hex
$(VVP) -N $< +vcd +trace +noerror
test_wb: testbench_wb.vvp firmware/firmware.hex
$(VVP) -N $<
@ -58,10 +55,6 @@ testbench.vvp: testbench.v picorv32.v
$(IVERILOG) -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
chmod -x $@
testbench_rvf.vvp: testbench.v picorv32.v rvfimon.v
$(IVERILOG) -o $@ -D RISCV_FORMAL $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
chmod -x $@
testbench_wb.vvp: testbench_wb.v picorv32.v
$(IVERILOG) -o $@ $(subst C,-DCOMPRESSED_ISA,$(COMPRESSED_ISA)) $^
chmod -x $@
@ -178,7 +171,7 @@ clean:
rm -vrf $(FIRMWARE_OBJS) $(TEST_OBJS) check.smt2 check.vcd synth.v synth.log \
firmware/firmware.elf firmware/firmware.bin firmware/firmware.hex firmware/firmware.map \
testbench.vvp testbench_sp.vvp testbench_synth.vvp testbench_ez.vvp \
testbench_rvf.vvp testbench_wb.vvp testbench.vcd testbench.trace \
testbench_wb.vvp testbench.vcd testbench.trace \
testbench_verilator testbench_verilator_dir
.PHONY: test test_vcd test_sp test_axi test_wb test_wb_vcd test_ez test_ez_vcd test_synth download-tools build-tools toc clean

366
picorv32.v
View File

@ -35,17 +35,8 @@
`define debug(debug_command)
`endif
`ifdef FORMAL
`define FORMAL_KEEP (* keep *)
`define assert(assert_expr) assert(assert_expr)
`else
`ifdef DEBUGNETS
`define FORMAL_KEEP (* keep *)
`else
`define FORMAL_KEEP
`endif
`define assert(assert_expr) empty_statement
`endif
`define assert(assert_expr) empty_statement
`define FORMAL_KEEP
// uncomment this for register file in extra module
// `define PICORV32_REGS picorv32_regs
@ -120,40 +111,6 @@ module picorv32 #(
input [31:0] irq,
output reg [31:0] eoi,
`ifdef RISCV_FORMAL
output reg rvfi_valid,
output reg [63:0] rvfi_order,
output reg [31:0] rvfi_insn,
output reg rvfi_trap,
output reg rvfi_halt,
output reg rvfi_intr,
output reg [ 1:0] rvfi_mode,
output reg [ 1:0] rvfi_ixl,
output reg [ 4:0] rvfi_rs1_addr,
output reg [ 4:0] rvfi_rs2_addr,
output reg [31:0] rvfi_rs1_rdata,
output reg [31:0] rvfi_rs2_rdata,
output reg [ 4:0] rvfi_rd_addr,
output reg [31:0] rvfi_rd_wdata,
output reg [31:0] rvfi_pc_rdata,
output reg [31:0] rvfi_pc_wdata,
output reg [31:0] rvfi_mem_addr,
output reg [ 3:0] rvfi_mem_rmask,
output reg [ 3:0] rvfi_mem_wmask,
output reg [31:0] rvfi_mem_rdata,
output reg [31:0] rvfi_mem_wdata,
output reg [63:0] rvfi_csr_mcycle_rmask,
output reg [63:0] rvfi_csr_mcycle_wmask,
output reg [63:0] rvfi_csr_mcycle_rdata,
output reg [63:0] rvfi_csr_mcycle_wdata,
output reg [63:0] rvfi_csr_minstret_rmask,
output reg [63:0] rvfi_csr_minstret_wmask,
output reg [63:0] rvfi_csr_minstret_rdata,
output reg [63:0] rvfi_csr_minstret_wdata,
`endif
// Trace Interface
output reg trace_valid,
output reg [35:0] trace_data
@ -217,41 +174,6 @@ module picorv32 #(
begin end
endtask
`ifdef DEBUGREGS
wire [31:0] dbg_reg_x0 = 0;
wire [31:0] dbg_reg_x1 = cpuregs[1];
wire [31:0] dbg_reg_x2 = cpuregs[2];
wire [31:0] dbg_reg_x3 = cpuregs[3];
wire [31:0] dbg_reg_x4 = cpuregs[4];
wire [31:0] dbg_reg_x5 = cpuregs[5];
wire [31:0] dbg_reg_x6 = cpuregs[6];
wire [31:0] dbg_reg_x7 = cpuregs[7];
wire [31:0] dbg_reg_x8 = cpuregs[8];
wire [31:0] dbg_reg_x9 = cpuregs[9];
wire [31:0] dbg_reg_x10 = cpuregs[10];
wire [31:0] dbg_reg_x11 = cpuregs[11];
wire [31:0] dbg_reg_x12 = cpuregs[12];
wire [31:0] dbg_reg_x13 = cpuregs[13];
wire [31:0] dbg_reg_x14 = cpuregs[14];
wire [31:0] dbg_reg_x15 = cpuregs[15];
wire [31:0] dbg_reg_x16 = cpuregs[16];
wire [31:0] dbg_reg_x17 = cpuregs[17];
wire [31:0] dbg_reg_x18 = cpuregs[18];
wire [31:0] dbg_reg_x19 = cpuregs[19];
wire [31:0] dbg_reg_x20 = cpuregs[20];
wire [31:0] dbg_reg_x21 = cpuregs[21];
wire [31:0] dbg_reg_x22 = cpuregs[22];
wire [31:0] dbg_reg_x23 = cpuregs[23];
wire [31:0] dbg_reg_x24 = cpuregs[24];
wire [31:0] dbg_reg_x25 = cpuregs[25];
wire [31:0] dbg_reg_x26 = cpuregs[26];
wire [31:0] dbg_reg_x27 = cpuregs[27];
wire [31:0] dbg_reg_x28 = cpuregs[28];
wire [31:0] dbg_reg_x29 = cpuregs[29];
wire [31:0] dbg_reg_x30 = cpuregs[30];
wire [31:0] dbg_reg_x31 = cpuregs[31];
`endif
// Internal PCPI Cores
wire pcpi_mul_wr;
@ -687,6 +609,7 @@ module picorv32 #(
assign is_rdcycle_rdcycleh_rdinstr_rdinstrh = |{instr_rdcycle, instr_rdcycleh, instr_rdinstr, instr_rdinstrh};
reg [63:0] new_ascii_instr;
`FORMAL_KEEP reg [63:0] dbg_ascii_instr;
`FORMAL_KEEP reg [31:0] dbg_insn_imm;
`FORMAL_KEEP reg [4:0] dbg_insn_rs1;
@ -696,6 +619,7 @@ module picorv32 #(
`FORMAL_KEEP reg [31:0] dbg_rs2val;
`FORMAL_KEEP reg dbg_rs1val_valid;
`FORMAL_KEEP reg dbg_rs2val_valid;
`FORMAL_KEEP reg [127:0] dbg_ascii_state;
always @* begin
new_ascii_instr = "";
@ -1176,8 +1100,6 @@ module picorv32 #(
reg [7:0] cpu_state;
reg [1:0] irq_state;
`FORMAL_KEEP reg [127:0] dbg_ascii_state;
always @* begin
dbg_ascii_state = "";
if (cpu_state == cpu_state_trap) dbg_ascii_state = "trap";
@ -1968,197 +1890,6 @@ module picorv32 #(
end
current_pc = 'bx;
end
`ifdef RISCV_FORMAL
reg dbg_irq_call;
reg dbg_irq_enter;
reg [31:0] dbg_irq_ret;
always @(posedge clk) begin
rvfi_valid <= resetn && (launch_next_insn || trap) && dbg_valid_insn;
rvfi_order <= resetn ? rvfi_order + rvfi_valid : 0;
rvfi_insn <= dbg_insn_opcode;
rvfi_rs1_addr <= dbg_rs1val_valid ? dbg_insn_rs1 : 0;
rvfi_rs2_addr <= dbg_rs2val_valid ? dbg_insn_rs2 : 0;
rvfi_pc_rdata <= dbg_insn_addr;
rvfi_rs1_rdata <= dbg_rs1val_valid ? dbg_rs1val : 0;
rvfi_rs2_rdata <= dbg_rs2val_valid ? dbg_rs2val : 0;
rvfi_trap <= trap;
rvfi_halt <= trap;
rvfi_intr <= dbg_irq_enter;
rvfi_mode <= 3;
rvfi_ixl <= 1;
if (!resetn) begin
dbg_irq_call <= 0;
dbg_irq_enter <= 0;
end else
if (rvfi_valid) begin
dbg_irq_call <= 0;
dbg_irq_enter <= dbg_irq_call;
end else
if (irq_state == 1) begin
dbg_irq_call <= 1;
dbg_irq_ret <= next_pc;
end
if (!resetn) begin
rvfi_rd_addr <= 0;
rvfi_rd_wdata <= 0;
end else
if (cpuregs_write && !irq_state) begin
`ifdef PICORV32_TESTBUG_003
rvfi_rd_addr <= latched_rd ^ 1;
`else
rvfi_rd_addr <= latched_rd;
`endif
`ifdef PICORV32_TESTBUG_004
rvfi_rd_wdata <= latched_rd ? cpuregs_wrdata ^ 1 : 0;
`else
rvfi_rd_wdata <= latched_rd ? cpuregs_wrdata : 0;
`endif
end else
if (rvfi_valid) begin
rvfi_rd_addr <= 0;
rvfi_rd_wdata <= 0;
end
casez (dbg_insn_opcode)
32'b 0000000_?????_000??_???_?????_0001011: begin // getq
rvfi_rs1_addr <= 0;
rvfi_rs1_rdata <= 0;
end
32'b 0000001_?????_?????_???_000??_0001011: begin // setq
rvfi_rd_addr <= 0;
rvfi_rd_wdata <= 0;
end
32'b 0000010_?????_00000_???_00000_0001011: begin // retirq
rvfi_rs1_addr <= 0;
rvfi_rs1_rdata <= 0;
end
endcase
if (!dbg_irq_call) begin
if (dbg_mem_instr) begin
rvfi_mem_addr <= 0;
rvfi_mem_rmask <= 0;
rvfi_mem_wmask <= 0;
rvfi_mem_rdata <= 0;
rvfi_mem_wdata <= 0;
end else
if (dbg_mem_valid && dbg_mem_ready) begin
rvfi_mem_addr <= dbg_mem_addr;
rvfi_mem_rmask <= dbg_mem_wstrb ? 0 : ~0;
rvfi_mem_wmask <= dbg_mem_wstrb;
rvfi_mem_rdata <= dbg_mem_rdata;
rvfi_mem_wdata <= dbg_mem_wdata;
end
end
end
always @* begin
`ifdef PICORV32_TESTBUG_005
rvfi_pc_wdata = (dbg_irq_call ? dbg_irq_ret : dbg_insn_addr) ^ 4;
`else
rvfi_pc_wdata = dbg_irq_call ? dbg_irq_ret : dbg_insn_addr;
`endif
rvfi_csr_mcycle_rmask = 0;
rvfi_csr_mcycle_wmask = 0;
rvfi_csr_mcycle_rdata = 0;
rvfi_csr_mcycle_wdata = 0;
rvfi_csr_minstret_rmask = 0;
rvfi_csr_minstret_wmask = 0;
rvfi_csr_minstret_rdata = 0;
rvfi_csr_minstret_wdata = 0;
if (rvfi_valid && rvfi_insn[6:0] == 7'b 1110011 && rvfi_insn[13:12] == 3'b010) begin
if (rvfi_insn[31:20] == 12'h C00) begin
rvfi_csr_mcycle_rmask = 64'h 0000_0000_FFFF_FFFF;
rvfi_csr_mcycle_rdata = {32'h 0000_0000, rvfi_rd_wdata};
end
if (rvfi_insn[31:20] == 12'h C80) begin
rvfi_csr_mcycle_rmask = 64'h FFFF_FFFF_0000_0000;
rvfi_csr_mcycle_rdata = {rvfi_rd_wdata, 32'h 0000_0000};
end
if (rvfi_insn[31:20] == 12'h C02) begin
rvfi_csr_minstret_rmask = 64'h 0000_0000_FFFF_FFFF;
rvfi_csr_minstret_rdata = {32'h 0000_0000, rvfi_rd_wdata};
end
if (rvfi_insn[31:20] == 12'h C82) begin
rvfi_csr_minstret_rmask = 64'h FFFF_FFFF_0000_0000;
rvfi_csr_minstret_rdata = {rvfi_rd_wdata, 32'h 0000_0000};
end
end
end
`endif
// Formal Verification
`ifdef FORMAL
reg [3:0] last_mem_nowait;
always @(posedge clk)
last_mem_nowait <= {last_mem_nowait, mem_ready || !mem_valid};
// stall the memory interface for max 4 cycles
restrict property (|last_mem_nowait || mem_ready || !mem_valid);
// resetn low in first cycle, after that resetn high
restrict property (resetn != $initstate);
// this just makes it much easier to read traces. uncomment as needed.
// assume property (mem_valid || !mem_ready);
reg ok;
always @* begin
if (resetn) begin
// instruction fetches are read-only
if (mem_valid && mem_instr)
assert (mem_wstrb == 0);
// cpu_state must be valid
ok = 0;
if (cpu_state == cpu_state_trap) ok = 1;
if (cpu_state == cpu_state_fetch) ok = 1;
if (cpu_state == cpu_state_ld_rs1) ok = 1;
if (cpu_state == cpu_state_ld_rs2) ok = !ENABLE_REGS_DUALPORT;
if (cpu_state == cpu_state_exec) ok = 1;
if (cpu_state == cpu_state_shift) ok = 1;
if (cpu_state == cpu_state_stmem) ok = 1;
if (cpu_state == cpu_state_ldmem) ok = 1;
assert (ok);
end
end
reg last_mem_la_read = 0;
reg last_mem_la_write = 0;
reg [31:0] last_mem_la_addr;
reg [31:0] last_mem_la_wdata;
reg [3:0] last_mem_la_wstrb = 0;
always @(posedge clk) begin
last_mem_la_read <= mem_la_read;
last_mem_la_write <= mem_la_write;
last_mem_la_addr <= mem_la_addr;
last_mem_la_wdata <= mem_la_wdata;
last_mem_la_wstrb <= mem_la_wstrb;
if (last_mem_la_read) begin
assert(mem_valid);
assert(mem_addr == last_mem_la_addr);
assert(mem_wstrb == 0);
end
if (last_mem_la_write) begin
assert(mem_valid);
assert(mem_addr == last_mem_la_addr);
assert(mem_wdata == last_mem_la_wdata);
assert(mem_wstrb == last_mem_la_wstrb);
end
if (mem_la_read || mem_la_write) begin
assert(!mem_valid || mem_ready);
end
end
`endif
endmodule
// This is a simple example implementation of PICORV32_REGS.
@ -2577,28 +2308,6 @@ module picorv32_axi #(
input [31:0] irq,
output [31:0] eoi,
`ifdef RISCV_FORMAL
output rvfi_valid,
output [63:0] rvfi_order,
output [31:0] rvfi_insn,
output rvfi_trap,
output rvfi_halt,
output rvfi_intr,
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
@ -2690,29 +2399,6 @@ 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_halt (rvfi_halt ),
.rvfi_intr (rvfi_intr ),
.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)
);
@ -2863,28 +2549,6 @@ module picorv32_wb #(
input [31:0] irq,
output [31:0] eoi,
`ifdef RISCV_FORMAL
output rvfi_valid,
output [63:0] rvfi_order,
output [31:0] rvfi_insn,
output rvfi_trap,
output rvfi_halt,
output rvfi_intr,
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,
@ -2955,28 +2619,6 @@ 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_halt (rvfi_halt ),
.rvfi_intr (rvfi_intr ),
.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)
);

69
testbench.v
View File

@ -138,28 +138,6 @@ module picorv32_wrapper #(
.tests_passed (tests_passed )
);
`ifdef RISCV_FORMAL
wire rvfi_valid;
wire [63:0] rvfi_order;
wire [31:0] rvfi_insn;
wire rvfi_trap;
wire rvfi_halt;
wire rvfi_intr;
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
@ -195,57 +173,10 @@ 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_halt (rvfi_halt ),
.rvfi_intr (rvfi_intr ),
.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
picorv32_rvfimon rvfi_monitor (
.clock (clk ),
.reset (!resetn ),
.rvfi_valid (rvfi_valid ),
.rvfi_order (rvfi_order ),
.rvfi_insn (rvfi_insn ),
.rvfi_trap (rvfi_trap ),
.rvfi_halt (rvfi_halt ),
.rvfi_intr (rvfi_intr ),
.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))