diff --git a/bhv/cv32e40x_wrapper.sv b/bhv/cv32e40x_wrapper.sv index 28365d2a..775f9b8a 100644 --- a/bhv/cv32e40x_wrapper.sv +++ b/bhv/cv32e40x_wrapper.sv @@ -418,6 +418,7 @@ endgenerate .write_buffer_valid_o ('0), .write_buffer_txn_bufferable ('0), .write_buffer_txn_cacheable ('0), + .obi_if_state (core_i.if_stage_i.instruction_obi_i.state_q), .*); bind cv32e40x_mpu: @@ -444,6 +445,7 @@ endgenerate .write_buffer_valid_o (core_i.load_store_unit_i.write_buffer_i.valid_o), .write_buffer_txn_bufferable (core_i.load_store_unit_i.write_buffer_i.trans_o.memtype[0]), .write_buffer_txn_cacheable (core_i.load_store_unit_i.write_buffer_i.trans_o.memtype[1]), + .obi_if_state (cv32e40x_pkg::TRANSPARENT), .*); bind cv32e40x_lsu_response_filter : diff --git a/rtl/cv32e40x_align_check.sv b/rtl/cv32e40x_align_check.sv index dd861b5a..2203bdb3 100644 --- a/rtl/cv32e40x_align_check.sv +++ b/rtl/cv32e40x_align_check.sv @@ -41,7 +41,6 @@ module cv32e40x_align_check import cv32e40x_pkg::*; // Interface towards bus interface input logic bus_trans_ready_i, output logic bus_trans_valid_o, - output logic bus_trans_pushpop_o, output CORE_REQ_TYPE bus_trans_o, input logic bus_resp_valid_i, @@ -50,7 +49,6 @@ module cv32e40x_align_check import cv32e40x_pkg::*; // Interface towards core (MPU) input logic core_trans_valid_i, output logic core_trans_ready_o, - input logic core_trans_pushpop_i, input CORE_REQ_TYPE core_trans_i, output logic core_resp_valid_o, @@ -156,7 +154,6 @@ module cv32e40x_align_check import cv32e40x_pkg::*; // Forward transaction request towards MPU assign bus_trans_valid_o = core_trans_valid_i && !align_block_bus; assign bus_trans_o = core_trans_i; - assign bus_trans_pushpop_o = core_trans_pushpop_i; // Forward transaction response towards core diff --git a/rtl/cv32e40x_alignment_buffer.sv b/rtl/cv32e40x_alignment_buffer.sv index edfb2816..2f252cea 100644 --- a/rtl/cv32e40x_alignment_buffer.sv +++ b/rtl/cv32e40x_alignment_buffer.sv @@ -60,7 +60,7 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; output logic [31:0] instr_addr_o, output privlvl_t instr_priv_lvl_o, output logic instr_is_clic_ptr_o, // True CLIC pointer after taking a CLIC SHV interrupt - output logic instr_is_mret_ptr_o, // CLIC pointer due to restarting pionter fetch during mret + output logic instr_is_mret_ptr_o, // CLIC pointer due to restarting pointer fetch during mret output logic instr_is_tbljmp_ptr_o, output logic [ALBUF_CNT_WIDTH-1:0] outstnd_cnt_q_o ); @@ -97,9 +97,10 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; // Store number of responses to flush when get get a branch logic [1:0] n_flush_n, n_flush_q, n_flush_branch; - // Error propagation signals for bus and mpu + // Error propagation signals for bus, mpu and alignment checker (pointers) logic bus_err_unaligned, bus_err; mpu_status_e mpu_status_unaligned, mpu_status; + align_status_e align_status_unaligned, align_status; // resp_valid gated while flushing logic resp_valid_gated; @@ -163,9 +164,11 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; // Aligned instructions will either be fully in index 0 or incoming data // This also applies for the bus_error and mpu_status - assign instr = (valid_q[rptr]) ? resp_q[rptr].bus_resp.rdata : resp_i.bus_resp.rdata; - assign bus_err = (valid_q[rptr]) ? resp_q[rptr].bus_resp.err : resp_i.bus_resp.err; - assign mpu_status = (valid_q[rptr]) ? resp_q[rptr].mpu_status : resp_i.mpu_status; + assign instr = (valid_q[rptr]) ? resp_q[rptr].bus_resp.rdata : resp_i.bus_resp.rdata; + assign bus_err = (valid_q[rptr]) ? resp_q[rptr].bus_resp.err : resp_i.bus_resp.err; + assign mpu_status = (valid_q[rptr]) ? resp_q[rptr].mpu_status : resp_i.mpu_status; + assign align_status = (valid_q[rptr]) ? resp_q[rptr].align_status : resp_i.align_status; + // Unaligned instructions will either be split across index 0 and 1, or index 0 and incoming data assign instr_unaligned = (valid_q[rptr2]) ? {resp_q[rptr2].bus_resp.rdata[15:0], instr[31:16]} : {resp_i.bus_resp.rdata[15:0], instr[31:16]}; @@ -178,13 +181,19 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; assign valid = valid_q[rptr] || resp_valid_gated; // unaligned_is_compressed and aligned_is_compressed are only defined when valid = 1 (which implies that instr_valid_o will be 1) - assign unaligned_is_compressed = instr[17:16] != 2'b11; - assign aligned_is_compressed = instr[1:0] != 2'b11; + // Never flag a compressed instruction (aligned or misaligned) for pointers. Otherwise one could signal instr_valid_o twice for one pointer + // if the pointer itself looks like two compressed instructions. + assign unaligned_is_compressed = (instr[17:16] != 2'b11) && + !(instr_is_clic_ptr_o || instr_is_mret_ptr_o || instr_is_tbljmp_ptr_o); + + assign aligned_is_compressed = (instr[1:0] != 2'b11) && + !(instr_is_clic_ptr_o || instr_is_mret_ptr_o || instr_is_tbljmp_ptr_o); - // Set mpu_status and bus error for unaligned instructions + // Set mpu_status, align_status and bus error for unaligned instructions always_comb begin mpu_status_unaligned = MPU_OK; + align_status_unaligned = ALIGN_OK; bus_err_unaligned = 1'b0; // There is valid data in q1 (valid q0 is implied) if(valid_q[rptr2]) begin @@ -195,12 +204,18 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; mpu_status_unaligned = MPU_RE_FAULT; end + if((resp_q[rptr2].align_status != ALIGN_OK) || (resp_q[rptr].align_status != ALIGN_OK)) begin + align_status_unaligned = ALIGN_RE_ERR; + end + // Bus error from either entry bus_err_unaligned = (resp_q[rptr2].bus_resp.err || resp_q[rptr].bus_resp.err); end else begin // Compressed, use only mpu_status from q0 mpu_status_unaligned = resp_q[rptr].mpu_status; + align_status_unaligned = resp_q[rptr].align_status; + // bus error from q0 bus_err_unaligned = resp_q[rptr].bus_resp.err; end @@ -214,19 +229,24 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; mpu_status_unaligned = MPU_RE_FAULT; end + if((resp_q[rptr].align_status != ALIGN_OK) || (resp_i.align_status != ALIGN_OK)) begin + align_status_unaligned = ALIGN_RE_ERR; + end + // Bus error from q0 and resp_i bus_err_unaligned = (resp_q[rptr].bus_resp.err || resp_i.bus_resp.err); end else begin // There is unaligned data in q0 and it is compressed mpu_status_unaligned = resp_q[rptr].mpu_status; - + align_status_unaligned = resp_q[rptr].align_status; // Bus error from q0 bus_err_unaligned = resp_q[rptr].bus_resp.err; end end else begin // There is no data in the buffer, use input - mpu_status_unaligned = resp_i.mpu_status; - bus_err_unaligned = resp_i.bus_resp.err; + mpu_status_unaligned = resp_i.mpu_status; + bus_err_unaligned = resp_i.bus_resp.err; + align_status_unaligned = resp_i.align_status; end end end @@ -238,6 +258,7 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; instr_instr_o.bus_resp.rdata = instr; instr_instr_o.bus_resp.err = bus_err; instr_instr_o.mpu_status = mpu_status; + instr_instr_o.align_status = align_status; instr_valid_o = 1'b0; // Invalidate output if we get killed @@ -248,14 +269,20 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; instr_instr_o.bus_resp.rdata = instr_unaligned; instr_instr_o.bus_resp.err = bus_err_unaligned; instr_instr_o.mpu_status = mpu_status_unaligned; - // No instruction valid + instr_instr_o.align_status = align_status_unaligned; + if (!valid) begin + // No instruction valid instr_valid_o = 1'b0; - // Unaligned instruction is compressed, we only need 16 upper bits from index 0 + end else if (instr_is_clic_ptr_o || instr_is_mret_ptr_o || instr_is_tbljmp_ptr_o) begin + // currently outputting a pointer, valid whenever the response arrives or we have + // the pointer within index 0 of the buffer. + instr_valid_o = valid; end else if (unaligned_is_compressed) begin + // Unaligned instruction is compressed, we only need 16 upper bits from index 0 instr_valid_o = valid; end else begin - // Unaligned is not compressed, we need data form either index 0 and 1, or 0 and input + // Unaligned is not compressed, we need data from either index 0 and 1, or 0 and input instr_valid_o = valid_unaligned_uncompressed; end end else begin @@ -545,6 +572,11 @@ module cv32e40x_alignment_buffer import cv32e40x_pkg::*; if(instr_valid_o && instr_ready_i) begin addr_q <= addr_n; rptr <= rptr_n; + + // Clear pointer flags when pointers are consumed. + is_clic_ptr_q <= 1'b0; + is_mret_ptr_q <= 1'b0; + is_tbljmp_ptr_q <= 1'b0; end end diff --git a/rtl/cv32e40x_controller_bypass.sv b/rtl/cv32e40x_controller_bypass.sv index c135659d..c8d57fcd 100644 --- a/rtl/cv32e40x_controller_bypass.sv +++ b/rtl/cv32e40x_controller_bypass.sv @@ -194,7 +194,7 @@ module cv32e40x_controller_bypass import cv32e40x_pkg::*; // Also deassert for trigger match, as with dcsr.timing==0 we do not execute before entering debug mode // CLIC pointer fetches go through the pipeline, but no write enables should be active. if (if_id_pipe_i.instr.bus_resp.err || !(if_id_pipe_i.instr.mpu_status == MPU_OK) || if_id_pipe_i.trigger_match || - if_id_pipe_i.instr_meta.clic_ptr || if_id_pipe_i.instr_meta.mret_ptr) begin + if_id_pipe_i.instr_meta.clic_ptr || if_id_pipe_i.instr_meta.mret_ptr || !(if_id_pipe_i.instr.align_status == ALIGN_OK)) begin ctrl_byp_o.deassert_we = 1'b1; end diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv index 8ac0676c..efcf7505 100644 --- a/rtl/cv32e40x_controller_fsm.sv +++ b/rtl/cv32e40x_controller_fsm.sv @@ -338,6 +338,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // M | 1 | 1 | Debug entry (restart from dm_halt_addr_i) // assign exception_in_wb = ((ex_wb_pipe_i.instr.mpu_status != MPU_OK) || + (ex_wb_pipe_i.instr.align_status != ALIGN_OK) || ex_wb_pipe_i.instr.bus_resp.err || ex_wb_pipe_i.illegal_insn || (ex_wb_pipe_i.sys_en && ex_wb_pipe_i.sys_ecall_insn) || @@ -349,7 +350,8 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; assign ctrl_fsm_o.exception_in_wb = exception_in_wb; // Set exception cause - assign exception_cause_wb = (ex_wb_pipe_i.instr.mpu_status != MPU_OK) ? EXC_CAUSE_INSTR_FAULT : // todo: add code from align_check in IF + assign exception_cause_wb = (ex_wb_pipe_i.instr.mpu_status != MPU_OK) ? EXC_CAUSE_INSTR_FAULT : + (ex_wb_pipe_i.instr.align_status != ALIGN_OK) ? EXC_CAUSE_INSTR_MISALIGNED : ex_wb_pipe_i.instr.bus_resp.err ? EXC_CAUSE_INSTR_BUS_FAULT : ex_wb_pipe_i.illegal_insn ? EXC_CAUSE_ILLEGAL_INSN : (ex_wb_pipe_i.sys_en && ex_wb_pipe_i.sys_ecall_insn) ? EXC_CAUSE_ECALL_MMODE : @@ -1023,7 +1025,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; end end else if (clic_ptr_in_id || mret_ptr_in_id) begin // todo e40s: Factor in integrity related errors - if (!(if_id_pipe_i.instr.bus_resp.err || (if_id_pipe_i.instr.mpu_status != MPU_OK))) begin // todo: add check for alignment check in IF (mret pointer) + if (!(if_id_pipe_i.instr.bus_resp.err || (if_id_pipe_i.instr.mpu_status != MPU_OK) || (if_id_pipe_i.instr.align_status != ALIGN_OK))) begin if (!branch_taken_q) begin ctrl_fsm_o.pc_set = 1'b1; ctrl_fsm_o.pc_mux = PC_POINTER; diff --git a/rtl/cv32e40x_ex_stage.sv b/rtl/cv32e40x_ex_stage.sv index db57e057..ec80efb4 100644 --- a/rtl/cv32e40x_ex_stage.sv +++ b/rtl/cv32e40x_ex_stage.sv @@ -147,10 +147,11 @@ module cv32e40x_ex_stage import cv32e40x_pkg::*; // Exception happened during IF or ID, or trigger match in ID (converted to NOP). // signal needed for ex_valid to go high in such cases - assign previous_exception = (id_ex_pipe_i.illegal_insn || - id_ex_pipe_i.instr.bus_resp.err || - (id_ex_pipe_i.instr.mpu_status != MPU_OK) || - id_ex_pipe_i.trigger_match) && + assign previous_exception = (id_ex_pipe_i.illegal_insn || + id_ex_pipe_i.instr.bus_resp.err || + (id_ex_pipe_i.instr.mpu_status != MPU_OK) || + (id_ex_pipe_i.instr.align_status != ALIGN_OK) || + id_ex_pipe_i.trigger_match) && id_ex_pipe_i.instr_valid; // ALU write port mux diff --git a/rtl/cv32e40x_id_stage.sv b/rtl/cv32e40x_id_stage.sv index 6acfdfe0..fa33f591 100644 --- a/rtl/cv32e40x_id_stage.sv +++ b/rtl/cv32e40x_id_stage.sv @@ -666,6 +666,7 @@ module cv32e40x_id_stage import cv32e40x_pkg::*; id_ex_pipe_o.instr.bus_resp.rdata <= {16'h0, if_id_pipe_i.compressed_instr}; id_ex_pipe_o.instr.bus_resp.err <= if_id_pipe_i.instr.bus_resp.err; id_ex_pipe_o.instr.mpu_status <= if_id_pipe_i.instr.mpu_status; + id_ex_pipe_o.instr.align_status <= if_id_pipe_i.instr.align_status; end else begin id_ex_pipe_o.instr <= if_id_pipe_i.instr; end diff --git a/rtl/cv32e40x_if_stage.sv b/rtl/cv32e40x_if_stage.sv index d342e4d4..ef3520b7 100644 --- a/rtl/cv32e40x_if_stage.sv +++ b/rtl/cv32e40x_if_stage.sv @@ -117,6 +117,7 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; logic prefetch_trans_valid; logic prefetch_trans_ready; logic [31:0] prefetch_trans_addr; + logic prefetch_trans_ptr; inst_resp_t prefetch_inst_resp; logic prefetch_one_txn_pend_n; logic [ALBUF_CNT_WIDTH-1:0] prefetch_outstnd_cnt_q; @@ -134,6 +135,9 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; logic alcheck_trans_ready; obi_inst_req_t alcheck_trans; + logic align_check_en; + logic address_misaligned; + // Local instr_valid logic instr_valid; @@ -214,6 +218,7 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; .trans_valid_o ( prefetch_trans_valid ), .trans_ready_i ( prefetch_trans_ready ), .trans_addr_o ( prefetch_trans_addr ), + .trans_ptr_o ( prefetch_trans_ptr ), .resp_valid_i ( prefetch_resp_valid ), .resp_i ( prefetch_inst_resp ), @@ -274,6 +279,9 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; ); + assign align_check_en = prefetch_trans_ptr; + assign address_misaligned = |prefetch_trans_addr[1:0]; + cv32e40x_align_check #( .IF_STAGE ( 1 ), @@ -285,8 +293,8 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; ( .clk ( clk ), .rst_n ( rst_n ), - .align_check_en_i ( 1'b0 ), // todo: enable check for pointers - .misaligned_access_i ( 1'b0 ), + .align_check_en_i ( align_check_en ), + .misaligned_access_i ( address_misaligned ), .core_one_txn_pend_n ( prefetch_one_txn_pend_n ), .core_align_err_wait_i( 1'b1 ), @@ -372,7 +380,8 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; // Set flag to indicate that instruction/sequence will be aborted due to known exceptions or trigger match - assign abort_op_o = instr_decompressed.bus_resp.err || (instr_decompressed.mpu_status != MPU_OK) || trigger_match_i; + assign abort_op_o = instr_decompressed.bus_resp.err || (instr_decompressed.mpu_status != MPU_OK) || + (instr_decompressed.align_status != ALIGN_OK) || trigger_match_i; // Signal current privilege level of IF assign priv_lvl_if_o = prefetch_priv_lvl; @@ -437,7 +446,7 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; // For mret pointers, the pointer address is only needed downstream if the pointer fetch fails. // If the pointer fetch is successful, the address of the mret (i.e. the previous PC) is needed. if(prefetch_is_mret_ptr ? - (instr_decompressed.bus_resp.err || (instr_decompressed.mpu_status != MPU_OK)) : + (instr_decompressed.bus_resp.err || (instr_decompressed.mpu_status != MPU_OK) || (instr_decompressed.align_status != ALIGN_OK)) : 1'b1) begin if_id_pipe_o.pc <= pc_if_o; end @@ -461,6 +470,7 @@ module cv32e40x_if_stage import cv32e40x_pkg::*; // Need to update bus error status and mpu status, but may omit the 32-bit instruction word if_id_pipe_o.instr.bus_resp.err <= instr_decompressed.bus_resp.err; if_id_pipe_o.instr.mpu_status <= instr_decompressed.mpu_status; + if_id_pipe_o.instr.align_status <= instr_decompressed.align_status; end else begin // Regular instruction, update the whole instr field if_id_pipe_o.instr <= seq_valid ? seq_instr : instr_decompressed; diff --git a/rtl/cv32e40x_prefetch_unit.sv b/rtl/cv32e40x_prefetch_unit.sv index ec48ea3d..430ab68e 100644 --- a/rtl/cv32e40x_prefetch_unit.sv +++ b/rtl/cv32e40x_prefetch_unit.sv @@ -53,6 +53,7 @@ module cv32e40x_prefetch_unit import cv32e40x_pkg::*; output logic trans_valid_o, input logic trans_ready_i, output logic [31:0] trans_addr_o, + output logic trans_ptr_o, input logic resp_valid_i, input inst_resp_t resp_i, @@ -99,7 +100,8 @@ module cv32e40x_prefetch_unit import cv32e40x_pkg::*; .fetch_priv_lvl_access_o ( fetch_priv_lvl_resp ), .trans_valid_o ( trans_valid_o ), .trans_ready_i ( trans_ready_i ), - .trans_addr_o ( trans_addr_o ) + .trans_addr_o ( trans_addr_o ), + .trans_ptr_o ( trans_ptr_o ) ); diff --git a/rtl/cv32e40x_prefetcher.sv b/rtl/cv32e40x_prefetcher.sv index c2c80516..4e623947 100644 --- a/rtl/cv32e40x_prefetcher.sv +++ b/rtl/cv32e40x_prefetcher.sv @@ -58,9 +58,8 @@ module cv32e40x_prefetcher import cv32e40x_pkg::*; // Transaction request interface output logic trans_valid_o, // Transaction request valid (to bus interface adapter) input logic trans_ready_i, // Transaction request ready (transaction gets accepted when trans_valid_o and trans_ready_i are both 1) - output logic [31:0] trans_addr_o // Transaction address (only valid when trans_valid_o = 1). No stability requirements. - - + output logic [31:0] trans_addr_o, // Transaction address (only valid when trans_valid_o = 1). No stability requirements. + output logic trans_ptr_o // Transaction is fetching a pointer ); @@ -80,6 +79,8 @@ module cv32e40x_prefetcher import cv32e40x_pkg::*; // and will always be ready to accept responses. assign trans_valid_o = fetch_valid_i; + assign trans_ptr_o = fetch_ptr_access_o; + assign fetch_ready_o = trans_valid_o && trans_ready_i; // FSM (state_q, next_state) to control trans_addr_o diff --git a/sva/cv32e40x_alignment_buffer_sva.sv b/sva/cv32e40x_alignment_buffer_sva.sv index a3768e34..53f7c7fa 100644 --- a/sva/cv32e40x_alignment_buffer_sva.sv +++ b/sva/cv32e40x_alignment_buffer_sva.sv @@ -34,7 +34,11 @@ module cv32e40x_alignment_buffer_sva input logic [2:0] instr_cnt_n, input logic [2:0] instr_cnt_q, input logic instr_valid_o, + input logic instr_ready_i, input logic [31:0] instr_addr_o, + input logic instr_is_clic_ptr_o, + input logic instr_is_mret_ptr_o, + input logic instr_is_tbljmp_ptr_o, input logic resp_valid_i, input logic resp_valid_gated, input logic [1:0] outstanding_cnt_q, @@ -43,8 +47,8 @@ module cv32e40x_alignment_buffer_sva input logic [1:0] wptr, input logic [1:0] rptr, input logic [1:0] rptr2, - input logic pop_q - + input logic pop_q, + input logic ptr_fetch_accepted_q ); @@ -237,7 +241,66 @@ module cv32e40x_alignment_buffer_sva else `uvm_error("Alignment buffer SVA", "Read pointer(2) illegal value") + // Check that the alignment buffer is empty when a pointer is received. + property p_pointer_fetch_empty; + @(posedge clk) disable iff (!rst_n) + ptr_fetch_accepted_q && resp_valid_i + |-> + !(|valid_q); + endproperty + + a_pointer_fetch_empty: + assert property(p_pointer_fetch_empty) + else + `uvm_error("Alignment buffer SVA", "Buffer not empty when requested pointer arrives.") + + // Check that a pointer is only emitted once. + // Pointers that look like two compressed instructions could cause two instr_rvalid_o's + property p_single_pointer_valid; + @(posedge clk) disable iff (!rst_n) + (instr_valid_o && instr_ready_i) && + (instr_is_clic_ptr_o || instr_is_mret_ptr_o || instr_is_tbljmp_ptr_o) + |=> + !instr_valid_o until_with(ctrl_fsm_i.pc_set); + endproperty + + a_single_pointer_valid: + assert property(p_single_pointer_valid) + else + `uvm_error("Alignment buffer SVA", "Multiple instr_valid_o for one pointer") + + // Check that we signal instr_valid_o when we have no outstanding transactions or ongoing requests. + // Unless we already signaled a valid pointer (then further fetches are blocked) + logic ptr_flagged; + always_ff @(posedge clk, negedge rst_n) begin + if(rst_n == 1'b0) begin + ptr_flagged <= 1'b0; + end else begin + if(ctrl_fsm_i.pc_set) begin + ptr_flagged <= 1'b0; + end else begin + if (instr_valid_o && instr_ready_i && (instr_is_clic_ptr_o || instr_is_mret_ptr_o || instr_is_tbljmp_ptr_o)) begin + ptr_flagged <= 1'b1; + end + end + end + end + + property p_no_outstanding_instr_valid; + @(posedge clk) disable iff (!rst_n) + ctrl_fsm_i.instr_req && // We are commanded to prefetch + !(|outstanding_cnt_q) && // There are no outstanding transactions + !fetch_valid_o // We are not requesting anything + |-> + instr_valid_o // There must be a valid entry in the buffer + or + ptr_flagged; // Or a pointer has already been sent out + endproperty +a_no_outstanding_instr_valid: + assert property(p_no_outstanding_instr_valid) + else + `uvm_error("Alignment buffer SVA", "No instr_valid when expected") endmodule // cv32e40x_alignment_buffer_sva diff --git a/sva/cv32e40x_core_sva.sv b/sva/cv32e40x_core_sva.sv index f6d8952d..c307e476 100644 --- a/sva/cv32e40x_core_sva.sv +++ b/sva/cv32e40x_core_sva.sv @@ -214,7 +214,7 @@ always_ff @(posedge clk , negedge rst_ni) expected_ebrk_mepc <= ex_wb_pipe.pc; end - if (!first_instr_err_found && (ex_wb_pipe.instr.mpu_status == MPU_OK) && !irq_ack && !pending_debug && + if (!first_instr_err_found && (ex_wb_pipe.instr.mpu_status == MPU_OK) && (ex_wb_pipe.instr.align_status == ALIGN_OK) && !irq_ack && !pending_debug && !(ctrl_fsm.pc_mux == PC_TRAP_NMI) && ex_wb_pipe.instr_valid && ex_wb_pipe.instr.bus_resp.err && !ctrl_debug_mode_n ) begin first_instr_err_found <= 1'b1; diff --git a/sva/cv32e40x_if_stage_sva.sv b/sva/cv32e40x_if_stage_sva.sv index 1bf285b9..f2081f79 100644 --- a/sva/cv32e40x_if_stage_sva.sv +++ b/sva/cv32e40x_if_stage_sva.sv @@ -42,7 +42,10 @@ module cv32e40x_if_stage_sva input logic prefetch_is_clic_ptr, input logic prefetch_is_mret_ptr, input logic [31:0] branch_addr_n, - input logic align_err_i + input logic align_err_i, + input logic alcheck_trans_valid, + input logic id_ready_i, + input logic ptr_in_if_o ); // Check that bus interface transactions are halfword aligned (will be forced word aligned at core boundary) @@ -110,19 +113,22 @@ module cv32e40x_if_stage_sva assert property (@(posedge clk) disable iff (!rst_n) (ctrl_fsm_i.pc_set_clicv) && (ctrl_fsm_i.pc_mux == PC_MRET) && - (branch_addr_n[1:0] == 2'b00) + (branch_addr_n[1:0] != 2'b00) |-> align_err_i ) else `uvm_error("if_stage", "Misaligned mret pointer not flagged with error") - // Aligned errors may only happen for mret pointers + // Aligned errors may only happen for mret pointers that are not otherwise blocked by the MPU a_aligned_err_mret_ptr: assert property (@(posedge clk) disable iff (!rst_n) - align_err_i + align_err_i && // Alignment error flagged + alcheck_trans_valid // Transaction not blocked by MPU |-> - (ctrl_fsm_i.pc_set_clicv) && + ((ctrl_fsm_i.pc_set_clicv) && // We have a pc_set for an mret pointer this cycle (ctrl_fsm_i.pc_mux == PC_MRET)) + or + prefetch_is_mret_ptr) // Or the trans_valid comes after the pc_set and an mret pointer is flagged else `uvm_error("if_stage", "Alignment error withouth mret pointer") end else begin @@ -133,6 +139,7 @@ module cv32e40x_if_stage_sva else `uvm_error("if_stage", "Alignment error withouth CLIC support.") end + // Tablejump pointer shall always be aligned a_aligned_tbljmp_ptr: assert property (@(posedge clk) disable iff (!rst_n) (ctrl_fsm_i.pc_set) && @@ -140,5 +147,17 @@ module cv32e40x_if_stage_sva |-> (branch_addr_n[1:0] == 2'b00)) else `uvm_error("if_stage", "Misaligned tablejump pointer") + + // Once a pointer exits IF, there cannot be another pointer following it. + // A possible case could be a SHV CLIC pointer following a tablejump pointer, but + // such a scenario would contain at least one bubble since acking the interrupt + // would kill the pipeline and redirect the prefetcher to the CLIC table. + a_no_ptr_after_ptr: + assert property (@(posedge clk) disable iff (!rst_n) + (if_valid_o && id_ready_i) && + ptr_in_if_o + |=> + !ptr_in_if_o) + else `uvm_error("if_stage", "IF stage flagging pointer after pointer has progressed to ID") endmodule // cv32e40x_if_stage diff --git a/sva/cv32e40x_mpu_sva.sv b/sva/cv32e40x_mpu_sva.sv index fefeee06..2bf47d2c 100644 --- a/sva/cv32e40x_mpu_sva.sv +++ b/sva/cv32e40x_mpu_sva.sv @@ -56,6 +56,8 @@ module cv32e40x_mpu_sva import cv32e40x_pkg::*; import uvm_pkg::*; input logic obi_gnt, input logic obi_dbg, + input obi_if_state_e obi_if_state, + // Interface towards bus interface input logic bus_trans_ready_i, input logic bus_trans_valid_o, @@ -323,12 +325,12 @@ module cv32e40x_mpu_sva import cv32e40x_pkg::*; import uvm_pkg::*; (!pma_err && is_addr_match) || // or a transaction from the write buffer is causing obi_req // (a different transaction could cause pma_err in the same cycle) - (write_buffer_state && write_buffer_valid_o) || + (!IS_INSTR_SIDE && (write_buffer_state && write_buffer_valid_o)) || // or we are already outputting a obi_req but a new address comes in which may cause a pma_err - (!is_addr_match && was_obi_waiting && $past(obi_req)) || + (IS_INSTR_SIDE && (!is_addr_match && (obi_if_state == REGISTERED))) || // or we get an address match, but was already outputting the same address (no pma_err) // but a change in debug mode causes the new transaction the same address to fail - (is_addr_match && was_obi_waiting && $past(obi_req) && (!pma_dbg && obi_dbg))) + (IS_INSTR_SIDE && (is_addr_match && (obi_if_state == REGISTERED) && (!pma_dbg && obi_dbg)))) else `uvm_error("mpu", "obi made request to pma-forbidden region") generate