From 6982e3e14e2f7aa25e8bebd90145582148eb50ce Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 10:12:10 +0200 Subject: [PATCH 01/23] Removed todo. CLIC assertions implemented in core-v-verif. Signed-off-by: Oivind Ekelund --- sva/cv32e40x_core_sva.sv | 1 - 1 file changed, 1 deletion(-) diff --git a/sva/cv32e40x_core_sva.sv b/sva/cv32e40x_core_sva.sv index c0f568549..d7e05f1c8 100644 --- a/sva/cv32e40x_core_sva.sv +++ b/sva/cv32e40x_core_sva.sv @@ -149,7 +149,6 @@ if (CLIC) begin endproperty a_clic_mip_tieoff : assert property(p_clic_mip_tieoff) else `uvm_error("core", "MIP not tied to 0 in CLIC mode") - //todo: add CLIC related assertions (level thresholds etc) end else begin // CLIC == 0 // Check that a taken IRQ is actually enabled (e.g. that we do not react to an IRQ that was just disabled in MIE) From d4928493b4f726f8b27bd8290f3ff79144b6e201 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 10:26:12 +0200 Subject: [PATCH 02/23] Remove CLIC guard around a_single_ptr_fetch. Valid and passing with and without CLIC. Signed-off-by: Oivind Ekelund --- sva/cv32e40x_prefetch_unit_sva.sv | 2 -- 1 file changed, 2 deletions(-) diff --git a/sva/cv32e40x_prefetch_unit_sva.sv b/sva/cv32e40x_prefetch_unit_sva.sv index 5cb835c2e..6416dc6f4 100644 --- a/sva/cv32e40x_prefetch_unit_sva.sv +++ b/sva/cv32e40x_prefetch_unit_sva.sv @@ -58,7 +58,6 @@ module cv32e40x_prefetch_unit_sva import cv32e40x_pkg::*; a_branch_implies_req : assert property(p_branch_implies_req) else `uvm_error("prefetch_buffer", "Assertion a_branch_implies_req failed") -if (CLIC) begin // Shall not fetch anything between pointer fetch and the actual instruction fetch // based on the pointer. property p_single_ptr_fetch; @@ -70,7 +69,6 @@ if (CLIC) begin assert property(p_single_ptr_fetch) else `uvm_error("Alignment buffer SVA", "Multiple fetches for CLIC/Zc pointer") -end // CLIC endmodule // cv32e40x_prefetch_unit From 49d53818af0eba2003c1a05b92d8d33b6eecdfd6 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 10:29:13 +0200 Subject: [PATCH 03/23] Remove assertion a_data_ind_timing. Not applicable for CV32E40X. Signed-off-by: Oivind Ekelund --- sva/cv32e40x_div_sva.sv | 29 ++--------------------------- 1 file changed, 2 insertions(+), 27 deletions(-) diff --git a/sva/cv32e40x_div_sva.sv b/sva/cv32e40x_div_sva.sv index 02f1f0e5d..049229f9a 100644 --- a/sva/cv32e40x_div_sva.sv +++ b/sva/cv32e40x_div_sva.sv @@ -29,35 +29,10 @@ module cv32e40x_div_sva input logic ready_o, input logic ready_i, - input logic valid_o, - - input logic data_ind_timing_i + input logic valid_o ); - - logic [5:0] cycle_count; - - // Division cycle counter - always_ff @(posedge clk) begin - if (valid_i && $past(ready_o)) begin - // Division accpted, reset counter - cycle_count <= '0; - end - else begin - cycle_count <= cycle_count + 1'b1; - end - end - // Assert that valid_o is set in the 34th cycle - // cycle_count==33 in the 34th cycle because the counter is reset in the cycle after division is accepted. - //TODO: lowThis only applies to the 40S, data_ind_timing_i only exists there. - // Keep commented until 40S fork, and then delete from 40X - /* - a_data_ind_timing : - assert property (@(posedge clk) disable iff (!rst_n) - ($rose(valid_o) && data_ind_timing_i |-> cycle_count == 33)) - else `uvm_error("div", "Data independent cycle count failed") - */ - a_ready_o : + a_ready_o : assert property (@(posedge clk) disable iff (!rst_n) (valid_o && ready_i |-> ready_o)) else `uvm_error("div", "ready_o not set in the same cycle as output is accepted") From 107568325180878c8d02f44abf5c4c7ba93526f2 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 10:32:19 +0200 Subject: [PATCH 04/23] Remove TODO. Assertion is correct and passing as it is. Signed-off-by: Oivind Ekelund --- sva/cv32e40x_cs_registers_sva.sv | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/sva/cv32e40x_cs_registers_sva.sv b/sva/cv32e40x_cs_registers_sva.sv index 9b96c428e..5a6e18738 100644 --- a/sva/cv32e40x_cs_registers_sva.sv +++ b/sva/cv32e40x_cs_registers_sva.sv @@ -361,9 +361,8 @@ generate else `uvm_error("cs_registers", "mepc not written with ctrl_fsm.pipe_pc when etrigger fires."); // Exception trigger shall cause dpc to point to first handler instruction and no instruction shall signal wb_valid the cycle after (while in DEBUG_TAKEN state) - // Excluding external debug and interrupts (halt_wb, kill_wb) as they (currently) both take priority over etrigger + // Excluding external debug and interrupts (halt_wb, kill_wb) as they both take priority over etrigger // Also checking that WB stage is empty after an exception trigger has been taken. - // todo: update when debug causes are updated, trigger match will not be highest priority property p_etrigger_dpc_write; logic [24:0] mtvec_at_trap; @(posedge clk) disable iff (!rst_n) From 951f3f435d1e88c527be0ea5e608e444e4538fb8 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 11:20:07 +0200 Subject: [PATCH 05/23] Add check for rf_we in assertions checking suppression of csr_en. Add todo:xif tag on xif related assertions. Signed-off-by: Oivind Ekelund --- sva/cv32e40x_ex_stage_sva.sv | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/sva/cv32e40x_ex_stage_sva.sv b/sva/cv32e40x_ex_stage_sva.sv index bd42cc9ec..8fe4a59f1 100644 --- a/sva/cv32e40x_ex_stage_sva.sv +++ b/sva/cv32e40x_ex_stage_sva.sv @@ -66,7 +66,7 @@ module cv32e40x_ex_stage_sva generate if(X_EXT == 1'b1) begin // csr_en suppressed for xif accepted and pipeline accepted CSR - // todo: Add similar check for rf_we + // todo:xif Add similar check for rf_we a_suppress_csr_xif_legal_pipeline_legal : assert property (@(posedge clk) disable iff (!rst_n) ((id_ex_pipe_i.xif_en && id_ex_pipe_i.xif_meta.accepted) && id_ex_pipe_i.csr_en && !csr_illegal_i) && @@ -75,7 +75,7 @@ generate else `uvm_error("ex_stage", "csr_en not suppressed after eXtension interface and pipeline accepted CSR") // csr_en suppressed for xif accepted and pipeline rejected CSR - // todo: Add similar check for rf_we + // todo:xif Add similar check for rf_we a_suppress_csr_xif_legal_pipeline_illegal : assert property (@(posedge clk) disable iff (!rst_n) ((id_ex_pipe_i.xif_en && id_ex_pipe_i.xif_meta.accepted) && id_ex_pipe_i.csr_en && csr_illegal_i) && @@ -84,23 +84,22 @@ generate else `uvm_error("ex_stage", "csr_en not suppressed after eXtension interface accepted and pipeline rejected CSR") end endgenerate + // csr_en suppressed for xif reject and pipeline reject CSR - // todo: Add similar check for rf_we a_suppress_csr_xif_illegal_pipeline_illegal : assert property (@(posedge clk) disable iff (!rst_n) (!(id_ex_pipe_i.xif_en && id_ex_pipe_i.xif_meta.accepted) && id_ex_pipe_i.csr_en && csr_illegal_i) && (id_ex_pipe_i.instr_valid && ex_valid_o && wb_ready_i) - |=> !ex_wb_pipe_o.csr_en) - else `uvm_error("ex_stage", "csr_en not suppressed after eXtension interface rejected and pipeline rejected CSR") + |=> !ex_wb_pipe_o.csr_en && !ex_wb_pipe_o.rf_we) + else `uvm_error("ex_stage", "csr_en or rf_we not suppressed after eXtension interface rejected and pipeline rejected CSR") - // csr_en not suppressed for xif reject and pipeline accept CSR - // todo: Add similar check for rf_we - a_suppress_csr_xif_illegal_pipeline_legal : - assert property (@(posedge clk) disable iff (!rst_n) - (!(id_ex_pipe_i.xif_en && id_ex_pipe_i.xif_meta.accepted) && id_ex_pipe_i.csr_en && !csr_illegal_i) && - (id_ex_pipe_i.instr_valid && ex_valid_o && wb_ready_i) - |=> ex_wb_pipe_o.csr_en) - else `uvm_error("ex_stage", "csr_en suppressed after eXtension interface rejected and pipeline accepted CSR") + // csr_en not suppressed for xif reject and pipeline accept CSR + a_suppress_csr_xif_illegal_pipeline_legal : + assert property (@(posedge clk) disable iff (!rst_n) + (!(id_ex_pipe_i.xif_en && id_ex_pipe_i.xif_meta.accepted) && id_ex_pipe_i.csr_en && !csr_illegal_i) && + (id_ex_pipe_i.instr_valid && ex_valid_o && wb_ready_i) + |=> ex_wb_pipe_o.csr_en && ex_wb_pipe_o.rf_we) + else `uvm_error("ex_stage", "csr_en or rf_we suppressed after eXtension interface rejected and pipeline accepted CSR") // First access of split LSU instruction should have rf_we deasserted a_split_rf_we: From 1a4fe0bc0bcfb84ab1dd7db4ccdeb7a61278df67 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 13:56:25 +0200 Subject: [PATCH 06/23] Fix todo in assertion a_valid_jump. Add assertion a_jalr_stable_target. Signed-off-by: Oivind Ekelund --- bhv/cv32e40x_wrapper.sv | 6 +++++- rtl/cv32e40x_controller.sv | 2 ++ rtl/cv32e40x_controller_fsm.sv | 3 ++- rtl/cv32e40x_core.sv | 1 + sva/cv32e40x_controller_fsm_sva.sv | 28 ++++++++++++++++++++++------ 5 files changed, 32 insertions(+), 8 deletions(-) diff --git a/bhv/cv32e40x_wrapper.sv b/bhv/cv32e40x_wrapper.sv index a3c650e2a..7669dc2de 100644 --- a/bhv/cv32e40x_wrapper.sv +++ b/bhv/cv32e40x_wrapper.sv @@ -225,7 +225,8 @@ module cv32e40x_wrapper #(.X_EXT(X_EXT), .DEBUG(DEBUG), .CLIC(CLIC), - .CLIC_ID_WIDTH(CLIC_ID_WIDTH)) + .CLIC_ID_WIDTH(CLIC_ID_WIDTH), + .RV32(RV32)) controller_fsm_sva ( .lsu_outstanding_cnt (core_i.load_store_unit_i.cnt_q), .rf_we_wb_i (core_i.wb_stage_i.rf_we_wb_o ), @@ -244,6 +245,9 @@ module cv32e40x_wrapper .instr_req_o (core_i.instr_req_o), .instr_dbg_o (core_i.instr_dbg_o), .mstatus_i (core_i.cs_registers_i.mstatus_rdata), + .rf_mem_i (core_i.register_file_wrapper_i.register_file_i.mem), + .alu_jmpr_id_i (core_i.alu_jmpr_id), + .jalr_fw_id_i (core_i.id_stage_i.jalr_fw), .*); bind cv32e40x_cs_registers: core_i.cs_registers_i diff --git a/rtl/cv32e40x_controller.sv b/rtl/cv32e40x_controller.sv index 485d74c51..0ead4af56 100644 --- a/rtl/cv32e40x_controller.sv +++ b/rtl/cv32e40x_controller.sv @@ -36,6 +36,7 @@ module cv32e40x_controller import cv32e40x_pkg::*; parameter int unsigned REGFILE_NUM_READ_PORTS = 2, parameter bit CLIC = 0, parameter int unsigned CLIC_ID_WIDTH = 5, + parameter rv32_e RV32 = RV32I, parameter bit DEBUG = 1 ) ( @@ -151,6 +152,7 @@ module cv32e40x_controller import cv32e40x_pkg::*; .X_EXT ( X_EXT ), .CLIC ( CLIC ), .CLIC_ID_WIDTH ( CLIC_ID_WIDTH ), + .RV32 ( RV32 ), .DEBUG ( DEBUG ) ) controller_fsm_i diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv index fb648dc96..8a6503883 100644 --- a/rtl/cv32e40x_controller_fsm.sv +++ b/rtl/cv32e40x_controller_fsm.sv @@ -34,7 +34,8 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; parameter bit X_EXT = 0, parameter bit DEBUG = 1, parameter bit CLIC = 0, - parameter int unsigned CLIC_ID_WIDTH = 5 + parameter int unsigned CLIC_ID_WIDTH = 5, + parameter rv32_e RV32 = RV32I ) ( // Clocks and reset diff --git a/rtl/cv32e40x_core.sv b/rtl/cv32e40x_core.sv index 22e411b01..05181bcad 100644 --- a/rtl/cv32e40x_core.sv +++ b/rtl/cv32e40x_core.sv @@ -896,6 +896,7 @@ module cv32e40x_core import cv32e40x_pkg::*; .REGFILE_NUM_READ_PORTS ( REGFILE_NUM_READ_PORTS ), .CLIC ( CLIC ), .CLIC_ID_WIDTH ( CLIC_ID_WIDTH ), + .RV32 ( RV32 ), .DEBUG ( DEBUG ) ) controller_i diff --git a/sva/cv32e40x_controller_fsm_sva.sv b/sva/cv32e40x_controller_fsm_sva.sv index f9c2c0464..3f54b0fe8 100644 --- a/sva/cv32e40x_controller_fsm_sva.sv +++ b/sva/cv32e40x_controller_fsm_sva.sv @@ -31,7 +31,8 @@ module cv32e40x_controller_fsm_sva #( parameter bit X_EXT = 1'b0, parameter bit DEBUG = 1'b0, parameter bit CLIC = 1'b0, - parameter int unsigned CLIC_ID_WIDTH = 5 + parameter int unsigned CLIC_ID_WIDTH = 5, + parameter rv32_e RV32 = RV32I ) ( input logic clk, @@ -130,7 +131,10 @@ module cv32e40x_controller_fsm_sva input logic dret_in_wb, input logic csr_flush_ack_q, input logic clic_ptr_in_id, - input logic mret_ptr_in_id + input logic mret_ptr_in_id, + input logic alu_jmpr_id_i, + input logic [31:0] jalr_fw_id_i, + input logic [REGFILE_WORD_WIDTH-1:0] rf_mem_i [(RV32 == RV32I) ? 32 : 16] ); @@ -153,15 +157,27 @@ module cv32e40x_controller_fsm_sva jump_taken |=> !jump_taken) else `uvm_error("controller", "Two jumps back-to-back are taken") -/* todo: fix // Check that a jump is taken only when ID is not killed a_valid_jump : assert property (@(posedge clk) jump_taken |-> if_id_pipe_i.instr_valid && !ctrl_fsm_o.kill_id) - else `uvm_error("controller", "Jump taken while ID is halted or killed") -*/ + else `uvm_error("controller", "Jump taken while ID is killed") + + // Check that register used for JALR target calculation is stable from the jump is taken from ID until the JALR retires from WB. + property p_jalr_stable_target; + logic [4:0] jalr_rs_id; + logic [31:0] rf_at_jump_id; + @(posedge clk) disable iff (!rst_n) + ((jump_taken && alu_jmpr_id_i, // When JALR is taken from ID, + rf_at_jump_id = jalr_fw_id_i, // Store (possibly forwarded) RF value used for target calculation + jalr_rs_id = if_id_pipe_i.instr.bus_resp.rdata[19:15]) // Store RS from JALR instruction + ##1 !(ctrl_fsm_o.kill_ex || ctrl_fsm_o.kill_wb) throughout (ex_wb_pipe_i.alu_jmp_qual && wb_valid_i)[->1] // Wait for JALR to retire from WB (while not being killed) + |-> rf_mem_i[jalr_rs_id] == rf_at_jump_id); // Check that RF value is consistent with the value used for jump target calculation + endproperty : p_jalr_stable_target + + a_jalr_stable_target: assert property(p_jalr_stable_target) else `uvm_error("controller", "Assertion a_jalr_stable_target failed"); -// Check that xret does not coincide with CSR write (to avoid using wrong return address) + // Check that xret does not coincide with CSR write (to avoid using wrong return address) // This check is more strict than really needed; a CSR instruction would be allowed in EX as long // as its write action happens before the xret CSR usage property p_xret_csr; From 4965a65b5b1674d1973dad0782cdb34afbf249cd Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 14:44:55 +0200 Subject: [PATCH 07/23] Fix todos. Update a_kill_if and a_kill_id. Signed-off-by: Oivind Ekelund --- sva/cv32e40x_controller_fsm_sva.sv | 34 ++++++++++++++++++++++-------- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/sva/cv32e40x_controller_fsm_sva.sv b/sva/cv32e40x_controller_fsm_sva.sv index f9c2c0464..e3a6f1304 100644 --- a/sva/cv32e40x_controller_fsm_sva.sv +++ b/sva/cv32e40x_controller_fsm_sva.sv @@ -91,6 +91,7 @@ module cv32e40x_controller_fsm_sva input logic first_op_ex_i, input logic last_op_id_i, input logic ex_ready_i, + input logic id_ready_i, input logic sequence_interruptible, input logic sequence_in_progress_wb, input logic id_stage_haltable, @@ -191,20 +192,35 @@ module cv32e40x_controller_fsm_sva else `uvm_error("controller", "Interrupt taken while oustanding transactions are pending") // Ensure .instr_valid is zero following a kill_ - /* TODO:OK:low Failing when bubble is inserted in ID (id_ready_o==0) when WFI is in EX. - Will investigate how to solve. Agreed that this assertion is maybe too strict. We only need to guarantee that if a stage is killed, that the instruction in that stage never reaches the following stage with instr_valid = 1 (it doesn't need instr_valid of the next stage 0 in the following cycle. + + // Support logic to indicate that IF has been killed, and not yet received a new instruction from the prefetcher + logic kill_if_no_prefetch_valid; + always_ff @(posedge clk, negedge rst_n) begin + if(!rst_n) begin + kill_if_no_prefetch_valid <= 1'b0; + end + else begin + if (ctrl_fsm_o.kill_if) begin + kill_if_no_prefetch_valid <= 1'b1; + end + else if (prefetch_valid_if_i) begin + kill_if_no_prefetch_valid <= 1'b0; + end + end + end + + // If IF is killed and ID is ready before a new instruction arrives, if_id_pipe_i.instr_valid must be 0 a_kill_if : assert property (@(posedge clk) disable iff (!rst_n) - (ctrl_fsm_o.kill_if) |=> (if_id_pipe_i.instr_valid == 1'b0) ) - else `uvm_error("controller", "if_id_pipe.instr_valid not zero after kill_if") -*/ -/* TODO:OK:low Failing when a DIV instruction is being executed - Causes ex_ready to be 0. Will be fixed then divider is interruptable + kill_if_no_prefetch_valid && $past(id_ready_i) |-> (if_id_pipe_i.instr_valid == 1'b0) ) + else `uvm_error("controller", "if_id_pipe_i.instr_valid not zero after kill_if") + + // If ID is killed, id_ex_pipe_i.instr_valid must be 0 following the next ex_ready_i a_kill_id : assert property (@(posedge clk) disable iff (!rst_n) - (ctrl_fsm_o.kill_id) |=> (id_ex_pipe_i.instr_valid == 1'b0) ) + ctrl_fsm_o.kill_id ##0 ex_ready_i[->1] |=> (id_ex_pipe_i.instr_valid == 1'b0) ) else `uvm_error("controller", "id_ex_pipe.instr_valid not zero after kill_id") -*/ + a_kill_ex : assert property (@(posedge clk) disable iff (!rst_n) (ctrl_fsm_o.kill_ex && !ctrl_fsm_o.halt_wb) |=> (ex_wb_pipe_i.instr_valid == 1'b0) ) From c20ae8ee2729326dc05c7f731b975231ffda22d8 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 15:12:48 +0200 Subject: [PATCH 08/23] Tag todo with xif Signed-off-by: Oivind Ekelund --- sva/cv32e40x_controller_fsm_sva.sv | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/sva/cv32e40x_controller_fsm_sva.sv b/sva/cv32e40x_controller_fsm_sva.sv index e3a6f1304..a82c95c29 100644 --- a/sva/cv32e40x_controller_fsm_sva.sv +++ b/sva/cv32e40x_controller_fsm_sva.sv @@ -364,8 +364,8 @@ generate; // Assert that a CSR instruction that is accepted by both eXtension interface and pipeline // causes an illegal instruction - // TODO: The checks for mpu_status and bus_resp.err below can be removed once the - // xif offload is fully implemented (no offload if mpu or bus error occured in IF) + // todo:xif The checks for mpu_status and bus_resp.err below can be removed once the + // xif offload is fully implemented (no offload if mpu or bus error occured in IF) a_duplicate_csr_illegal: assert property (@(posedge clk) disable iff (!rst_n) ex_valid_i && wb_ready_i && (id_ex_pipe_i.xif_en && id_ex_pipe_i.xif_meta.accepted) && id_ex_pipe_i.csr_en && !csr_illegal_i && From cd6e6d5c2b99eb1569e37b1bfae578fa3aa24b52 Mon Sep 17 00:00:00 2001 From: Oystein Knauserud Date: Thu, 31 Aug 2023 15:30:37 +0200 Subject: [PATCH 09/23] Updates for CLIC spec (august 23): mcause.minhv only set when taking an exception for a CLIC pointer or mret pointer restart. When jumping due to an mret, mcause.minhv is checked regardless of mcause.mpp. Signed-off-by: Oystein Knauserud --- rtl/cv32e40x_controller_fsm.sv | 36 +++++++++------------------ rtl/cv32e40x_cs_registers.sv | 23 +---------------- rtl/include/cv32e40x_pkg.sv | 1 - sva/cv32e40x_controller_fsm_sva.sv | 1 - sva/cv32e40x_cs_registers_sva.sv | 40 ++++++++++++++---------------- 5 files changed, 32 insertions(+), 69 deletions(-) diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv index fb648dc96..39ea4b619 100644 --- a/rtl/cv32e40x_controller_fsm.sv +++ b/rtl/cv32e40x_controller_fsm.sv @@ -681,8 +681,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.csr_save_cause = 1'b0; ctrl_fsm_o.csr_cause = 32'h0; - ctrl_fsm_o.csr_clear_minhv = 1'b0; - pipe_pc_mux_ctrl = PC_WB; exc_cause = 11'b0; @@ -745,8 +743,8 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.csr_cause.irq = 1'b1; ctrl_fsm_o.csr_cause.exception_code = nmi_is_store_q ? INT_CAUSE_LSU_STORE_FAULT : INT_CAUSE_LSU_LOAD_FAULT; - // Keep mcause.minhv when taking exceptions and interrupts, only cleared on successful pointer fetches or CSR writes. - ctrl_fsm_o.csr_cause.minhv = mcause_i.minhv; + // Clear mcause.minhv when taking an NMI (only set when taking exceptions on CLIC/mret pointers) + ctrl_fsm_o.csr_cause.minhv = 1'b0; if (CLIC) begin // Keep current interrupt level when taking NMIs @@ -796,9 +794,8 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.csr_save_cause = 1'b1; ctrl_fsm_o.csr_cause.irq = 1'b1; - // Default to keeping mcause.minhv. It will only be set to 1 when taking a CLIC SHV interrupt (or by a CSR write). - // For all other cases it keeps its value. - ctrl_fsm_o.csr_cause.minhv = mcause_i.minhv; + // Clear mcause.minhv when taking an interrupt. (only set when taking exceptions on CLIC/mret pointers) + ctrl_fsm_o.csr_cause.minhv = 1'b0; if (CLIC) begin @@ -810,9 +807,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.pc_mux = PC_TRAP_CLICV; clic_ptr_in_progress_id_set = 1'b1; ctrl_fsm_o.pc_set_clicv = 1'b1; - // When taking an SHV interrupt, always set minhv. - // Mcause.minhv will only be cleared when a successful pointer fetch is done, or when it is cleared by a CSR write. - ctrl_fsm_o.csr_cause.minhv = 1'b1; end else begin ctrl_fsm_o.pc_mux = PC_TRAP_IRQ; end @@ -864,8 +858,8 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.csr_save_cause = !debug_mode_q; // Do not update CSRs if in debug mode ctrl_fsm_o.csr_cause.exception_code = exception_cause_wb; - // Keep mcause.minhv when taking exceptions and interrupts, only cleared on successful pointer fetches or CSR writes. - ctrl_fsm_o.csr_cause.minhv = mcause_i.minhv; + // Set mcause.minhv if exception is for a CLIC or mret pointer. Otherwise clear it + ctrl_fsm_o.csr_cause.minhv = (ex_wb_pipe_i.instr_meta.clic_ptr || ex_wb_pipe_i.instr_meta.mret_ptr); // Special insn end else if (wfi_in_wb || wfe_in_wb) begin @@ -987,14 +981,13 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.kill_if = 1'b1; if (sys_mret_id) begin - // If the xcause.minhv bit is set for the previous privilege level (mcause.mpp) when an mret is in ID, - // the mret should restart the CLIC pointer fetch using mepc as a pointer to the pointer instead of jumping to - // the address in mepc. If mpp==PRIV_LVL_U, the (not existing) ucause.uinhv bit is assumed to be 0. + // If the mcause.minhv bit is set when an mret is in ID, the mret should restart the CLIC pointer fetch using mepc as + // a pointer to the pointer instead of jumping to the address in mepc. // This is done below by signalling pc_set_clicv along with pc_mux=PC_MRET. This will - // treat the mepc as an address to a CLIC pointer. The minhv flag will only be cleared - // when a pointer reaches the WB stage with no faults from fetching. - // ID stage is halted while it contains an mret and at the same time there are CSR writes (including CLIC pointers) EX or WB, hence it is safe to use mcause here. - if (mcause_i.minhv && (mcause_i.mpp == PRIV_LVL_M)) begin + // treat the mepc as an address to a CLIC pointer. The minhv flag will only be set when an exception is taken on a + // CLIC or mret pointer, and cleared when a trap for any other cause except debug is taken. It is also writeable by SW. + // ID stage is halted while it contains an mret and at the same time there are CSR writes (including CLIC pointers) in EX or WB, hence it is safe to use mcause here. + if (mcause_i.minhv) begin // mcause.minhv set, exception occured during last pointer fetch (or SW wrote it) // Do another pointer fetch from the address stored in mepc. ctrl_fsm_o.pc_set = 1'b1; @@ -1063,11 +1056,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.csr_restore_mret_ptr = !debug_mode_q; end - // CLIC pointer in WB - if (clic_ptr_in_wb && !ctrl_fsm_o.kill_wb && !ctrl_fsm_o.halt_wb && !exception_in_wb) begin - // Clear minhv if no exceptions are associated with the pointer - ctrl_fsm_o.csr_clear_minhv = 1'b1; - end end // !debug or interrupts // Single step debug entry or etrigger debug entry diff --git a/rtl/cv32e40x_cs_registers.sv b/rtl/cv32e40x_cs_registers.sv index 16e4cf22a..b54771287 100644 --- a/rtl/cv32e40x_cs_registers.sv +++ b/rtl/cv32e40x_cs_registers.sv @@ -1024,7 +1024,7 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; cause : ctrl_fsm_i.debug_cause, default : 'd0 }; -dcsr_we = 1'b1; + dcsr_we = 1'b1; dpc_n = ctrl_fsm_i.pipe_pc; dpc_we = 1'b1; @@ -1106,11 +1106,6 @@ dcsr_we = 1'b1; mintthresh_n = 32'h00000000; mintthresh_we = 1'b1; end - - if (ctrl_fsm_i.csr_restore_mret_ptr) begin - // Clear mcause.minhv if the mret also caused a successful CLIC pointer fetch - mcause_n.minhv = 1'b0; - end end end //ctrl_fsm_i.csr_restore_mret @@ -1134,22 +1129,6 @@ dcsr_we = 1'b1; end //ctrl_fsm_i.csr_restore_dret - // Clear mcause.minhv on successful CLIC pointer fetches - // This only happens for CLIC pointer that did not originate from an mret. - // In the case of mret restarting CLIC pointer fetches, minhv is cleared while - // ctrl_fsm_i.csr_restore_mret_ptr is asserted. - ctrl_fsm_i.csr_clear_minhv: begin - if (CLIC) begin - // Keep mcause values, only clear minhv bit. - mcause_n = mcause_rdata; - mcause_n.minhv = 1'b0; - mcause_we = 1'b1; - - // Not really needed, but allows for asserting mstatus_we == mcause_we to check aliasing formally - mstatus_n = mstatus_rdata; - mstatus_we = 1'b1; - end - end default:; endcase diff --git a/rtl/include/cv32e40x_pkg.sv b/rtl/include/cv32e40x_pkg.sv index 65b61eb02..1f5c93947 100644 --- a/rtl/include/cv32e40x_pkg.sv +++ b/rtl/include/cv32e40x_pkg.sv @@ -1370,7 +1370,6 @@ typedef struct packed { logic csr_restore_mret_ptr; // Restore CSR due to mret followed by CLIC logic csr_restore_dret; // Restore CSR due to dret logic csr_save_cause; // Update CSRs - logic csr_clear_minhv; // Clear the mcause.minhv field logic pending_nmi; // An NMI is pending (for dcsr.nmip) // Performance counter events diff --git a/sva/cv32e40x_controller_fsm_sva.sv b/sva/cv32e40x_controller_fsm_sva.sv index f9c2c0464..fcbf9bc06 100644 --- a/sva/cv32e40x_controller_fsm_sva.sv +++ b/sva/cv32e40x_controller_fsm_sva.sv @@ -658,7 +658,6 @@ end else begin // CLIC |-> (clic_ptr_in_progress_id_set != 1'b1) && !ctrl_fsm_o.csr_cause.minhv && - !ctrl_fsm_o.csr_clear_minhv && !mcause_i.minhv && !if_id_pipe_i.instr_meta.clic_ptr && !id_ex_pipe_i.instr_meta.clic_ptr && diff --git a/sva/cv32e40x_cs_registers_sva.sv b/sva/cv32e40x_cs_registers_sva.sv index 02e173513..dcc5b32e0 100644 --- a/sva/cv32e40x_cs_registers_sva.sv +++ b/sva/cv32e40x_cs_registers_sva.sv @@ -163,6 +163,25 @@ module cv32e40x_cs_registers_sva a_mcause_mstatus_alias: assert property(p_mcause_mstatus_alias) else `uvm_error("cs_registers", "mcause.mpp and mcause.mpie not aliased correctly") + // Whenever mepc is written by HW, mcause.minhv must also be written with the correct value. + // mcause.minhv is only set when an exception is taken on a CLIC or mret pointer + // SW can still write both mepc and mcause independently + property p_mepc_minhv_write; + @(posedge clk) disable iff (!rst_n) + ( + mepc_we // mepc is written + |-> + (mcause_we && // mcause is written + mcause_n.minhv == ((ex_wb_pipe_i.instr_meta.clic_ptr || ex_wb_pipe_i.instr_meta.mret_ptr) && // pointer in WB + (ctrl_fsm_i.pc_set && ctrl_fsm_i.pc_mux == PC_TRAP_EXC))) // exception taken + or + csr_we_int // SW writes mepc + ); + endproperty; + + a_mepc_minhv_write: assert property(p_mepc_minhv_write) + else `uvm_error("cs_registers", "mcause.minhv not updated correctly on mepc write.") + end // Check that no csr instruction can be in WB during sleep when ctrl_fsm.halt_limited_wb is set @@ -174,27 +193,6 @@ module cv32e40x_cs_registers_sva a_halt_limited_wb: assert property(p_halt_limited_wb) else `uvm_error("cs_registers", "CSR in WB while halt_limited_wb is set"); - - // Check csr_clear_minhv cannot happen at the same time as csr_save_cause or csr_restore_dret (would cause mcause_we conflict) - sequence seq_csr_clear_minhv; - ctrl_fsm_i.csr_clear_minhv; - endsequence - - property p_minhv_unique; - @(posedge clk) disable iff (!rst_n) - ( seq_csr_clear_minhv |-> !(ctrl_fsm_i.csr_save_cause || ctrl_fsm_i.csr_restore_dret)); - endproperty; - - if (CLIC) begin - a_minhv_unique: assert property(p_minhv_unique) - else `uvm_error("cs_registers", "csr_save_cause at the same time as csr_clear_minhv."); - - end else begin - a_minhv_unique_nocover: assert property( - @(posedge clk) disable iff (!rst_n) - not seq_csr_clear_minhv); - end - ///////////////////////////////////////////////////////////////////////////////////////// // Asserts to check that the CSR flops remain unchanged if a set/clear has all_zero rs1 ///////////////////////////////////////////////////////////////////////////////////////// From eb2074dae2d7a406e87c7fa2f7001956ebf9dd74 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Thu, 31 Aug 2023 16:55:41 +0200 Subject: [PATCH 10/23] Clean up truncation warnings in SVA Signed-off-by: Oivind Ekelund --- bhv/cv32e40x_rvfi_data_obi.sv | 2 +- sva/cv32e40x_rvfi_sva.sv | 41 +++++++++++++++++++++-------------- 2 files changed, 26 insertions(+), 17 deletions(-) diff --git a/bhv/cv32e40x_rvfi_data_obi.sv b/bhv/cv32e40x_rvfi_data_obi.sv index 718173ef4..94cbd9197 100644 --- a/bhv/cv32e40x_rvfi_data_obi.sv +++ b/bhv/cv32e40x_rvfi_data_obi.sv @@ -46,7 +46,7 @@ module cv32e40x_rvfi_data_obi import cv32e40x_pkg::*; import cv32e40x_rvfi_pkg:: lsu_data_trans_o = buffer_trans_i; // Align Memory write data - lsu_data_trans_o.wdata = buffer_trans_wdata_ror; + lsu_data_trans_o.wdata = buffer_trans_wdata_ror[31:0]; end endmodule diff --git a/sva/cv32e40x_rvfi_sva.sv b/sva/cv32e40x_rvfi_sva.sv index d09daaf45..0d2554cea 100644 --- a/sva/cv32e40x_rvfi_sva.sv +++ b/sva/cv32e40x_rvfi_sva.sv @@ -437,6 +437,8 @@ end */ + // The following assertions and support logic check that memory transfers reported on rvfi_mem are consistent with LSU OBI transfers + localparam int unsigned OBI_FIFO_SIZE = 32; // FIFO needs to be able to hold at least 2*13 memory transfers (because Zc can cause 13 transfers, and these can be split misaligned) localparam int unsigned MAX_NUM_MEMOP = 13; // This must be set to the maximum number of memory operations per retired instruction. If set too high it will result in unreachable covers @@ -455,9 +457,9 @@ end } rvfi_mem_t; // Return number of memory operations based on rvfi_mem_rmaks/wmask - function automatic int unsigned get_num_memop(bit [4*NMEM-1:0] rvfi_mem_mask); + function automatic bit [$clog2(NMEM)-1:0] get_num_memop(bit [4*NMEM-1:0] rvfi_mem_mask); - int unsigned num_memop = 0; + bit [$clog2(NMEM)-1:0] num_memop = 0; for (int i=0; i num_memop <= MAX_NUM_MEMOP) + else `uvm_error("rvfi", "Memory operations > MAX_NUM_MEMOP. Potential overflow in SVA support logic.") + genvar i_memop; generate @@ -630,7 +639,7 @@ end bit [31:0] split_2nd_wdata; bit [31:0] split_1st_rdata; bit [31:0] split_2nd_rdata; - bit [1:0] split_2nd_shift; + bit [2:0] split_2nd_shift; bit [$clog2(OBI_FIFO_SIZE)-1:0] rd_ptr_memop, rd_ptr_memop_inc; @@ -662,10 +671,10 @@ end if(split_transfer) begin // Split misaligned transfer(s) - rd_ptr_memop = rd_ptr + 2*i_memop; // Split transfers are reported in one memory operation on rvfi_mem, but results in 2 OBI transfers. - rd_ptr_memop_inc = rd_ptr_memop + 1; + rd_ptr_memop = rd_ptr + ($clog2(OBI_FIFO_SIZE))'(2*i_memop); // Split transfers are reported in one memory operation on rvfi_mem, but results in 2 OBI transfers. + rd_ptr_memop_inc = rd_ptr_memop + 1'b1; - split_2nd_shift = 4 - data_obi_req_fifo[rd_ptr_memop].addr[1:0]; + split_2nd_shift = 3'h4 - data_obi_req_fifo[rd_ptr_memop].addr[1:0]; exp_rvfi_mem_mask = (data_obi_req_fifo[rd_ptr_memop].be >> data_obi_req_fifo[rd_ptr_memop].addr[1:0]) | (data_obi_req_fifo[rd_ptr_memop_inc].be << split_2nd_shift); @@ -686,7 +695,7 @@ end end else begin - rd_ptr_memop = rd_ptr + i_memop; + rd_ptr_memop = rd_ptr + ($clog2(OBI_FIFO_SIZE))'(i_memop); exp_rvfi_mem_mask = data_obi_req_fifo[rd_ptr_memop].be >> data_obi_req_fifo[rd_ptr_memop].addr[1:0]; From 75b048d46d105889fe697f1dee15814d8c0a9b17 Mon Sep 17 00:00:00 2001 From: Oystein Knauserud Date: Tue, 5 Sep 2023 10:42:15 +0200 Subject: [PATCH 11/23] Added 'unused_signals' to controller_fsm and added clic_ptr_in_wb to its fan-in. The signal clic_ptr_in_wb is used by RVFI but not by the controller. Signed-off-by: Oystein Knauserud --- rtl/cv32e40x_controller_fsm.sv | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv index 39ea4b619..28201cbae 100644 --- a/rtl/cv32e40x_controller_fsm.sv +++ b/rtl/cv32e40x_controller_fsm.sv @@ -262,6 +262,9 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; logic clic_ptr_in_progress_id_set; logic clic_ptr_in_progress_id_clear; + // Signal for or'ing int signals not used by the RTL but are used by RVFI + logic unused_signals; + assign sequence_interruptible = !sequence_in_progress_wb; assign id_stage_haltable = !(sequence_in_progress_id || clic_ptr_in_progress_id); @@ -1453,6 +1456,9 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; assign ctrl_fsm_o.debug_running = debug_fsm_cs[RUNNING_INDEX]; assign ctrl_fsm_o.debug_halted = debug_fsm_cs[HALTED_INDEX]; + // Tie off unused signals + assign unused_signals = clic_ptr_in_wb; + //--------------------------------------------------------------------------- // eXtension interface From 518b590b2666efb6dc24f7a840f702d07dff3db5 Mon Sep 17 00:00:00 2001 From: Halfdan Bechmann Dolva Date: Tue, 5 Sep 2023 13:27:01 +0200 Subject: [PATCH 12/23] Remove mscratchcsw register as it is meant for priv mode change Signed-off-by: Halfdan Bechmann Dolva --- docs/user_manual/source/control_status_registers.rst | 2 -- 1 file changed, 2 deletions(-) diff --git a/docs/user_manual/source/control_status_registers.rst b/docs/user_manual/source/control_status_registers.rst index 25f95f7a2..b544f2341 100644 --- a/docs/user_manual/source/control_status_registers.rst +++ b/docs/user_manual/source/control_status_registers.rst @@ -80,8 +80,6 @@ instruction exception. +---------------+-------------------+-----------+--------------------------+---------------------------------------------------------+ | 0x347 | ``mintthresh`` | MRW | ``CLIC`` = 1 | Interrupt-level threshold | +---------------+-------------------+-----------+--------------------------+---------------------------------------------------------+ - | 0x348 | ``mscratchcsw`` | MRW | ``CLIC`` = 1 | Conditional scratch swap on priv mode change | - +---------------+-------------------+-----------+--------------------------+---------------------------------------------------------+ | 0x349 | ``mscratchcswl`` | MRW | ``CLIC`` = 1 | Conditional scratch swap on level change | +---------------+-------------------+-----------+--------------------------+---------------------------------------------------------+ | 0x7A0 | ``tselect`` | MRW | ``DBG_NUM_TRIGGERS`` > 0 | Trigger Select Register | From f5280953140505851820cb745496afc278d5d8be Mon Sep 17 00:00:00 2001 From: Oystein Knauserud Date: Tue, 5 Sep 2023 13:49:53 +0200 Subject: [PATCH 13/23] Changes after review. Added assert for checking that mepc is always written when mcause.minhv is changed. Refactored some code in controller_fsm. SEC clean. Signed-off-by: Oystein Knauserud --- rtl/cv32e40x_controller_fsm.sv | 15 ++++++--------- sva/cv32e40x_cs_registers_sva.sv | 18 +++++++++++++++++- 2 files changed, 23 insertions(+), 10 deletions(-) diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv index 28201cbae..f632fb8b9 100644 --- a/rtl/cv32e40x_controller_fsm.sv +++ b/rtl/cv32e40x_controller_fsm.sv @@ -166,6 +166,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; logic branch_taken_n; logic branch_taken_q; + logic clic_ptr_in_ex; // WB signals logic exception_in_wb; @@ -262,9 +263,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; logic clic_ptr_in_progress_id_set; logic clic_ptr_in_progress_id_clear; - // Signal for or'ing int signals not used by the RTL but are used by RVFI - logic unused_signals; - assign sequence_interruptible = !sequence_in_progress_wb; assign id_stage_haltable = !(sequence_in_progress_id || clic_ptr_in_progress_id); @@ -410,6 +408,9 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // An offloaded instruction is in WB assign xif_in_wb = (ex_wb_pipe_i.xif_en && ex_wb_pipe_i.instr_valid); + // Regular CLIC pointer in EX (not caused by mret) + assign clic_ptr_in_ex = id_ex_pipe_i.instr_meta.clic_ptr && id_ex_pipe_i.instr_valid; + // Regular CLIC pointer in WB (not caused by mret) assign clic_ptr_in_wb = ex_wb_pipe_i.instr_meta.clic_ptr && ex_wb_pipe_i.instr_valid; @@ -471,9 +472,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; if (CLIC) begin : gen_clic_pointer_flag // A CLIC pointer may be in the pipeline from the moment we start fetching (clic_ptr_in_progress_id == 1) // or while a pointer is in the EX or WB stages. - assign clic_ptr_in_pipeline = (id_ex_pipe_i.instr_valid && id_ex_pipe_i.instr_meta.clic_ptr) || - (ex_wb_pipe_i.instr_valid && ex_wb_pipe_i.instr_meta.clic_ptr) || - clic_ptr_in_progress_id; + assign clic_ptr_in_pipeline = clic_ptr_in_ex || clic_ptr_in_wb || clic_ptr_in_progress_id; end else begin : gen_basic_pointer_flag assign clic_ptr_in_pipeline = 1'b0; end @@ -862,7 +861,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.csr_cause.exception_code = exception_cause_wb; // Set mcause.minhv if exception is for a CLIC or mret pointer. Otherwise clear it - ctrl_fsm_o.csr_cause.minhv = (ex_wb_pipe_i.instr_meta.clic_ptr || ex_wb_pipe_i.instr_meta.mret_ptr); + ctrl_fsm_o.csr_cause.minhv = clic_ptr_in_wb || mret_ptr_in_wb; // Special insn end else if (wfi_in_wb || wfe_in_wb) begin @@ -1456,8 +1455,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; assign ctrl_fsm_o.debug_running = debug_fsm_cs[RUNNING_INDEX]; assign ctrl_fsm_o.debug_halted = debug_fsm_cs[HALTED_INDEX]; - // Tie off unused signals - assign unused_signals = clic_ptr_in_wb; //--------------------------------------------------------------------------- diff --git a/sva/cv32e40x_cs_registers_sva.sv b/sva/cv32e40x_cs_registers_sva.sv index dcc5b32e0..0f4c78b22 100644 --- a/sva/cv32e40x_cs_registers_sva.sv +++ b/sva/cv32e40x_cs_registers_sva.sv @@ -172,7 +172,7 @@ module cv32e40x_cs_registers_sva mepc_we // mepc is written |-> (mcause_we && // mcause is written - mcause_n.minhv == ((ex_wb_pipe_i.instr_meta.clic_ptr || ex_wb_pipe_i.instr_meta.mret_ptr) && // pointer in WB + mcause_n.minhv == ((ex_wb_pipe_i.instr_valid && (ex_wb_pipe_i.instr_meta.clic_ptr || ex_wb_pipe_i.instr_meta.mret_ptr)) && // pointer in WB (ctrl_fsm_i.pc_set && ctrl_fsm_i.pc_mux == PC_TRAP_EXC))) // exception taken or csr_we_int // SW writes mepc @@ -182,6 +182,22 @@ module cv32e40x_cs_registers_sva a_mepc_minhv_write: assert property(p_mepc_minhv_write) else `uvm_error("cs_registers", "mcause.minhv not updated correctly on mepc write.") + // Whenever mcause.minhv is changed mepc should also be written (or SW writes to mcause.minhv) + property p_minhv_mepc_write; + @(posedge clk) disable iff (!rst_n) + ( + mcause_we && + (mcause_n.minhv != mcause_q.minhv) + |-> + mepc_we + or + csr_we_int + ); + endproperty; + + a_minhv_mepc_write: assert property(p_minhv_mepc_write) + else `uvm_error("cs_registers", "mcause written without mepc written") + end // Check that no csr instruction can be in WB during sleep when ctrl_fsm.halt_limited_wb is set From 9d71878abd6683ee38f8dc929952982c2a0b949d Mon Sep 17 00:00:00 2001 From: Arjan Bink <40633348+Silabs-ArjanB@users.noreply.github.com> Date: Tue, 5 Sep 2023 15:02:59 +0200 Subject: [PATCH 14/23] Update cv32e40x_controller_fsm.sv --- rtl/cv32e40x_controller_fsm.sv | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv index f632fb8b9..81ca261bf 100644 --- a/rtl/cv32e40x_controller_fsm.sv +++ b/rtl/cv32e40x_controller_fsm.sv @@ -75,7 +75,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; input align_status_e align_status_wb_i, // Aligned status (atomics) in WB input logic [31:0] wpt_match_wb_i, // LSU watchpoint trigger (WB) - // From LSU (WB) input logic data_stall_wb_i, // WB stalled by LSU input logic lsu_valid_wb_i, // LSU instruction in WB is valid @@ -282,8 +281,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // index 0 for non-vectored CLINT mode and CLIC mode, 0xF for vectored CLINT mode assign ctrl_fsm_o.nmi_mtvec_index = (mtvec_mode_i == 2'b01) ? 5'hF : 5'h0; - - //////////////////////////////////////////////////////////////////// // ID stage @@ -292,8 +289,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // Using the ID stage local instr_valid would bring halt_id and kill_id into the equation // causing a path from data_rvalid to instr_addr_o/instr_req_o/instr_memtype_o via pc_set. - - assign sys_mret_id = sys_en_id_i && sys_mret_id_i && if_id_pipe_i.instr_valid; assign jmp_id = alu_en_id_i && alu_jmp_id_i && if_id_pipe_i.instr_valid; @@ -429,7 +424,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // This CSR bit shall not be gated by debug mode or step without stepie assign ctrl_fsm_o.pending_nmi = nmi_pending_q; - // Debug // + // Debug // Single step will need to finish insn in WB, including LSU // LSU will now set valid_1_o only for second part of misaligned instructions. @@ -465,7 +460,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // The signal pending_single_step should never be used outside of the FUNCTIONAL state. assign pending_single_step = (!debug_mode_q && dcsr_i.step && ((wb_valid_i && (last_op_wb_i || abort_op_wb_i)) || non_shv_irq_ack || (pending_nmi && nmi_allowed))); - // Detect if there is a live CLIC pointer in the pipeline // This should block debug and interrupts generate @@ -753,7 +747,6 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.irq_level = mintstatus_i.mil; end - // Save pc from oldest valid instruction if (ex_wb_pipe_i.instr_valid) begin pipe_pc_mux_ctrl = PC_WB; @@ -796,10 +789,9 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; ctrl_fsm_o.csr_save_cause = 1'b1; ctrl_fsm_o.csr_cause.irq = 1'b1; - // Clear mcause.minhv when taking an interrupt. (only set when taking exceptions on CLIC/mret pointers) + // Clear mcause.minhv when taking an interrupt (only set when taking exceptions on CLIC/mret pointers) ctrl_fsm_o.csr_cause.minhv = 1'b0; - if (CLIC) begin ctrl_fsm_o.csr_cause.exception_code = {1'b0, irq_id_ctrl_i}; ctrl_fsm_o.irq_level = irq_clic_level_i; From 32857d984f02796123f2c296289300e994d4a252 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Tue, 5 Sep 2023 16:05:22 +0200 Subject: [PATCH 15/23] Add missing parenthesis in property p_jalr_stable_target Signed-off-by: Oivind Ekelund --- sva/cv32e40x_controller_fsm_sva.sv | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/sva/cv32e40x_controller_fsm_sva.sv b/sva/cv32e40x_controller_fsm_sva.sv index 5123c4367..dd4e444f3 100644 --- a/sva/cv32e40x_controller_fsm_sva.sv +++ b/sva/cv32e40x_controller_fsm_sva.sv @@ -169,11 +169,11 @@ module cv32e40x_controller_fsm_sva logic [4:0] jalr_rs_id; logic [31:0] rf_at_jump_id; @(posedge clk) disable iff (!rst_n) - ((jump_taken && alu_jmpr_id_i, // When JALR is taken from ID, - rf_at_jump_id = jalr_fw_id_i, // Store (possibly forwarded) RF value used for target calculation - jalr_rs_id = if_id_pipe_i.instr.bus_resp.rdata[19:15]) // Store RS from JALR instruction - ##1 !(ctrl_fsm_o.kill_ex || ctrl_fsm_o.kill_wb) throughout (ex_wb_pipe_i.alu_jmp_qual && wb_valid_i)[->1] // Wait for JALR to retire from WB (while not being killed) - |-> rf_mem_i[jalr_rs_id] == rf_at_jump_id); // Check that RF value is consistent with the value used for jump target calculation + ((jump_taken && alu_jmpr_id_i, // When JALR is taken from ID, + rf_at_jump_id = jalr_fw_id_i, // Store (possibly forwarded) RF value used for target calculation + jalr_rs_id = if_id_pipe_i.instr.bus_resp.rdata[19:15]) // Store RS from JALR instruction + ##1 (!(ctrl_fsm_o.kill_ex || ctrl_fsm_o.kill_wb) throughout (ex_wb_pipe_i.alu_jmp_qual && wb_valid_i)[->1]) // Wait for JALR to retire from WB (while not being killed) + |-> rf_mem_i[jalr_rs_id] == rf_at_jump_id); // Check that RF value is consistent with the value used for jump target calculation endproperty : p_jalr_stable_target a_jalr_stable_target: assert property(p_jalr_stable_target) else `uvm_error("controller", "Assertion a_jalr_stable_target failed"); From 103ab2ccad93de048a0e732e9c6503a7744c2057 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Wed, 6 Sep 2023 08:09:37 +0200 Subject: [PATCH 16/23] Fix todo in cv32e40x_core_log Signed-off-by: Oivind Ekelund --- bhv/cv32e40x_core_log.sv | 54 +++++++++++++++++++++++++++++++++++++--- bhv/cv32e40x_wrapper.sv | 23 +++++++++++++++-- 2 files changed, 71 insertions(+), 6 deletions(-) diff --git a/bhv/cv32e40x_core_log.sv b/bhv/cv32e40x_core_log.sv index 74137cd61..4c4de056c 100644 --- a/bhv/cv32e40x_core_log.sv +++ b/bhv/cv32e40x_core_log.sv @@ -38,9 +38,28 @@ module cv32e40x_core_log import cv32e40x_pkg::*; #( -// todo: log all parameters - parameter int unsigned NUM_MHPMCOUNTERS = 1, - parameter bit ENABLE = 1 + parameter bit ENABLE = 1, + parameter rv32_e RV32 = RV32I, + parameter a_ext_e A_EXT = A_NONE, + parameter b_ext_e B_EXT = B_NONE, + parameter m_ext_e M_EXT = M, + parameter bit DEBUG = 1, + parameter logic [31:0] DM_REGION_START = 32'hF0000000, + parameter logic [31:0] DM_REGION_END = 32'hF0003FFF, + parameter int DBG_NUM_TRIGGERS = 1, + parameter int PMA_NUM_REGIONS = 0, + parameter pma_cfg_t PMA_CFG[PMA_NUM_REGIONS-1:0] = '{default:PMA_R_DEFAULT}, + parameter bit CLIC = 0, + parameter int unsigned CLIC_ID_WIDTH = 5, + parameter bit X_EXT = 0, + parameter int unsigned X_NUM_RS = 2, + parameter int unsigned X_ID_WIDTH = 4, + parameter int unsigned X_MEM_WIDTH = 32, + parameter int unsigned X_RFR_WIDTH = 32, + parameter int unsigned X_RFW_WIDTH = 32, + parameter logic [31:0] X_MISA = 32'h00000000, + parameter logic [1:0] X_ECS_XS = 2'b00, + parameter int unsigned NUM_MHPMCOUNTERS = 1 ) ( input logic clk_i, @@ -55,7 +74,34 @@ module cv32e40x_core_log import cv32e40x_pkg::*; // Log top level parameter values initial begin - $display("[cv32e40x_core]: NUM_MHPMCOUNTERS %d", NUM_MHPMCOUNTERS); + $display("[cv32e40x_core]: RV32 = %s", RV32.name() ); + $display("[cv32e40x_core]: A_EXT = %s", A_EXT.name() ); + $display("[cv32e40x_core]: B_EXT = %s", B_EXT.name() ); + $display("[cv32e40x_core]: M_EXT = %s", M_EXT.name() ); + $display("[cv32e40x_core]: DEBUG = %-1d", DEBUG ); + $display("[cv32e40x_core]: DM_REGION_START = 0x%8h", DM_REGION_START ); + $display("[cv32e40x_core]: DM_REGION_END = 0x%8h", DM_REGION_END ); + $display("[cv32e40x_core]: DBG_NUM_TRIGGERS = %-1d", DBG_NUM_TRIGGERS); + $display("[cv32e40x_core]: PMA_NUM_REGIONS = %-2d", PMA_NUM_REGIONS ); + for (int i_pma=0; i_pma Date: Wed, 6 Sep 2023 08:13:48 +0200 Subject: [PATCH 17/23] Fix todo in cv32e40x_wrapper. Probe lsu_exokay_wb from the core side of the LSU. Signed-off-by: Oivind Ekelund --- bhv/cv32e40x_wrapper.sv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bhv/cv32e40x_wrapper.sv b/bhv/cv32e40x_wrapper.sv index 022ba6c3c..795f5a890 100644 --- a/bhv/cv32e40x_wrapper.sv +++ b/bhv/cv32e40x_wrapper.sv @@ -369,7 +369,7 @@ module cv32e40x_wrapper .mie_we (core_i.cs_registers_i.mie_we), .lsu_exception_wb (core_i.wb_stage_i.lsu_exception), .lsu_wpt_match_wb (core_i.wb_stage_i.lsu_wpt_match), - .lsu_exokay_wb (core_i.data_exokay_i), // todo: Could poke into LSU, but this signal is fed directly through the LSU + .lsu_exokay_wb (core_i.load_store_unit_i.resp.bus_resp.exokay), .prefetch_is_mret_ptr_i (core_i.if_stage_i.prefetch_is_mret_ptr), .first_op_if (core_i.if_stage_i.first_op), .xif_compressed_valid (core_i.xif_compressed_if.compressed_valid), From 6b4f596ea6e16518e34456d9f24e930c471b0f32 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Wed, 6 Sep 2023 08:14:54 +0200 Subject: [PATCH 18/23] Fix todo in cv32e40x_wrapper. Complete cv32e40x_rvfi signal connections. Signed-off-by: Oivind Ekelund --- bhv/cv32e40x_wrapper.sv | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/bhv/cv32e40x_wrapper.sv b/bhv/cv32e40x_wrapper.sv index 795f5a890..01a66be52 100644 --- a/bhv/cv32e40x_wrapper.sv +++ b/bhv/cv32e40x_wrapper.sv @@ -739,14 +739,15 @@ endgenerate .csr_marchid_i ( core_i.cs_registers_i.marchid_rdata ), .csr_mhartid_i ( core_i.cs_registers_i.mhartid_rdata ), .csr_mimpid_i ( core_i.cs_registers_i.mimpid_rdata ), - // TODO Tie relevant signals below to RTL .csr_mstatush_n_i ( core_i.cs_registers_i.mstatush_n ), .csr_mstatush_q_i ( core_i.cs_registers_i.mstatush_rdata ), .csr_mstatush_we_i ( core_i.cs_registers_i.mstatush_we ), .csr_tselect_n_i ( core_i.cs_registers_i.debug_triggers_i.tselect_n ), .csr_tselect_q_i ( core_i.cs_registers_i.tselect_rdata ), .csr_tselect_we_i ( core_i.cs_registers_i.tselect_we ), - + .csr_mconfigptr_n_i ( core_i.cs_registers_i.mconfigptr_n ), + .csr_mconfigptr_q_i ( core_i.cs_registers_i.mconfigptr_rdata ), + .csr_mconfigptr_we_i ( core_i.cs_registers_i.mconfigptr_we ), .csr_mcounteren_n_i ( '0 /* Not supported in cv32e40x*/ ), .csr_mcounteren_q_i ( '0 /* Not supported in cv32e40x*/ ), .csr_mcounteren_we_i ( '0 /* Not supported in cv32e40x*/ ), @@ -762,9 +763,6 @@ endgenerate .csr_mseccfgh_n_i ( '0 /* Not supported in cv32e40x*/ ), .csr_mseccfgh_q_i ( '0 /* Not supported in cv32e40x*/ ), .csr_mseccfgh_we_i ( '0 /* Not supported in cv32e40x*/ ), - .csr_mconfigptr_n_i ( '0 ), - .csr_mconfigptr_q_i ( '0 ), - .csr_mconfigptr_we_i ( '0 ), .csr_menvcfg_n_i ( '0 /* Not supported in cv32e40x*/ ), .csr_menvcfg_q_i ( '0 /* Not supported in cv32e40x*/ ), .csr_menvcfg_we_i ( '0 /* Not supported in cv32e40x*/ ), From e55d4f5d6e69a53afd8498ff77fb6a0c785c7037 Mon Sep 17 00:00:00 2001 From: Oivind Ekelund Date: Wed, 6 Sep 2023 08:19:25 +0200 Subject: [PATCH 19/23] Remove todo in cv32e40x_wrapper. Current solution works fine, and mhpmevent_we is a single bit in RTL. Signed-off-by: Oivind Ekelund --- bhv/cv32e40x_wrapper.sv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bhv/cv32e40x_wrapper.sv b/bhv/cv32e40x_wrapper.sv index 01a66be52..2b30ebd76 100644 --- a/bhv/cv32e40x_wrapper.sv +++ b/bhv/cv32e40x_wrapper.sv @@ -682,7 +682,7 @@ endgenerate .csr_mcountinhibit_we_i ( core_i.cs_registers_i.mcountinhibit_we ), .csr_mhpmevent_n_i ( core_i.cs_registers_i.mhpmevent_n ), .csr_mhpmevent_q_i ( core_i.cs_registers_i.mhpmevent_rdata ), - .csr_mhpmevent_we_i ( {31'h0, core_i.cs_registers_i.mhpmevent_we} << // todo:ok: Add write enable for each register + .csr_mhpmevent_we_i ( {31'h0, core_i.cs_registers_i.mhpmevent_we} << core_i.cs_registers_i.csr_waddr[4:0] ), .csr_mscratch_n_i ( core_i.cs_registers_i.mscratch_n ), .csr_mscratch_q_i ( core_i.cs_registers_i.mscratch_rdata ), From 84ffbcd9cdcdf886223b1f6ca118d2ed6fe855be Mon Sep 17 00:00:00 2001 From: Halfdan Bechmann Dolva Date: Wed, 6 Sep 2023 09:26:01 +0200 Subject: [PATCH 20/23] Moved mscratchcsw register into USER section Signed-off-by: Halfdan Bechmann Dolva --- .../source/control_status_registers.rst | 118 +++++++++--------- 1 file changed, 61 insertions(+), 57 deletions(-) diff --git a/docs/user_manual/source/control_status_registers.rst b/docs/user_manual/source/control_status_registers.rst index b544f2341..30c93d7f8 100644 --- a/docs/user_manual/source/control_status_registers.rst +++ b/docs/user_manual/source/control_status_registers.rst @@ -197,33 +197,35 @@ instruction exception. :name: Control and Status Register Map (additional CSRs for User mode support) :class: no-scrollbar-table - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | CSR address | Name | Privilege | Parameter | Description | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | Machine CSRs | - +===================+================+============+============+====================================================+ - | 0x306 | ``mcounteren`` | MRW | | Machine Counter Enable | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x30A | ``menvcfg`` | MRW | | Machine Environment Configuration (lower 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x30C | ``mstateen0`` | MRW | | Machine state enable 0 (lower 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x30D | ``mstateen1`` | MRW | | Machine state enable 1 (lower 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x30E | ``mstateen2`` | MRW | | Machine state enable 2 (lower 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x30F | ``mstateen3`` | MRW | | Machine state enable 3 (lower 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x31A | ``menvcfgh`` | MRW | | Machine Environment Configuration (upper 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x31C | ``mstateen0h`` | MRW | | Machine state enable 0 (upper 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x31D | ``mstateen1h`` | MRW | | Machine state enable 1 (upper 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x31E | ``mstateen2h`` | MRW | | Machine state enable 2 (upper 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ - | 0x31F | ``mstateen3h`` | MRW | | Machine state enable 3 (upper 32 bits) | - +-------------------+----------------+------------+------------+----------------------------------------------------+ + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | CSR address | Name | Privilege | Parameter | Description | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | Machine CSRs | + +===================+=================+============+==============+====================================================+ + | 0x306 | ``mcounteren`` | MRW | | Machine Counter Enable | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x30A | ``menvcfg`` | MRW | | Machine Environment Configuration (lower 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x30C | ``mstateen0`` | MRW | | Machine state enable 0 (lower 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x30D | ``mstateen1`` | MRW | | Machine state enable 1 (lower 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x30E | ``mstateen2`` | MRW | | Machine state enable 2 (lower 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x30F | ``mstateen3`` | MRW | | Machine state enable 3 (lower 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x31A | ``menvcfgh`` | MRW | | Machine Environment Configuration (upper 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x31C | ``mstateen0h`` | MRW | | Machine state enable 0 (upper 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x31D | ``mstateen1h`` | MRW | | Machine state enable 1 (upper 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x31E | ``mstateen2h`` | MRW | | Machine state enable 2 (upper 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x31F | ``mstateen3h`` | MRW | | Machine state enable 3 (upper 32 bits) | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ + | 0x348 | ``mscratchcsw`` | MRW | ``CLIC`` = 1 | Conditional scratch swap on priv mode change | + +-------------------+-----------------+------------+--------------+----------------------------------------------------+ .. only:: PMP @@ -1013,6 +1015,38 @@ Detailed: | 31:0 | WARL (0x0) | Hardwired to 0. | +-------+------------+------------------------------------------------------------------+ + + .. _csr-mscratchcsw: + + Machine Scratch Swap for Priv Mode Change (``mscratchcsw``) + ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + CSR Address: 0x348 + + Reset Value: 0x0000_0000 + + Include Condition: ``CLIC`` = 1 + + Detailed: + + .. table:: + :widths: 10 20 70 + :class: no-scrollbar-table + + +-------------+------------+-------------------------------------------------------------------------+ + | Bit # | R/W | Description | + +=============+============+=========================================================================+ + | 31:0 | RW | **MSCRATCHCSW**: Machine scratch swap for privilege mode change | + +-------------+------------+-------------------------------------------------------------------------+ + + Scratch swap register for multiple privilege modes. + + .. note:: + Only the read-modify-write (swap/CSRRW) operation is useful for ``mscratchcsw``. + The behavior of the non-CSRRW variants (i.e. CSRRS/C, CSRRWI, CSRRS/CI) and CSRRW variants with **rd** = **x0** or **rs1** = **x0** on ``mscratchcsw`` are implementation-defined. + |corev| will treat such instructions as illegal instructions. + + Machine Counter-Inhibit Register (``mcountinhibit``) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1319,36 +1353,6 @@ Detailed: This register holds the machine mode interrupt level threshold. -.. _csr-mscratchcsw: - -Machine Scratch Swap for Priv Mode Change (``mscratchcsw``) -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -CSR Address: 0x348 - -Reset Value: 0x0000_0000 - -Include Condition: ``CLIC`` = 1 - -Detailed: - -.. table:: - :widths: 10 20 70 - :class: no-scrollbar-table - - +-------------+------------+-------------------------------------------------------------------------+ - | Bit # | R/W | Description | - +=============+============+=========================================================================+ - | 31:0 | RW | **MSCRATCHCSW**: Machine scratch swap for privilege mode change | - +-------------+------------+-------------------------------------------------------------------------+ - -Scratch swap register for multiple privilege modes. - -.. note:: - Only the read-modify-write (swap/CSRRW) operation is useful for ``mscratchcsw``. - The behavior of the non-CSRRW variants (i.e. CSRRS/C, CSRRWI, CSRRS/CI) and CSRRW variants with **rd** = **x0** or **rs1** = **x0** on ``mscratchcsw`` are implementation-defined. - |corev| will treat such instructions as illegal instructions. - .. _csr-mscratchcswl: Machine Scratch Swap for Interrupt-Level Change (``mscratchcswl``) From 0237acdeef48337a60d08f571831c5391082bd9c Mon Sep 17 00:00:00 2001 From: Oystein Knauserud Date: Wed, 6 Sep 2023 12:22:32 +0200 Subject: [PATCH 21/23] Removed dependency on mcause.mpp when checking if an mret will generate a pointer fetch (ID stage). SEC clean Signed-off-by: Oystein Knauserud --- rtl/cv32e40x_id_stage.sv | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/rtl/cv32e40x_id_stage.sv b/rtl/cv32e40x_id_stage.sv index 43c66f62a..850381146 100644 --- a/rtl/cv32e40x_id_stage.sv +++ b/rtl/cv32e40x_id_stage.sv @@ -670,11 +670,11 @@ module cv32e40x_id_stage import cv32e40x_pkg::*; assign id_valid_o = (instr_valid && !xif_waiting); assign first_op_o = if_id_pipe_i.first_op; - // An mret with mcause.minhv set and mcause.mpp = PRIV_LVL_M will cause a pointer fetch, and that pointer fetch is the last operation of the mret. + // An mret with mcause.minhv set will cause a pointer fetch, and that pointer fetch is the last operation of the mret. // Mrets with the mcause conditions not true will be normal single operation instructions. - // Using CSR signals below is safe, as any implicit or explicit CSR read in ID stage is halted if there is an implicit or explicit CSR write + // Using CSR signals below is safe, as any implicit CSR read in ID stage is halted if there is an implicit or explicit CSR write // in either EX or WB at the same time. - assign last_op_o = (sys_en && sys_mret_insn && mcause_i.minhv && (mcause_i.mpp == PRIV_LVL_M)) ? 1'b0 : if_id_pipe_i.last_op; + assign last_op_o = (sys_en && sys_mret_insn && mcause_i.minhv) ? 1'b0 : if_id_pipe_i.last_op; assign abort_op_o = if_id_pipe_i.abort_op || ctrl_byp_i.id_stage_abort; //--------------------------------------------------------------------------- // eXtension interface From 3966245a5d2e7a8805ae764041c57e4e6161ee0a Mon Sep 17 00:00:00 2001 From: Oystein Knauserud Date: Wed, 6 Sep 2023 14:16:52 +0200 Subject: [PATCH 22/23] Updated assertion a_priv_lvl_consistency to also allow mret pointers to change privilege level. Signed-off-by: Oystein Knauserud --- sva/cv32e40s_core_sva.sv | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/sva/cv32e40s_core_sva.sv b/sva/cv32e40s_core_sva.sv index dd86b54bf..2a6ce67e0 100644 --- a/sva/cv32e40s_core_sva.sv +++ b/sva/cv32e40s_core_sva.sv @@ -520,11 +520,15 @@ end // Check priviledge level consistency accross the pipeline. - // The only scenario where priv_lvl_if_q and priv_lvl are allowed to differ is when there's an MRET in the pipe + // The only scenario where priv_lvl_if_q and priv_lvl are allowed to differ is when there's an MRET or mret pointer in the pipe // MRET in ID will immediatly update the priviledge level for the IF stage, but priv_lvl won't be updated until the MRET retires in the WB stage a_priv_lvl_consistency : assert property (@(posedge clk) disable iff (!rst_ni) - (priv_lvl_if_q != priv_lvl) |-> ((sys_en_id && sys_mret_insn_id) || (id_ex_pipe.sys_en && id_ex_pipe.sys_mret_insn) || (ex_wb_pipe.sys_en && ex_wb_pipe.sys_mret_insn))) + (priv_lvl_if_q != priv_lvl) + |-> + ((sys_en_id && sys_mret_insn_id) || (id_ex_pipe.sys_en && id_ex_pipe.sys_mret_insn) || (ex_wb_pipe.sys_en && ex_wb_pipe.sys_mret_insn) || + (id_ex_pipe.instr_valid && id_ex_pipe.instr_meta.mret_ptr) || + (ex_wb_pipe.instr_valid && ex_wb_pipe.instr_meta.mret_ptr))) else `uvm_error("core", "IF priviledge level not consistent with current priviledge level") // Assert that change to user mode only happens when and MRET is in ID and mstatus.mpp == PRIV_LVL_U From 6c02cb84c1eb52fe0d0eadf27f2c8140577b7491 Mon Sep 17 00:00:00 2001 From: Oystein Knauserud Date: Thu, 7 Sep 2023 11:49:33 +0200 Subject: [PATCH 23/23] Updated format for printing LFSR_CFG parameters. Updated comments and added assertion for jalr with rs1==x0. Signed-off-by: Oystein Knauserud --- bhv/cv32e40s_core_log.sv | 12 ++++++------ sva/cv32e40s_controller_fsm_sva.sv | 15 ++++++++++++++- sva/cv32e40s_core_sva.sv | 30 +++++++++++++++++++++++------- 3 files changed, 43 insertions(+), 14 deletions(-) diff --git a/bhv/cv32e40s_core_log.sv b/bhv/cv32e40s_core_log.sv index 3aec792ad..bd6fe4e74 100644 --- a/bhv/cv32e40s_core_log.sv +++ b/bhv/cv32e40s_core_log.sv @@ -104,12 +104,12 @@ module cv32e40s_core_log import cv32e40s_pkg::*; $display("[cv32e40s_core]: PMP_MSECCFG_RV.rlb = %-1d", PMP_MSECCFG_RV.rlb); $display("[cv32e40s_core]: PMP_MSECCFG_RV.mmwp = %-1d", PMP_MSECCFG_RV.mmwp); $display("[cv32e40s_core]: PMP_MSECCFG_RV.mml = %-1d", PMP_MSECCFG_RV.mml); - $display("[cv32e40s_core]: LFSR0_CFG.coeffs = %-1d", LFSR0_CFG.coeffs); - $display("[cv32e40s_core]: LFSR0_CFG.default_seed = %-1d", LFSR0_CFG.default_seed); - $display("[cv32e40s_core]: LFSR1_CFG.coeffs = %-1d", LFSR1_CFG.coeffs); - $display("[cv32e40s_core]: LFSR1_CFG.default_seed = %-1d", LFSR1_CFG.default_seed); - $display("[cv32e40s_core]: LFSR2_CFG.coeffs = %-1d", LFSR2_CFG.coeffs); - $display("[cv32e40s_core]: LFSR2_CFG.default_seed = %-1d", LFSR2_CFG.default_seed); + $display("[cv32e40s_core]: LFSR0_CFG.coeffs = 0x%8h", LFSR0_CFG.coeffs); + $display("[cv32e40s_core]: LFSR0_CFG.default_seed = 0x%8h", LFSR0_CFG.default_seed); + $display("[cv32e40s_core]: LFSR1_CFG.coeffs = 0x%8h", LFSR1_CFG.coeffs); + $display("[cv32e40s_core]: LFSR1_CFG.default_seed = 0x%8h", LFSR1_CFG.default_seed); + $display("[cv32e40s_core]: LFSR2_CFG.coeffs = 0x%8h", LFSR2_CFG.coeffs); + $display("[cv32e40s_core]: LFSR2_CFG.default_seed = 0x%8h", LFSR2_CFG.default_seed); end // Log illegal instructions diff --git a/sva/cv32e40s_controller_fsm_sva.sv b/sva/cv32e40s_controller_fsm_sva.sv index 730852be4..507ef747c 100644 --- a/sva/cv32e40s_controller_fsm_sva.sv +++ b/sva/cv32e40s_controller_fsm_sva.sv @@ -178,7 +178,7 @@ module cv32e40s_controller_fsm_sva logic [4:0] jalr_rs_id; logic [31:0] rf_at_jump_id; @(posedge clk) disable iff (!rst_n) - ((jump_taken && alu_jmpr_id_i && (|if_id_pipe_i.instr.bus_resp.rdata[19:15]), // When JALR is taken from ID, + ((jump_taken && alu_jmpr_id_i && (|if_id_pipe_i.instr.bus_resp.rdata[19:15]), // When JALR is taken from ID, rf_at_jump_id = jalr_fw_id_i, // Store (possibly forwarded) RF value used for target calculation jalr_rs_id = if_id_pipe_i.instr.bus_resp.rdata[19:15]) // Store RS from JALR instruction ##1 (!(ctrl_fsm_o.kill_ex || ctrl_fsm_o.kill_wb) throughout (ex_wb_pipe_i.alu_jmp_qual && wb_valid_i && !ex_wb_pipe_i.last_sec_op)[->1]) // Wait for JALR to retire from WB (while not being killed) @@ -187,6 +187,19 @@ module cv32e40s_controller_fsm_sva a_jalr_stable_target: assert property(p_jalr_stable_target) else `uvm_error("controller", "Assertion a_jalr_stable_target failed"); + // Check that a JALR instruction which reads x0 gets zero as result on jalr_fw_id_i. + property p_jalr_target_x0; + logic [4:0] jalr_rs_id; + logic [31:0] rf_at_jump_id; + @(posedge clk) disable iff (!rst_n) + (jump_taken && alu_jmpr_id_i && !(|if_id_pipe_i.instr.bus_resp.rdata[19:15]) + |-> + jalr_fw_id_i == 32'd0); + + endproperty : p_jalr_target_x0 + + a_jalr_target_x0: assert property(p_jalr_target_x0) else `uvm_error("controller", "Assertion a_jalr_target_x0 failed"); + // Check that xret does not coincide with CSR write (to avoid using wrong return address) // This check is more strict than really needed; a CSR instruction would be allowed in EX as long // as its write action happens before the xret CSR usage diff --git a/sva/cv32e40s_core_sva.sv b/sva/cv32e40s_core_sva.sv index 2a6ce67e0..429c894ae 100644 --- a/sva/cv32e40s_core_sva.sv +++ b/sva/cv32e40s_core_sva.sv @@ -519,9 +519,25 @@ end else begin end - // Check priviledge level consistency accross the pipeline. + // Check privilege level consistency accross the pipeline. // The only scenario where priv_lvl_if_q and priv_lvl are allowed to differ is when there's an MRET or mret pointer in the pipe - // MRET in ID will immediatly update the priviledge level for the IF stage, but priv_lvl won't be updated until the MRET retires in the WB stage + // MRET in ID will immediately update the privilege level for the IF stage, but priv_lvl won't be updated until the MRET retires in the WB stage + // The actual privilege level used for instructions following an mret is propagated from the IF stage along with the instructions, giving proper + // privilege level even though the mret will not update the architectural state until it reaches WB. + // + // mret will change IF priv while in ID, and the difference between IF stage privilege and the architectural privilege may stay until the mret retires. + // If an mret generates a CLIC pointer fetch (mcause.minhv == 1), the mret is split in two operations in the ID stage. The architectural state + // will only update when the last part (the pointer) reaches WB. + // For the assert, we can thus allow a privilege level difference if an mret is in ID, EX or WB, or an mret pointer is in EX or WB. See pipeline diagram. + // + // IF | ID | EX | WB | + //----------|---------|---------|---------| + // | mret | x | x | // mret in ID kills IF + // pointer | <> | mret | x | // Pointer in IF, mret is in EX + // | pointer | <> | mret | // pointer in ID kills IF and jumps to pointer, mret is in WB (no state update due to pointer restart) + // x | x | pointer | <> | // pointer is in EX + // x | x | x | pointer | // pointer is in WB (will update architectural state) + a_priv_lvl_consistency : assert property (@(posedge clk) disable iff (!rst_ni) (priv_lvl_if_q != priv_lvl) @@ -529,7 +545,7 @@ end ((sys_en_id && sys_mret_insn_id) || (id_ex_pipe.sys_en && id_ex_pipe.sys_mret_insn) || (ex_wb_pipe.sys_en && ex_wb_pipe.sys_mret_insn) || (id_ex_pipe.instr_valid && id_ex_pipe.instr_meta.mret_ptr) || (ex_wb_pipe.instr_valid && ex_wb_pipe.instr_meta.mret_ptr))) - else `uvm_error("core", "IF priviledge level not consistent with current priviledge level") + else `uvm_error("core", "IF privilege level not consistent with current privilege level") // Assert that change to user mode only happens when and MRET is in ID and mstatus.mpp == PRIV_LVL_U // or a DRET is in WB and dcsr.prv == PRIV_LVL_U @@ -538,7 +554,7 @@ end $changed(priv_lvl_if) && (priv_lvl_if == PRIV_LVL_U) |-> ((sys_en_id && sys_mret_insn_id) && if_id_pipe.instr_valid && (cs_registers_mstatus_q.mpp == PRIV_LVL_U)) || ((ex_wb_pipe.instr_valid && ex_wb_pipe.sys_dret_insn && (dcsr.prv == PRIV_LVL_U)))) - else `uvm_error("core", "IF priviledge level changed to user mode when there's no MRET in ID stage") + else `uvm_error("core", "IF privilege level changed to user mode when there's no MRET in ID stage") // Assert that MPRV is cleared when privilege mode is changed to user a_priv_lvl_u_mode_mprv_clr: @@ -562,7 +578,7 @@ end assert property (@(posedge clk) disable iff (!rst_ni) ##1 $changed(priv_lvl_if) && (priv_lvl_if == PRIV_LVL_M) |-> (ctrl_fsm.pc_set && pc_mux_is_trap || ctrl_fsm.kill_if)) - else `uvm_error("core", "IF priviledge level changed to user mode when there's no MRET in ID stage") + else `uvm_error("core", "IF privilege level changed to user mode when there's no MRET in ID stage") // Assert that all exceptions trap to machine mode, except when in debug mode (todo: revisit when debug related part of user mode is implemented) a_priv_lvl_exception : @@ -571,12 +587,12 @@ end |-> (priv_lvl_if == PRIV_LVL_M)) else `uvm_error("core", "Exception not trapping to machine mode") - // Assert that jumps to mepc is done with priviledge level from mstatus.mpp + // Assert that jumps to mepc is done with privilege level from mstatus.mpp a_priv_lvl_mepc : assert property (@(posedge clk) disable iff (!rst_ni) (ctrl_fsm.pc_set && (ctrl_fsm.pc_mux == PC_MRET)) |-> (priv_lvl_if == cs_registers_mstatus_q.mpp)) - else `uvm_error("core", "MEPC fetch not performed with priviledge level from mstatus.mpp") + else `uvm_error("core", "MEPC fetch not performed with privilege level from mstatus.mpp") // Check that instruction fetches are always word aligned a_instr_addr_word_aligned :