From c676992a0742c9e61967a2b69e4880eb5e5c7647 Mon Sep 17 00:00:00 2001 From: "colin.liang" Date: Mon, 9 Jan 2023 13:26:32 +0800 Subject: [PATCH] Remove RISCV_FORMAL. --- .gitignore | 1 + Makefile | 9 +- picorv32.v | 366 +--------------------------------------------------- testbench.v | 69 ---------- 4 files changed, 6 insertions(+), 439 deletions(-) diff --git a/.gitignore b/.gitignore index 487adcc..b80458f 100644 --- a/.gitignore +++ b/.gitignore @@ -35,3 +35,4 @@ /synth.log /synth.v .*.swp +.vscode diff --git a/Makefile b/Makefile index d28b598..f9d7594 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/picorv32.v b/picorv32.v index cfc7ce0..90640ac 100644 --- a/picorv32.v +++ b/picorv32.v @@ -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) ); diff --git a/testbench.v b/testbench.v index 9d8e249..04c1946 100644 --- a/testbench.v +++ b/testbench.v @@ -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))