Fix for issue #410

bhv/cv32e40x_wrapper.sv

@@ -231,6 +231,8 @@ module cv32e40x_wrapper
                               .lsu_trans_valid_i            (core_i.load_store_unit_i.trans_valid),
                               .csr_en_id_i                  (core_i.id_stage_i.csr_en),
                               .ptr_in_if_i                  (core_i.if_stage_i.ptr_in_if_o),
+                              .instr_req_o                  (core_i.instr_req_o),
+                              .instr_dbg_o                  (core_i.instr_dbg_o),
                               .*);
   bind cv32e40x_cs_registers:
     core_i.cs_registers_i
@@ -266,7 +268,10 @@ module cv32e40x_wrapper
     core_i.if_stage_i.prefetch_unit_i
       cv32e40x_prefetch_unit_sva
       #(.SMCLIC(SMCLIC))
-      prefetch_unit_sva (.*);
+      prefetch_unit_sva (
+                          .ctrl_fsm_cs     (core_i.controller_i.controller_fsm_i.ctrl_fsm_cs),
+                          .debug_req_i     (core_i.debug_req_i),
+                          .*);
 
   generate
     if(M_EXT == M) begin: div_sva

rtl/cv32e40x_controller_fsm.sv

@@ -669,17 +669,20 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
       RESET: begin
         ctrl_fsm_o.instr_req = 1'b0;
         if (fetch_enable_i) begin
-          ctrl_fsm_ns = BOOT_SET;
+          if (debug_req_i) begin
+            // Not raising instr_req to prevent fetching until we are in debug mode
+            ctrl_fsm_o.instr_req = 1'b0;
+            ctrl_fsm_o.pc_mux    = PC_BOOT;
+            ctrl_fsm_o.pc_set    = 1'b1; // pc_set is required for propagating boot address to dpc (from IF stage)
+            ctrl_fsm_ns          = DEBUG_TAKEN;
+          end else begin
+            ctrl_fsm_o.instr_req = 1'b1;
+            ctrl_fsm_o.pc_mux    = PC_BOOT;
+            ctrl_fsm_o.pc_set    = 1'b1;
+            ctrl_fsm_ns          = FUNCTIONAL;
+          end
         end
       end
-      // BOOT_SET state required to prevent (timing) path from
-      // fetch_enable_i via pc_set to instruction interface outputs
-      BOOT_SET: begin
-        ctrl_fsm_o.instr_req = 1'b1;
-        ctrl_fsm_o.pc_mux    = PC_BOOT;
-        ctrl_fsm_o.pc_set    = 1'b1;
-        ctrl_fsm_ns = FUNCTIONAL;
-      end
       FUNCTIONAL: begin
         // NMI
         if (pending_nmi && nmi_allowed) begin
@@ -1346,7 +1349,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*;
 
     case (debug_fsm_cs)
       HAVERESET: begin
-        if (debug_mode_n || (ctrl_fsm_ns == BOOT_SET)) begin
+        if (debug_mode_n || (ctrl_fsm_ns == FUNCTIONAL)) begin
           if (debug_mode_n) begin
             debug_fsm_ns = HALTED;
           end else begin

rtl/include/cv32e40x_pkg.sv

@@ -169,7 +169,7 @@ typedef enum logic [DIV_OP_WIDTH-1:0]
  } div_opcode_e;
 
 // FSM state encoding
-typedef enum logic [2:0] { RESET, BOOT_SET, FUNCTIONAL, SLEEP, DEBUG_TAKEN} ctrl_state_e;
+typedef enum logic [2:0] { RESET, FUNCTIONAL, SLEEP, DEBUG_TAKEN} ctrl_state_e;
 
 // Debug FSM state encoding
 // State encoding done one-hot to ensure that debug_havereset_o, debug_running_o, debug_halted_o

sva/cv32e40x_alignment_buffer_sva.sv

@@ -186,16 +186,6 @@ module cv32e40x_alignment_buffer_sva
         `uvm_error("Alignment buffer SVA",
                   $sformatf("Wrong PC after branch"))
 
-  // Check that a taken branch can only occur if fetching is requested
-  property p_branch_implies_req;
-    @(posedge clk) disable iff (!rst_n) (ctrl_fsm_i.pc_set) |-> (ctrl_fsm_i.instr_req);
-  endproperty
-
-   a_branch_implies_req:
-     assert property(p_branch_implies_req)
-     else
-       `uvm_error("Alignment buffer SVA",
-                  $sformatf("Taken branch occurs while fetching is not requested"))
 
   // Check that we never exceed two outstanding transactions
   property p_max_outstanding;

sva/cv32e40x_controller_fsm_sva.sv

@@ -108,7 +108,11 @@ module cv32e40x_controller_fsm_sva
   input pipe_pc_mux_e   pipe_pc_mux_ctrl,
   input logic           ptr_in_if_i,
   input logic           etrigger_in_wb,
-  input logic           lsu_wpt_match_wb_i
+  input logic           lsu_wpt_match_wb_i,
+  input logic           debug_req_i,
+  input logic           fetch_enable_i,
+  input logic           instr_req_o,
+  input logic           instr_dbg_o
 );
 
 
