diff --git a/hdl/hazard3_core.v b/hdl/hazard3_core.v index 05c8316..fb59af7 100644 --- a/hdl/hazard3_core.v +++ b/hdl/hazard3_core.v @@ -72,8 +72,6 @@ module hazard3_core #( //synthesis translate_on `endif -wire flush_d_x; - wire d_stall; wire x_stall; wire m_stall; @@ -82,8 +80,6 @@ localparam HSIZE_WORD = 3'd2; localparam HSIZE_HWORD = 3'd1; localparam HSIZE_BYTE = 3'd0; - - // ---------------------------------------------------------------------------- // Pipe Stage F @@ -103,7 +99,7 @@ wire [1:0] fd_cir_vld; wire [1:0] df_cir_use; wire df_cir_lock; -assign bus_aph_panic_i = m_jump_req; +assign bus_aph_panic_i = 1'b0; wire f_mem_size; assign bus_hsize_i = f_mem_size ? HSIZE_WORD : HSIZE_HWORD; @@ -137,8 +133,6 @@ hazard3_frontend #( .next_regs_vld (f_regnum_vld) ); -assign flush_d_x = m_jump_req && f_jump_rdy; - // ---------------------------------------------------------------------------- // Pipe Stage X (Decode Logic) @@ -198,7 +192,6 @@ hazard3_decode #( .d_stall (d_stall), .x_stall (x_stall), - .flush_d_x (flush_d_x), .f_jump_rdy (f_jump_rdy), .f_jump_now (f_jump_now), .f_jump_target (f_jump_target), @@ -262,8 +255,11 @@ reg [W_MEMOP-1:0] xm_memop; reg x_stall_raw; wire x_stall_muldiv; -assign x_stall = m_stall || - x_stall_raw || x_stall_muldiv || bus_aph_req_d && !bus_aph_ready_d; +assign x_stall = + 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_generating_result = xm_memop < MEMOP_SW || m_fast_mul_result_vld; @@ -310,10 +306,7 @@ always @ (*) begin MEMOP_SH: bus_hsize_d = HSIZE_HWORD; default: bus_hsize_d = HSIZE_BYTE; endcase - // m_jump_req implies flush_d_x is coming. Can't use flush_d_x because it's - // 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); + bus_aph_req_d = x_memop_vld && !(x_stall_raw || x_trap_enter); end // ALU operand muxes and bypass @@ -353,14 +346,12 @@ end wire x_except_ecall = d_except == EXCEPT_ECALL; wire x_except_breakpoint = d_except == EXCEPT_EBREAK; wire x_except_invalid_instr = d_except == EXCEPT_INSTR_ILLEGAL; -assign x_trap_exit = d_except == EXCEPT_MRET && !(x_stall || m_jump_req); -wire x_trap_enter_rdy = !(x_stall || m_jump_req || x_trap_exit); +assign x_trap_exit = d_except == EXCEPT_MRET; +wire x_trap_enter_rdy = !(x_stall || x_trap_exit); wire x_trap_is_exception; // diagnostic `ifdef FORMAL always @ (posedge clk) begin - if (flush_d_x) - assert(!x_trap_enter_rdy); if (x_trap_exit) assert(!bus_aph_req_d); end @@ -383,11 +374,11 @@ hazard3_csr #( .addr (d_imm[11:0]), // todo could just connect this to the instruction bits .wdata (x_csr_wdata), .wen_soon (d_csr_wen), - .wen (d_csr_wen && !(x_stall || flush_d_x)), + .wen (d_csr_wen && !x_stall), .wtype (d_csr_wtype), .rdata (x_csr_rdata), .ren_soon (d_csr_ren), - .ren (d_csr_ren && !(x_stall || flush_d_x)), + .ren (d_csr_ren && !x_stall), // Trap signalling .trap_addr (x_trap_addr), .trap_enter_vld (x_trap_enter), @@ -431,7 +422,7 @@ if (EXTENSION_M) begin: has_muldiv else 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; @@ -468,7 +459,7 @@ if (EXTENSION_M) begin: has_muldiv 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 #( .XLEN(W_DATA) @@ -511,13 +502,11 @@ always @ (posedge clk or negedge rst_n) begin xm_memop <= MEMOP_NONE; {xm_rs1, xm_rs2, xm_rd} <= {3 * W_REGADDR{1'b0}}; 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 {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 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 xm_rd <= {W_REGADDR{1'b0}}; 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_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? diff --git a/hdl/hazard3_decode.v b/hdl/hazard3_decode.v index 361a6a0..8eb7e83 100644 --- a/hdl/hazard3_decode.v +++ b/hdl/hazard3_decode.v @@ -33,7 +33,6 @@ module hazard3_decode #( output wire d_stall, input wire x_stall, - input wire flush_d_x, input wire f_jump_rdy, input wire f_jump_now, 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 d_jump_is_regoffs, 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 [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 // 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 deassert_cir_lock = !d_stall; reg cir_lock_prev; diff --git a/hdl/hazard3_rvfi_monitor.vh b/hdl/hazard3_rvfi_monitor.vh index 50d11b5..4318808 100644 --- a/hdl/hazard3_rvfi_monitor.vh +++ b/hdl/hazard3_rvfi_monitor.vh @@ -8,6 +8,11 @@ // // All modelling signals prefixed with rvfm (riscv-formal monitor) +// FIXME!!!!! +always assume(!(x_trap_enter || x_trap_exit)); + + + // ---------------------------------------------------------------------------- // Instruction monitor @@ -16,8 +21,9 @@ // TODO fix all the redundant RVFI registers in a nice way -reg rvfm_x_valid, rvfm_m_valid; -reg [31:0] rvfm_x_instr; +wire rvfm_x_valid = fd_cir_vld >= 2 || (fd_cir_vld >= 1 && fd_cir[1:0] != 2'b11); + +reg rvfm_m_valid; reg [31:0] rvfm_m_instr; 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 if (!rst_n) begin - rvfm_x_valid <= 1'b0; rvfm_m_valid <= 1'b0; rvfm_m_trap <= 1'b0; rvfm_entered_intr <= 1'b0; @@ -44,33 +49,20 @@ always @ (posedge clk or negedge rst_n) begin end else begin if (!x_stall) begin // 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_instr <= rvfm_x_instr; - rvfm_x_valid <= 1'b0; + rvfm_m_valid <= |df_cir_use && !(x_trap_enter && x_trap_enter_rdy && !rvfm_x_trap); + rvfm_m_instr <= {fd_cir[31:16] & {16{df_cir_use[1]}}, fd_cir[15:0]}; rvfm_m_trap <= rvfm_x_trap; end else if (!m_stall) begin rvfm_m_valid <= 1'b0; 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_insn_r <= rvfm_m_instr; 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) - || (m_jump_req && f_jump_now && !rvfm_m_valid); + rvfm_entered_intr <= rvfm_entered_intr && !rvfi_valid; // Sanity checks - if (dx_rd != 5'h0) + if (d_rd != 5'h0) assert(rvfm_x_valid); if (xm_rd != 5'h0) assert(rvfm_m_valid); @@ -93,8 +85,6 @@ assign rvfi_halt = 1'b0; // TODO // ---------------------------------------------------------------------------- // PC and jump monitor -reg rvfm_dx_have_jumped; - reg [31:0] rvfm_xm_pc; 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_next <= 0; 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 - rvfm_xm_pc <= dx_pc; - rvfm_xm_pc_next <= rvfm_dx_have_jumped ? dx_jump_target : dx_mispredict_addr; + rvfm_xm_pc <= d_pc; + rvfm_xm_pc_next <= f_jump_now || rvfm_past_df_cir_lock ? x_jump_target : d_mispredict_addr; end end end @@ -131,7 +118,7 @@ assign rvfi_pc_wdata = rvfi_pc_wdata_r; always @ (posedge clk) begin if (!m_stall) begin 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 @@ -190,11 +177,11 @@ reg [1:0] rvfm_htrans_dph; reg [2:0] rvfm_hsize_dph; always @ (posedge clk) begin - if (ahblm_hready) begin - rvfm_htrans_dph <= ahblm_htrans & {2{ahb_gnt_d}}; // Load/store only! - rvfm_haddr_dph <= ahblm_haddr; - rvfm_hwrite_dph <= ahblm_hwrite; - rvfm_hsize_dph <= ahblm_hsize; + if (bus_aph_ready_d) begin + rvfm_htrans_dph <= {bus_aph_req_d, 1'b0}; + rvfm_haddr_dph <= bus_haddr_d; + rvfm_hwrite_dph <= bus_hwrite_d; + rvfm_hsize_dph <= bus_hsize_d; end end @@ -217,16 +204,16 @@ assign rvfi_mem_wmask = rvfi_mem_wmask_r; assign rvfi_mem_wdata = rvfi_mem_wdata_r; 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_mem_addr_r <= rvfm_haddr_dph & 32'hffff_fffc; {rvfi_mem_rmask_r, rvfi_mem_wmask_r} <= 0; if (rvfm_htrans_dph[1] && rvfm_hwrite_dph) begin 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 rvfi_mem_rmask_r <= rvfm_mem_bytemask_dph; - rvfi_mem_rdata_r <= ahblm_hrdata; + rvfi_mem_rdata_r <= bus_rdata_d; end end else begin // As far as RVFI is concerned nothing happens except final cycle of dphase diff --git a/hdl/hazard3_rvfi_wrapper.v b/hdl/hazard3_rvfi_wrapper.v index 0691b91..ecec6e5 100644 --- a/hdl/hazard3_rvfi_wrapper.v +++ b/hdl/hazard3_rvfi_wrapper.v @@ -8,40 +8,59 @@ module rvfi_wrapper ( // Memory Interface // ---------------------------------------------------------------------------- -(* keep *) wire [31:0] haddr; -(* keep *) wire hwrite; -(* keep *) wire [1:0] htrans; -(* keep *) wire [2:0] hsize; -(* keep *) wire [2:0] hburst; -(* keep *) wire [3:0] hprot; -(* keep *) wire hmastlock; -(* keep *) `rvformal_rand_reg hready; -(* keep *) wire hresp; -(* keep *) wire [31:0] hwdata; -(* keep *) `rvformal_rand_reg [31:0] hrdata; +(* keep *) wire [31:0] i_haddr; +(* keep *) wire i_hwrite; +(* keep *) wire [1:0] i_htrans; +(* keep *) wire [2:0] i_hsize; +(* keep *) wire [2:0] i_hburst; +(* keep *) wire [3:0] i_hprot; +(* keep *) wire i_hmastlock; +(* keep *) `rvformal_rand_reg i_hready; +(* keep *) wire i_hresp; +(* keep *) wire [31:0] i_hwdata; +(* 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 -always @ (posedge clock) - if ($past(htrans) == 2'b00 && $past(hready)) - assume(hready); - -// Handling of bus faults is not tested -// always assume(!hresp); +always @ (posedge clock) begin + if ($past(i_htrans) == 2'b00 && $past(i_hready)) + assume(i_hready); + if ($past(d_htrans) == 2'b00 && $past(d_hready)) + assume(d_hready); +end `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; always @ (posedge clock) begin - if (reset) - bus_fairness_ctr <= 8'h0; - else if (hready) - bus_fairness_ctr <= 8'h0; - else - bus_fairness_ctr <= bus_fairness_ctr + ~&bus_fairness_ctr; - - assume(bus_fairness_ctr <= MAX_STALL_LENGTH); + if (reset) begin + i_bus_fairness_ctr <= 8'h0; + d_bus_fairness_ctr <= 8'h0; + end else begin + i_bus_fairness_ctr <= i_bus_fairness_ctr + ~&i_bus_fairness_ctr; + d_bus_fairness_ctr <= d_bus_fairness_ctr + ~&d_bus_fairness_ctr; + if (i_hready) + 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 `endif @@ -50,24 +69,44 @@ end // Device Under Test // ---------------------------------------------------------------------------- -hazard3_cpu #( - .RESET_VECTOR (0), - .EXTENSION_C (1), - .EXTENSION_M (1) +(* keep *) `rvformal_rand_reg [15:0] irq; + +hazard3_cpu_2port #( + .RESET_VECTOR (0), + .EXTENSION_C (1), + .EXTENSION_M (1), + .MUL_FAST (1), + .MULDIV_UNROLL (2) ) dut ( - .clk (clock), - .rst_n (!reset), - .ahblm_haddr (haddr), - .ahblm_hwrite (hwrite), - .ahblm_htrans (htrans), - .ahblm_hsize (hsize), - .ahblm_hburst (hburst), - .ahblm_hprot (hprot), - .ahblm_hmastlock (hmastlock), - .ahblm_hready (hready), - .ahblm_hresp (hresp), - .ahblm_hwdata (hwdata), - .ahblm_hrdata (hrdata), + .clk (clock), + .rst_n (!reset), + + .i_haddr (i_haddr), + .i_hwrite (i_hwrite), + .i_htrans (i_htrans), + .i_hsize (i_hsize), + .i_hburst (i_hburst), + .i_hprot (i_hprot), + .i_hmastlock (i_hmastlock), + .i_hready (i_hready), + .i_hresp (i_hresp), + .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 );