ruige/eb001
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

成功插入黑盒

Browse Source
This commit is contained in:
RuigeLee
2024-10-25 10:51:36 +08:00
parent 59961b5f31
commit d1ce60daaf
2 changed files with 98 additions and 328 deletions
Download Patch File Download Diff File Expand all files Collapse all files

330
src/main/verilog/picorv32.v → src/main/resources/picorv32.v
View File

@@ -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)

96
src/main/scala/backBoard/pico/picorv32.scala
View File

@@ -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
}