@@ -198,11 +202,11 @@ module cv32e40x_controller_fsm_sva
                     (ctrl_fsm_o.kill_wb) |-> (!csr_we_i) )
     else `uvm_error("controller", "csr written while kill_wb is asserted")
 
-  // Check that no stages have valid instructions using RESET or BOOT_SET
+  // Check that no stages have valid instructions using RESET
   a_reset_if_csr :
     assert property (@(posedge clk) disable iff (!rst_n)
-            ((ctrl_fsm_cs == RESET) || (ctrl_fsm_cs == BOOT_SET)) |-> (!if_valid_i && !if_id_pipe_i.instr_valid && !id_ex_pipe_i.instr_valid && !ex_wb_pipe_i.instr_valid) )
-      else `uvm_error("controller", "Instruction valid during RESET or BOOT_SET")
+            ((ctrl_fsm_cs == RESET)) |-> (!if_valid_i && !if_id_pipe_i.instr_valid && !id_ex_pipe_i.instr_valid && !ex_wb_pipe_i.instr_valid) )
+      else `uvm_error("controller", "Instruction valid during RESET")
 
   // Check that no LSU insn can be in EX when there is a WFI or WFE in WB
   a_wfi_wfe_lsu_csr :
@@ -870,5 +874,9 @@ end
                   |->
                   (abort_op_wb_i && (ctrl_fsm_ns == DEBUG_TAKEN)))
     else `uvm_error("controller", "Debug not entered on a WPT match")
+
+
+
+
 endmodule
 

sva/cv32e40x_core_sva.sv

@@ -32,6 +32,7 @@ module cv32e40x_core_sva
   )
   (
   input logic        clk,
+  input logic        clk_i,
   input logic        rst_ni,
 
   input ctrl_fsm_t   ctrl_fsm,
@@ -54,6 +55,9 @@ module cv32e40x_core_sva
   input logic        branch_taken_in_ex,
   input logic        last_op_wb,
 
+  input logic        fetch_enable_i,
+  input logic        debug_req_i,
+
   input alu_op_a_mux_e alu_op_a_mux_sel_id_i,
   input alu_op_b_mux_e alu_op_b_mux_sel_id_i,
   input logic [31:0]   operand_a_id_i,
@@ -69,6 +73,8 @@ module cv32e40x_core_sva
   // probed OBI signals
   input logic [31:0] instr_addr_o,
   input logic [1:0]  instr_memtype_o,
+  input logic        instr_req_o,
+  input logic        instr_dbg_o,
   input logic [1:0]  data_memtype_o,
   input logic        data_req_o,
   input logic        data_we_o,
@@ -554,5 +560,29 @@ endproperty;
 
 a_no_irq_after_lsu: assert property(p_no_irq_after_lsu)
   else `uvm_error("core", "Interrupt taken after disabling");
-endmodule // cv32e40x_core_sva
 
+// If debug_req_i is asserted when fetch_enable_i gets asserted we should not execute any
+// instruction until the core is in debug mode.
+a_reset_into_debug:
+assert property (@(posedge clk_i) disable iff (!rst_ni)
+                (ctrl_fsm_cs == RESET) &&
+                fetch_enable_i &&
+                debug_req_i
+                ##1
+                debug_req_i // Controller gets a one cycle delayed fetch enable, must keep debug_req_i asserted for two cycles
+                |->
+                !wb_valid until (wb_valid && ctrl_fsm.debug_mode))
+  else `uvm_error("controller", "Debug out of reset but executed instruction outside debug mode")
+
+// When entering debug out of reset, the first fetch must also flag debug on the instruction OBI interface
+a_first_fetch_debug:
+assert property (@(posedge clk_i) disable iff (!rst_ni)
+                (ctrl_fsm_cs == RESET) &&
+                fetch_enable_i &&
+                debug_req_i
+                ##1
+                debug_req_i // Controller gets a one cycle delayed fetch enable, must keep debug_req_i asserted for two cycles
+                |->
+                !instr_req_o until (instr_req_o && instr_dbg_o))
+  else `uvm_error("controller", "Debug out of reset but fetched without setting instr_dbg_o")
+endmodule // cv32e40x_core_sva

sva/cv32e40x_prefetch_unit_sva.sv

@@ -32,7 +32,9 @@ module cv32e40x_prefetch_unit_sva import cv32e40x_pkg::*;
    input logic        prefetch_ready_i,
    input logic        trans_valid_o,
    input logic        trans_ready_i,
-   input logic        fetch_ptr_resp
+   input logic        fetch_ptr_resp,
+   input ctrl_state_e ctrl_fsm_cs,
+   input logic        debug_req_i
 
   );
 
@@ -46,8 +48,11 @@ module cv32e40x_prefetch_unit_sva import cv32e40x_pkg::*;
     else `uvm_error("prefetch_buffer", "Assertion a_branch_halfword_aligned failed")
 
   // Check that a taken branch can only occur if fetching is requested
+  // Exception while in RESET state and debug_request_i is high - in that case we want to
+  // do a pc_set to update the IF stage PC without actually fetching anything. This is to ensure
+  // that dpc gets the correct (boot) address when going from reset to debug.
   property p_branch_implies_req;
-      @(posedge clk) (ctrl_fsm_i.pc_set) |-> (ctrl_fsm_i.instr_req);
+      @(posedge clk) (ctrl_fsm_i.pc_set) && !((ctrl_fsm_cs == RESET) && debug_req_i) |-> (ctrl_fsm_i.instr_req);
     endproperty
 
   a_branch_implies_req : assert property(p_branch_implies_req)