Fix a few things that were obviously wrong, and the first signs of a plausible RVFI bridge circuit
This commit is contained in:
parent
08e986912c
commit
dec78a728d
|
@ -72,8 +72,6 @@ module hazard3_core #(
|
||||||
//synthesis translate_on
|
//synthesis translate_on
|
||||||
`endif
|
`endif
|
||||||
|
|
||||||
wire flush_d_x;
|
|
||||||
|
|
||||||
wire d_stall;
|
wire d_stall;
|
||||||
wire x_stall;
|
wire x_stall;
|
||||||
wire m_stall;
|
wire m_stall;
|
||||||
|
@ -82,8 +80,6 @@ localparam HSIZE_WORD = 3'd2;
|
||||||
localparam HSIZE_HWORD = 3'd1;
|
localparam HSIZE_HWORD = 3'd1;
|
||||||
localparam HSIZE_BYTE = 3'd0;
|
localparam HSIZE_BYTE = 3'd0;
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// ----------------------------------------------------------------------------
|
// ----------------------------------------------------------------------------
|
||||||
// Pipe Stage F
|
// Pipe Stage F
|
||||||
|
|
||||||
|
@ -103,7 +99,7 @@ wire [1:0] fd_cir_vld;
|
||||||
wire [1:0] df_cir_use;
|
wire [1:0] df_cir_use;
|
||||||
wire df_cir_lock;
|
wire df_cir_lock;
|
||||||
|
|
||||||
assign bus_aph_panic_i = m_jump_req;
|
assign bus_aph_panic_i = 1'b0;
|
||||||
|
|
||||||
wire f_mem_size;
|
wire f_mem_size;
|
||||||
assign bus_hsize_i = f_mem_size ? HSIZE_WORD : HSIZE_HWORD;
|
assign bus_hsize_i = f_mem_size ? HSIZE_WORD : HSIZE_HWORD;
|
||||||
|
@ -137,8 +133,6 @@ hazard3_frontend #(
|
||||||
.next_regs_vld (f_regnum_vld)
|
.next_regs_vld (f_regnum_vld)
|
||||||
);
|
);
|
||||||
|
|
||||||
assign flush_d_x = m_jump_req && f_jump_rdy;
|
|
||||||
|
|
||||||
// ----------------------------------------------------------------------------
|
// ----------------------------------------------------------------------------
|
||||||
// Pipe Stage X (Decode Logic)
|
// Pipe Stage X (Decode Logic)
|
||||||
|
|
||||||
|
@ -198,7 +192,6 @@ hazard3_decode #(
|
||||||
|
|
||||||
.d_stall (d_stall),
|
.d_stall (d_stall),
|
||||||
.x_stall (x_stall),
|
.x_stall (x_stall),
|
||||||
.flush_d_x (flush_d_x),
|
|
||||||
.f_jump_rdy (f_jump_rdy),
|
.f_jump_rdy (f_jump_rdy),
|
||||||
.f_jump_now (f_jump_now),
|
.f_jump_now (f_jump_now),
|
||||||
.f_jump_target (f_jump_target),
|
.f_jump_target (f_jump_target),
|
||||||
|
@ -262,8 +255,11 @@ reg [W_MEMOP-1:0] xm_memop;
|
||||||
reg x_stall_raw;
|
reg x_stall_raw;
|
||||||
wire x_stall_muldiv;
|
wire x_stall_muldiv;
|
||||||
|
|
||||||
assign x_stall = m_stall ||
|
assign x_stall =
|
||||||
x_stall_raw || x_stall_muldiv || bus_aph_req_d && !bus_aph_ready_d;
|
m_stall ||
|
||||||
|
x_stall_raw || x_stall_muldiv ||
|
||||||
|
bus_aph_req_d && !bus_aph_ready_d ||
|
||||||
|
f_jump_req && !f_jump_rdy;
|
||||||
|
|
||||||
wire m_fast_mul_result_vld;
|
wire m_fast_mul_result_vld;
|
||||||
wire m_generating_result = xm_memop < MEMOP_SW || m_fast_mul_result_vld;
|
wire m_generating_result = xm_memop < MEMOP_SW || m_fast_mul_result_vld;
|
||||||
|
@ -310,10 +306,7 @@ always @ (*) begin
|
||||||
MEMOP_SH: bus_hsize_d = HSIZE_HWORD;
|
MEMOP_SH: bus_hsize_d = HSIZE_HWORD;
|
||||||
default: bus_hsize_d = HSIZE_BYTE;
|
default: bus_hsize_d = HSIZE_BYTE;
|
||||||
endcase
|
endcase
|
||||||
// m_jump_req implies flush_d_x is coming. Can't use flush_d_x because it's
|
bus_aph_req_d = x_memop_vld && !(x_stall_raw || x_trap_enter);
|
||||||
// possible for a mispredicted load/store to go through whilst a late jump
|
|
||||||
// request is stalled, if there are two bus masters.
|
|
||||||
bus_aph_req_d = x_memop_vld && !(x_stall_raw || m_jump_req || x_trap_enter);
|
|
||||||
end
|
end
|
||||||
|
|
||||||
// ALU operand muxes and bypass
|
// ALU operand muxes and bypass
|
||||||
|
@ -353,14 +346,12 @@ end
|
||||||
wire x_except_ecall = d_except == EXCEPT_ECALL;
|
wire x_except_ecall = d_except == EXCEPT_ECALL;
|
||||||
wire x_except_breakpoint = d_except == EXCEPT_EBREAK;
|
wire x_except_breakpoint = d_except == EXCEPT_EBREAK;
|
||||||
wire x_except_invalid_instr = d_except == EXCEPT_INSTR_ILLEGAL;
|
wire x_except_invalid_instr = d_except == EXCEPT_INSTR_ILLEGAL;
|
||||||
assign x_trap_exit = d_except == EXCEPT_MRET && !(x_stall || m_jump_req);
|
assign x_trap_exit = d_except == EXCEPT_MRET;
|
||||||
wire x_trap_enter_rdy = !(x_stall || m_jump_req || x_trap_exit);
|
wire x_trap_enter_rdy = !(x_stall || x_trap_exit);
|
||||||
wire x_trap_is_exception; // diagnostic
|
wire x_trap_is_exception; // diagnostic
|
||||||
|
|
||||||
`ifdef FORMAL
|
`ifdef FORMAL
|
||||||
always @ (posedge clk) begin
|
always @ (posedge clk) begin
|
||||||
if (flush_d_x)
|
|
||||||
assert(!x_trap_enter_rdy);
|
|
||||||
if (x_trap_exit)
|
if (x_trap_exit)
|
||||||
assert(!bus_aph_req_d);
|
assert(!bus_aph_req_d);
|
||||||
end
|
end
|
||||||
|
@ -383,11 +374,11 @@ hazard3_csr #(
|
||||||
.addr (d_imm[11:0]), // todo could just connect this to the instruction bits
|
.addr (d_imm[11:0]), // todo could just connect this to the instruction bits
|
||||||
.wdata (x_csr_wdata),
|
.wdata (x_csr_wdata),
|
||||||
.wen_soon (d_csr_wen),
|
.wen_soon (d_csr_wen),
|
||||||
.wen (d_csr_wen && !(x_stall || flush_d_x)),
|
.wen (d_csr_wen && !x_stall),
|
||||||
.wtype (d_csr_wtype),
|
.wtype (d_csr_wtype),
|
||||||
.rdata (x_csr_rdata),
|
.rdata (x_csr_rdata),
|
||||||
.ren_soon (d_csr_ren),
|
.ren_soon (d_csr_ren),
|
||||||
.ren (d_csr_ren && !(x_stall || flush_d_x)),
|
.ren (d_csr_ren && !x_stall),
|
||||||
// Trap signalling
|
// Trap signalling
|
||||||
.trap_addr (x_trap_addr),
|
.trap_addr (x_trap_addr),
|
||||||
.trap_enter_vld (x_trap_enter),
|
.trap_enter_vld (x_trap_enter),
|
||||||
|
@ -431,7 +422,7 @@ if (EXTENSION_M) begin: has_muldiv
|
||||||
else
|
else
|
||||||
x_muldiv_posted <= (x_muldiv_posted || (x_muldiv_op_vld && x_muldiv_op_rdy)) && x_stall;
|
x_muldiv_posted <= (x_muldiv_posted || (x_muldiv_op_vld && x_muldiv_op_rdy)) && x_stall;
|
||||||
|
|
||||||
wire x_muldiv_kill = flush_d_x || x_trap_enter; // TODO this takes an extra cycle to kill muldiv before trap entry
|
wire x_muldiv_kill = x_trap_enter; // TODO this takes an extra cycle to kill muldiv before trap entry
|
||||||
|
|
||||||
wire x_use_fast_mul = MUL_FAST && d_aluop == ALUOP_MULDIV && d_mulop == M_OP_MUL;
|
wire x_use_fast_mul = MUL_FAST && d_aluop == ALUOP_MULDIV && d_mulop == M_OP_MUL;
|
||||||
|
|
||||||
|
@ -468,7 +459,7 @@ if (EXTENSION_M) begin: has_muldiv
|
||||||
|
|
||||||
if (MUL_FAST) begin: has_fast_mul
|
if (MUL_FAST) begin: has_fast_mul
|
||||||
|
|
||||||
wire x_issue_fast_mul = x_use_fast_mul && |d_rd && !(x_stall || flush_d_x);
|
wire x_issue_fast_mul = x_use_fast_mul && |d_rd && !x_stall;
|
||||||
|
|
||||||
hazard3_mul_fast #(
|
hazard3_mul_fast #(
|
||||||
.XLEN(W_DATA)
|
.XLEN(W_DATA)
|
||||||
|
@ -511,13 +502,11 @@ always @ (posedge clk or negedge rst_n) begin
|
||||||
xm_memop <= MEMOP_NONE;
|
xm_memop <= MEMOP_NONE;
|
||||||
{xm_rs1, xm_rs2, xm_rd} <= {3 * W_REGADDR{1'b0}};
|
{xm_rs1, xm_rs2, xm_rd} <= {3 * W_REGADDR{1'b0}};
|
||||||
end else begin
|
end else begin
|
||||||
// TODO: this assertion may become untrue depending on how we handle exceptions/IRQs when stalled?
|
|
||||||
//`ASSERT(!(m_stall && flush_d_x));// bubble insertion logic below is broken otherwise
|
|
||||||
if (!m_stall) begin
|
if (!m_stall) begin
|
||||||
{xm_rs1, xm_rs2, xm_rd} <= {d_rs1, d_rs2, d_rd};
|
{xm_rs1, xm_rs2, xm_rd} <= {d_rs1, d_rs2, d_rd};
|
||||||
// If the transfer is unaligned, make sure it is completely NOP'd on the bus
|
// If the transfer is unaligned, make sure it is completely NOP'd on the bus
|
||||||
xm_memop <= d_memop | {x_unaligned_addr, 3'h0};
|
xm_memop <= d_memop | {x_unaligned_addr, 3'h0};
|
||||||
if (x_stall || flush_d_x || x_trap_enter) begin
|
if (x_stall || x_trap_enter) begin
|
||||||
// Insert bubble
|
// Insert bubble
|
||||||
xm_rd <= {W_REGADDR{1'b0}};
|
xm_rd <= {W_REGADDR{1'b0}};
|
||||||
xm_memop <= MEMOP_NONE;
|
xm_memop <= MEMOP_NONE;
|
||||||
|
@ -573,7 +562,7 @@ reg [W_DATA-1:0] m_rdata_shift;
|
||||||
reg [W_DATA-1:0] m_wdata;
|
reg [W_DATA-1:0] m_wdata;
|
||||||
reg [W_DATA-1:0] m_result;
|
reg [W_DATA-1:0] m_result;
|
||||||
|
|
||||||
assign m_stall = (!xm_memop[3] && !bus_dph_ready_d) || (m_jump_req && !f_jump_rdy);
|
assign m_stall = !xm_memop[3] && !bus_dph_ready_d;
|
||||||
|
|
||||||
wire m_except_bus_fault = bus_dph_err_d; // TODO: handle differently for LSU/ifetch?
|
wire m_except_bus_fault = bus_dph_err_d; // TODO: handle differently for LSU/ifetch?
|
||||||
|
|
||||||
|
|
|
@ -33,7 +33,6 @@ module hazard3_decode #(
|
||||||
|
|
||||||
output wire d_stall,
|
output wire d_stall,
|
||||||
input wire x_stall,
|
input wire x_stall,
|
||||||
input wire flush_d_x,
|
|
||||||
input wire f_jump_rdy,
|
input wire f_jump_rdy,
|
||||||
input wire f_jump_now,
|
input wire f_jump_now,
|
||||||
input wire [W_ADDR-1:0] f_jump_target,
|
input wire [W_ADDR-1:0] f_jump_target,
|
||||||
|
@ -55,7 +54,6 @@ module hazard3_decode #(
|
||||||
output reg [W_ADDR-1:0] d_jump_target,
|
output reg [W_ADDR-1:0] d_jump_target,
|
||||||
output reg d_jump_is_regoffs,
|
output reg d_jump_is_regoffs,
|
||||||
output reg d_result_is_linkaddr,
|
output reg d_result_is_linkaddr,
|
||||||
output reg [W_ADDR-1:0] d_pc,
|
|
||||||
output reg [W_ADDR-1:0] d_mispredict_addr,
|
output reg [W_ADDR-1:0] d_mispredict_addr,
|
||||||
output reg [2:0] d_except
|
output reg [2:0] d_except
|
||||||
);
|
);
|
||||||
|
@ -113,7 +111,7 @@ assign df_cir_use =
|
||||||
|
|
||||||
// Note it is possible for d_jump_req and m_jump_req to be asserted
|
// Note it is possible for d_jump_req and m_jump_req to be asserted
|
||||||
// simultaneously, hence checking flush:
|
// simultaneously, hence checking flush:
|
||||||
wire jump_caused_by_d = d_jump_req && f_jump_rdy && !flush_d_x;
|
wire jump_caused_by_d = d_jump_req && f_jump_rdy; /// FIXME what about JALR?
|
||||||
wire assert_cir_lock = jump_caused_by_d && d_stall;
|
wire assert_cir_lock = jump_caused_by_d && d_stall;
|
||||||
wire deassert_cir_lock = !d_stall;
|
wire deassert_cir_lock = !d_stall;
|
||||||
reg cir_lock_prev;
|
reg cir_lock_prev;
|
||||||
|
|
|
@ -8,6 +8,11 @@
|
||||||
//
|
//
|
||||||
// All modelling signals prefixed with rvfm (riscv-formal monitor)
|
// All modelling signals prefixed with rvfm (riscv-formal monitor)
|
||||||
|
|
||||||
|
// FIXME!!!!!
|
||||||
|
always assume(!(x_trap_enter || x_trap_exit));
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// ----------------------------------------------------------------------------
|
// ----------------------------------------------------------------------------
|
||||||
// Instruction monitor
|
// Instruction monitor
|
||||||
|
|
||||||
|
@ -16,8 +21,9 @@
|
||||||
|
|
||||||
// TODO fix all the redundant RVFI registers in a nice way
|
// TODO fix all the redundant RVFI registers in a nice way
|
||||||
|
|
||||||
reg rvfm_x_valid, rvfm_m_valid;
|
wire rvfm_x_valid = fd_cir_vld >= 2 || (fd_cir_vld >= 1 && fd_cir[1:0] != 2'b11);
|
||||||
reg [31:0] rvfm_x_instr;
|
|
||||||
|
reg rvfm_m_valid;
|
||||||
reg [31:0] rvfm_m_instr;
|
reg [31:0] rvfm_m_instr;
|
||||||
|
|
||||||
wire rvfm_x_trap = x_trap_is_exception && x_trap_enter;
|
wire rvfm_x_trap = x_trap_is_exception && x_trap_enter;
|
||||||
|
@ -34,7 +40,6 @@ assign rvfi_trap = rvfi_trap_r;
|
||||||
|
|
||||||
always @ (posedge clk or negedge rst_n) begin
|
always @ (posedge clk or negedge rst_n) begin
|
||||||
if (!rst_n) begin
|
if (!rst_n) begin
|
||||||
rvfm_x_valid <= 1'b0;
|
|
||||||
rvfm_m_valid <= 1'b0;
|
rvfm_m_valid <= 1'b0;
|
||||||
rvfm_m_trap <= 1'b0;
|
rvfm_m_trap <= 1'b0;
|
||||||
rvfm_entered_intr <= 1'b0;
|
rvfm_entered_intr <= 1'b0;
|
||||||
|
@ -44,33 +49,20 @@ always @ (posedge clk or negedge rst_n) begin
|
||||||
end else begin
|
end else begin
|
||||||
if (!x_stall) begin
|
if (!x_stall) begin
|
||||||
// Squash X instrs on IRQ entry -- these instructions will be reexecuted on return.
|
// Squash X instrs on IRQ entry -- these instructions will be reexecuted on return.
|
||||||
rvfm_m_valid <= rvfm_x_valid && !(x_trap_enter && x_trap_enter_rdy && !rvfm_x_trap);
|
rvfm_m_valid <= |df_cir_use && !(x_trap_enter && x_trap_enter_rdy && !rvfm_x_trap);
|
||||||
rvfm_m_instr <= rvfm_x_instr;
|
rvfm_m_instr <= {fd_cir[31:16] & {16{df_cir_use[1]}}, fd_cir[15:0]};
|
||||||
rvfm_x_valid <= 1'b0;
|
|
||||||
rvfm_m_trap <= rvfm_x_trap;
|
rvfm_m_trap <= rvfm_x_trap;
|
||||||
end else if (!m_stall) begin
|
end else if (!m_stall) begin
|
||||||
rvfm_m_valid <= 1'b0;
|
rvfm_m_valid <= 1'b0;
|
||||||
end
|
end
|
||||||
if (flush_d_x) begin
|
|
||||||
rvfm_x_valid <= 1'b0;
|
|
||||||
rvfm_m_valid <= rvfm_m_valid && m_stall;
|
|
||||||
end else if (df_cir_use) begin
|
|
||||||
rvfm_x_valid <= 1'b1;
|
|
||||||
rvfm_x_instr <= {
|
|
||||||
fd_cir[31:16] & {16{df_cir_use[1]}},
|
|
||||||
fd_cir[15:0]
|
|
||||||
};
|
|
||||||
end
|
|
||||||
rvfi_valid_r <= rvfm_m_valid && !m_stall;
|
rvfi_valid_r <= rvfm_m_valid && !m_stall;
|
||||||
rvfi_insn_r <= rvfm_m_instr;
|
rvfi_insn_r <= rvfm_m_instr;
|
||||||
rvfi_trap_r <= rvfm_m_trap;
|
rvfi_trap_r <= rvfm_m_trap;
|
||||||
|
|
||||||
// Take note of M-jump in pipe bubble in between instruction retires:
|
rvfm_entered_intr <= rvfm_entered_intr && !rvfi_valid;
|
||||||
rvfm_entered_intr <= (rvfm_entered_intr && !rvfi_valid)
|
|
||||||
|| (m_jump_req && f_jump_now && !rvfm_m_valid);
|
|
||||||
|
|
||||||
// Sanity checks
|
// Sanity checks
|
||||||
if (dx_rd != 5'h0)
|
if (d_rd != 5'h0)
|
||||||
assert(rvfm_x_valid);
|
assert(rvfm_x_valid);
|
||||||
if (xm_rd != 5'h0)
|
if (xm_rd != 5'h0)
|
||||||
assert(rvfm_m_valid);
|
assert(rvfm_m_valid);
|
||||||
|
@ -93,8 +85,6 @@ assign rvfi_halt = 1'b0; // TODO
|
||||||
// ----------------------------------------------------------------------------
|
// ----------------------------------------------------------------------------
|
||||||
// PC and jump monitor
|
// PC and jump monitor
|
||||||
|
|
||||||
reg rvfm_dx_have_jumped;
|
|
||||||
|
|
||||||
reg [31:0] rvfm_xm_pc;
|
reg [31:0] rvfm_xm_pc;
|
||||||
reg [31:0] rvfm_xm_pc_next;
|
reg [31:0] rvfm_xm_pc_next;
|
||||||
|
|
||||||
|
@ -112,12 +102,9 @@ always @ (posedge clk or negedge rst_n) begin
|
||||||
rvfm_xm_pc <= 0;
|
rvfm_xm_pc <= 0;
|
||||||
rvfm_xm_pc_next <= 0;
|
rvfm_xm_pc_next <= 0;
|
||||||
end else begin
|
end else begin
|
||||||
if (!d_stall) begin
|
|
||||||
rvfm_dx_have_jumped <= d_jump_req && f_jump_now || rvfm_past_df_cir_lock;
|
|
||||||
end
|
|
||||||
if (!x_stall) begin
|
if (!x_stall) begin
|
||||||
rvfm_xm_pc <= dx_pc;
|
rvfm_xm_pc <= d_pc;
|
||||||
rvfm_xm_pc_next <= rvfm_dx_have_jumped ? dx_jump_target : dx_mispredict_addr;
|
rvfm_xm_pc_next <= f_jump_now || rvfm_past_df_cir_lock ? x_jump_target : d_mispredict_addr;
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
@ -131,7 +118,7 @@ assign rvfi_pc_wdata = rvfi_pc_wdata_r;
|
||||||
always @ (posedge clk) begin
|
always @ (posedge clk) begin
|
||||||
if (!m_stall) begin
|
if (!m_stall) begin
|
||||||
rvfi_pc_rdata_r <= rvfm_xm_pc;
|
rvfi_pc_rdata_r <= rvfm_xm_pc;
|
||||||
rvfi_pc_wdata_r <= m_jump_req ? m_jump_target : rvfm_xm_pc_next;
|
rvfi_pc_wdata_r <= rvfm_xm_pc_next;
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
|
@ -190,11 +177,11 @@ reg [1:0] rvfm_htrans_dph;
|
||||||
reg [2:0] rvfm_hsize_dph;
|
reg [2:0] rvfm_hsize_dph;
|
||||||
|
|
||||||
always @ (posedge clk) begin
|
always @ (posedge clk) begin
|
||||||
if (ahblm_hready) begin
|
if (bus_aph_ready_d) begin
|
||||||
rvfm_htrans_dph <= ahblm_htrans & {2{ahb_gnt_d}}; // Load/store only!
|
rvfm_htrans_dph <= {bus_aph_req_d, 1'b0};
|
||||||
rvfm_haddr_dph <= ahblm_haddr;
|
rvfm_haddr_dph <= bus_haddr_d;
|
||||||
rvfm_hwrite_dph <= ahblm_hwrite;
|
rvfm_hwrite_dph <= bus_hwrite_d;
|
||||||
rvfm_hsize_dph <= ahblm_hsize;
|
rvfm_hsize_dph <= bus_hsize_d;
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
|
@ -217,16 +204,16 @@ assign rvfi_mem_wmask = rvfi_mem_wmask_r;
|
||||||
assign rvfi_mem_wdata = rvfi_mem_wdata_r;
|
assign rvfi_mem_wdata = rvfi_mem_wdata_r;
|
||||||
|
|
||||||
always @ (posedge clk) begin
|
always @ (posedge clk) begin
|
||||||
if (ahblm_hready) begin
|
if (bus_dph_ready_d) begin
|
||||||
// RVFI has an AXI-like concept of byte strobes, rather than AHB-like
|
// RVFI has an AXI-like concept of byte strobes, rather than AHB-like
|
||||||
rvfi_mem_addr_r <= rvfm_haddr_dph & 32'hffff_fffc;
|
rvfi_mem_addr_r <= rvfm_haddr_dph & 32'hffff_fffc;
|
||||||
{rvfi_mem_rmask_r, rvfi_mem_wmask_r} <= 0;
|
{rvfi_mem_rmask_r, rvfi_mem_wmask_r} <= 0;
|
||||||
if (rvfm_htrans_dph[1] && rvfm_hwrite_dph) begin
|
if (rvfm_htrans_dph[1] && rvfm_hwrite_dph) begin
|
||||||
rvfi_mem_wmask_r <= rvfm_mem_bytemask_dph;
|
rvfi_mem_wmask_r <= rvfm_mem_bytemask_dph;
|
||||||
rvfi_mem_wdata_r <= ahblm_hwdata;
|
rvfi_mem_wdata_r <= bus_wdata_d;
|
||||||
end else if (rvfm_htrans_dph[1] && !rvfm_hwrite_dph) begin
|
end else if (rvfm_htrans_dph[1] && !rvfm_hwrite_dph) begin
|
||||||
rvfi_mem_rmask_r <= rvfm_mem_bytemask_dph;
|
rvfi_mem_rmask_r <= rvfm_mem_bytemask_dph;
|
||||||
rvfi_mem_rdata_r <= ahblm_hrdata;
|
rvfi_mem_rdata_r <= bus_rdata_d;
|
||||||
end
|
end
|
||||||
end else begin
|
end else begin
|
||||||
// As far as RVFI is concerned nothing happens except final cycle of dphase
|
// As far as RVFI is concerned nothing happens except final cycle of dphase
|
||||||
|
|
|
@ -8,40 +8,59 @@ module rvfi_wrapper (
|
||||||
// Memory Interface
|
// Memory Interface
|
||||||
// ----------------------------------------------------------------------------
|
// ----------------------------------------------------------------------------
|
||||||
|
|
||||||
(* keep *) wire [31:0] haddr;
|
(* keep *) wire [31:0] i_haddr;
|
||||||
(* keep *) wire hwrite;
|
(* keep *) wire i_hwrite;
|
||||||
(* keep *) wire [1:0] htrans;
|
(* keep *) wire [1:0] i_htrans;
|
||||||
(* keep *) wire [2:0] hsize;
|
(* keep *) wire [2:0] i_hsize;
|
||||||
(* keep *) wire [2:0] hburst;
|
(* keep *) wire [2:0] i_hburst;
|
||||||
(* keep *) wire [3:0] hprot;
|
(* keep *) wire [3:0] i_hprot;
|
||||||
(* keep *) wire hmastlock;
|
(* keep *) wire i_hmastlock;
|
||||||
(* keep *) `rvformal_rand_reg hready;
|
(* keep *) `rvformal_rand_reg i_hready;
|
||||||
(* keep *) wire hresp;
|
(* keep *) wire i_hresp;
|
||||||
(* keep *) wire [31:0] hwdata;
|
(* keep *) wire [31:0] i_hwdata;
|
||||||
(* keep *) `rvformal_rand_reg [31:0] hrdata;
|
(* keep *) `rvformal_rand_reg [31:0] i_hrdata;
|
||||||
|
|
||||||
|
(* keep *) wire [31:0] d_haddr;
|
||||||
|
(* keep *) wire d_hwrite;
|
||||||
|
(* keep *) wire [1:0] d_htrans;
|
||||||
|
(* keep *) wire [2:0] d_hsize;
|
||||||
|
(* keep *) wire [2:0] d_hburst;
|
||||||
|
(* keep *) wire [3:0] d_hprot;
|
||||||
|
(* keep *) wire d_hmastlock;
|
||||||
|
(* keep *) `rvformal_rand_reg d_hready;
|
||||||
|
(* keep *) wire d_hresp;
|
||||||
|
(* keep *) wire [31:0] d_hwdata;
|
||||||
|
(* keep *) `rvformal_rand_reg [31:0] d_hrdata;
|
||||||
|
|
||||||
|
|
||||||
// AHB-lite requires: data phase of IDLE has no wait states
|
// AHB-lite requires: data phase of IDLE has no wait states
|
||||||
always @ (posedge clock)
|
always @ (posedge clock) begin
|
||||||
if ($past(htrans) == 2'b00 && $past(hready))
|
if ($past(i_htrans) == 2'b00 && $past(i_hready))
|
||||||
assume(hready);
|
assume(i_hready);
|
||||||
|
if ($past(d_htrans) == 2'b00 && $past(d_hready))
|
||||||
// Handling of bus faults is not tested
|
assume(d_hready);
|
||||||
// always assume(!hresp);
|
end
|
||||||
|
|
||||||
`ifdef RISCV_FORMAL_FAIRNESS
|
`ifdef RISCV_FORMAL_FAIRNESS
|
||||||
|
|
||||||
reg [7:0] bus_fairness_ctr;
|
reg [7:0] i_bus_fairness_ctr;
|
||||||
|
reg [7:0] d_bus_fairness_ctr;
|
||||||
localparam MAX_STALL_LENGTH = 8;
|
localparam MAX_STALL_LENGTH = 8;
|
||||||
|
|
||||||
always @ (posedge clock) begin
|
always @ (posedge clock) begin
|
||||||
if (reset)
|
if (reset) begin
|
||||||
bus_fairness_ctr <= 8'h0;
|
i_bus_fairness_ctr <= 8'h0;
|
||||||
else if (hready)
|
d_bus_fairness_ctr <= 8'h0;
|
||||||
bus_fairness_ctr <= 8'h0;
|
end else begin
|
||||||
else
|
i_bus_fairness_ctr <= i_bus_fairness_ctr + ~&i_bus_fairness_ctr;
|
||||||
bus_fairness_ctr <= bus_fairness_ctr + ~&bus_fairness_ctr;
|
d_bus_fairness_ctr <= d_bus_fairness_ctr + ~&d_bus_fairness_ctr;
|
||||||
|
if (i_hready)
|
||||||
assume(bus_fairness_ctr <= MAX_STALL_LENGTH);
|
i_bus_fairness_ctr <= 8'h0;
|
||||||
|
if (d_hready)
|
||||||
|
d_bus_fairness_ctr <= 8'h0;
|
||||||
|
end
|
||||||
|
assume(i_bus_fairness_ctr <= MAX_STALL_LENGTH);
|
||||||
|
assume(d_bus_fairness_ctr <= MAX_STALL_LENGTH);
|
||||||
end
|
end
|
||||||
|
|
||||||
`endif
|
`endif
|
||||||
|
@ -50,24 +69,44 @@ end
|
||||||
// Device Under Test
|
// Device Under Test
|
||||||
// ----------------------------------------------------------------------------
|
// ----------------------------------------------------------------------------
|
||||||
|
|
||||||
hazard3_cpu #(
|
(* keep *) `rvformal_rand_reg [15:0] irq;
|
||||||
|
|
||||||
|
hazard3_cpu_2port #(
|
||||||
.RESET_VECTOR (0),
|
.RESET_VECTOR (0),
|
||||||
.EXTENSION_C (1),
|
.EXTENSION_C (1),
|
||||||
.EXTENSION_M (1)
|
.EXTENSION_M (1),
|
||||||
|
.MUL_FAST (1),
|
||||||
|
.MULDIV_UNROLL (2)
|
||||||
) dut (
|
) dut (
|
||||||
.clk (clock),
|
.clk (clock),
|
||||||
.rst_n (!reset),
|
.rst_n (!reset),
|
||||||
.ahblm_haddr (haddr),
|
|
||||||
.ahblm_hwrite (hwrite),
|
.i_haddr (i_haddr),
|
||||||
.ahblm_htrans (htrans),
|
.i_hwrite (i_hwrite),
|
||||||
.ahblm_hsize (hsize),
|
.i_htrans (i_htrans),
|
||||||
.ahblm_hburst (hburst),
|
.i_hsize (i_hsize),
|
||||||
.ahblm_hprot (hprot),
|
.i_hburst (i_hburst),
|
||||||
.ahblm_hmastlock (hmastlock),
|
.i_hprot (i_hprot),
|
||||||
.ahblm_hready (hready),
|
.i_hmastlock (i_hmastlock),
|
||||||
.ahblm_hresp (hresp),
|
.i_hready (i_hready),
|
||||||
.ahblm_hwdata (hwdata),
|
.i_hresp (i_hresp),
|
||||||
.ahblm_hrdata (hrdata),
|
.i_hwdata (i_hwdata),
|
||||||
|
.i_hrdata (i_hrdata),
|
||||||
|
|
||||||
|
.d_haddr (d_haddr),
|
||||||
|
.d_hwrite (d_hwrite),
|
||||||
|
.d_htrans (d_htrans),
|
||||||
|
.d_hsize (d_hsize),
|
||||||
|
.d_hburst (d_hburst),
|
||||||
|
.d_hprot (d_hprot),
|
||||||
|
.d_hmastlock (d_hmastlock),
|
||||||
|
.d_hready (d_hready),
|
||||||
|
.d_hresp (d_hresp),
|
||||||
|
.d_hwdata (d_hwdata),
|
||||||
|
.d_hrdata (d_hrdata),
|
||||||
|
|
||||||
|
.irq (irq),
|
||||||
|
|
||||||
`RVFI_CONN
|
`RVFI_CONN
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue