diff --git a/src/main/verilog/picorv32.v b/src/main/resources/picorv32.v similarity index 90% rename from src/main/verilog/picorv32.v rename to src/main/resources/picorv32.v index cc45fa9..70c0a63 100644 --- a/src/main/verilog/picorv32.v +++ b/src/main/resources/picorv32.v @@ -35,17 +35,14 @@ `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 + // uncomment this for register file in extra module // `define PICORV32_REGS picorv32_regs @@ -120,39 +117,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, @@ -1283,10 +1247,6 @@ module picorv32 #( alu_out = alu_shr; endcase -`ifdef RISCV_FORMAL_BLACKBOX_ALU - alu_out_0 = $anyseq; - alu_out = $anyseq; -`endif end reg clear_prefetched_high_word_q; @@ -1348,20 +1308,11 @@ module picorv32 #( always @* begin decoded_rs = 'bx; if (ENABLE_REGS_DUALPORT) begin -`ifndef RISCV_FORMAL_BLACKBOX_REGS cpuregs_rs1 = decoded_rs1 ? cpuregs[decoded_rs1] : 0; cpuregs_rs2 = decoded_rs2 ? cpuregs[decoded_rs2] : 0; -`else - cpuregs_rs1 = decoded_rs1 ? $anyseq : 0; - cpuregs_rs2 = decoded_rs2 ? $anyseq : 0; -`endif end else begin decoded_rs = (cpu_state == cpu_state_ld_rs2) ? decoded_rs2 : decoded_rs1; -`ifndef RISCV_FORMAL_BLACKBOX_REGS cpuregs_rs1 = decoded_rs ? cpuregs[decoded_rs] : 0; -`else - cpuregs_rs1 = decoded_rs ? $anyseq : 0; -`endif cpuregs_rs2 = cpuregs_rs1; end end @@ -1974,196 +1925,6 @@ module picorv32 #( 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. @@ -2582,28 +2343,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 @@ -2696,28 +2435,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) ); @@ -2868,28 +2585,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, @@ -2960,27 +2655,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/src/main/scala/backBoard/pico/picorv32.scala b/src/main/scala/backBoard/pico/picorv32.scala index f658bbb..67a6ab6 100644 --- a/src/main/scala/backBoard/pico/picorv32.scala +++ b/src/main/scala/backBoard/pico/picorv32.scala @@ -2,5 +2,101 @@ package BACK import chisel3._ import chisel3.util._ +import chisel3.experimental._ + + +class Picorv32 extends BlackBox() with HasBlackBoxResource { + val io = IO(new Bundle { + val clk = Input(Bool()) + val resetn = Input(Bool()) + val trap = Output(Bool()) + + val mem_valid = Output(Bool()) + val mem_instr = Output(Bool()) + val mem_ready = Input(Bool()) + + val mem_addr = Output(UInt(32.W)) + val mem_wdata = Output(UInt(32.W)) + val mem_wstrb = Output(UInt(4.W)) + val mem_rdata = Input(UInt(32.W)) + + // Look-Ahead Interface + val mem_la_read = Output(Bool()) + val mem_la_write = Output(Bool()) + val mem_la_addr = Output(UInt(32.W)) + val mem_la_wdata = Output(UInt(32.W)) + val mem_la_wstrb = Output(UInt(4.W)) + + // Pico Co-Processor Interface (PCPI) + val pcpi_valid = Output(Bool()) + val pcpi_insn = Output(UInt(32.W)) + val pcpi_rs1 = Output(UInt(32.W)) + val pcpi_rs2 = Output(UInt(32.W)) + val pcpi_wr = Input(Bool()) + val pcpi_rd = Input(UInt(32.W)) + val pcpi_wait = Input(Bool()) + val pcpi_ready = Input(Bool()) + + // IRQ Interface + val irq = Input(UInt(32.W)) + val eoi = Output(UInt(32.W)) + + // Trace Interface + val trace_valid = Output(Bool()) + val trace_data = Output(UInt(36.W)) + }) + addResource("./picorv32.v") +} + +class picorv32_tl extends Module{ + val io = IO(new Bundle { + + val trap = Output(Bool()) + + val mem_valid = Output(Bool()) + val mem_instr = Output(Bool()) + val mem_ready = Input(Bool()) + + val mem_addr = Output(UInt(32.W)) + val mem_wdata = Output(UInt(32.W)) + val mem_wstrb = Output(UInt(4.W)) + val mem_rdata = Input(UInt(32.W)) + + + // IRQ Interface + val irq = Input(UInt(32.W)) + val eoi = Output(UInt(32.W)) + + }) + + + val core = Module(new Picorv32) + + core.io.clk := clock.asBool + core.io.resetn := ~reset.asBool + io.trap := core.io.trap + + io.mem_valid := core.io.mem_valid + io.mem_instr := core.io.mem_instr + core.io.mem_ready := io.mem_ready + + io.mem_addr := core.io.mem_addr + io.mem_wdata:= core.io.mem_wdata + io.mem_wstrb:= core.io.mem_wstrb + core.io.mem_rdata := io.mem_rdata + + + + // Pico Co-Processor Interface (PCPI) + core.io.pcpi_wr := false.B + core.io.pcpi_rd := 0.U + core.io.pcpi_wait := false.B + core.io.pcpi_ready := true.B + + // IRQ Interface + core.io.irq := io.irq + io.eoi := core.io.eoi + +}