Merge pull request #973 from silabs-oysteink/silabs-oysteink_missing-…

…s-asserts

Added assertions from e40s that were missing on e40x

sva/cv32e40x_controller_fsm_sva.sv

@@ -41,6 +41,8 @@ module cv32e40x_controller_fsm_sva
   input ctrl_fsm_t      ctrl_fsm_o,
   input ctrl_byp_t      ctrl_byp_i,
   input logic           jump_taken_id,
+  input logic           branch_in_ex,
+  input logic           branch_taken_q,
   input logic           branch_taken_ex,
   input logic           branch_decision_ex_i,
   input ctrl_state_e    ctrl_fsm_cs,
@@ -181,6 +183,19 @@ module cv32e40x_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
@@ -340,6 +355,44 @@ module cv32e40x_controller_fsm_sva
                       |-> exception_in_wb && (exception_cause_wb == EXC_CAUSE_ILLEGAL_INSN))
       else `uvm_error("controller", "mret in debug mode not flagged as illegal")
 
+  // Helper logic to make assertion look cleaner
+  // Same logic as in the bypass module, but duplicated here to catch any changes in bypass
+  // that could lead to undetected errors
+  logic csrw_ex_wb;
+  assign csrw_ex_wb = (
+                        ((id_ex_pipe_i.csr_en || (id_ex_pipe_i.sys_en && id_ex_pipe_i.sys_mret_insn)) && id_ex_pipe_i.instr_valid) ||
+                        ((ex_wb_pipe_i.csr_en || (ex_wb_pipe_i.sys_en && ex_wb_pipe_i.sys_mret_insn)) && ex_wb_pipe_i.instr_valid)
+                      );
+
+  // Check that mret is stalled in ID if CSR writes (explicit and implicit)
+  // are present in EX or WB. Exluding the case where the second part of an mret is in ID while the first part
+  // is in either EX or WB.
+  a_mret_id_halt :
+  assert property (@(posedge clk) disable iff (!rst_n)
+                    ((sys_en_id_i && sys_mret_id_i) && if_id_pipe_i.instr_valid && csrw_ex_wb)
+                    |-> (!id_valid_i && ctrl_fsm_o.halt_id))
+    else `uvm_error("controller", "mret not halted in ID when CSR write is present in EX or WB")
+
+  // Assert that branches (that are not already taken) are always taken in the first cycle of EX, unless EX is killed or halted
+  // What we really want to check with this assertion is that a branch taken always results
+  // in a pc_set to PC_BRANCH.
+  // If the branch is not taken in the first cycle of EX, caution must be taken to avoid e.g. a jump in
+  // ID taking presedence over the branch in EX.
+
+  a_branch_in_ex_taken_first_cycle:
+  assert property (@(posedge clk) disable iff (!rst_n)
+                    ($rose(branch_in_ex && branch_decision_ex_i) && !branch_taken_q && !(ctrl_fsm_o.halt_ex || ctrl_fsm_o.kill_ex) |->
+                    ctrl_fsm_o.pc_set && (ctrl_fsm_o.pc_mux == PC_BRANCH) &&
+                    ctrl_fsm_o.kill_if && ctrl_fsm_o.kill_id));
+
+  // When flushing the pipeline due to CSR updates in WB, make sure there we don't initiate transactions on the data interface
+  // and that there are no outstanding transactions from the LSU point of view.
+  // There might still be outstanding transactions in the write buffer, which is why we can't check that data_req_o==0
+  a_csr_wr_in_wb_flush_no_obi:
+  assert property (@(posedge clk) disable iff (!rst_n)
+                    (csr_wr_in_wb_flush_i) |-> (lsu_outstanding_cnt == 2'b00) && !lsu_trans_valid_i)
+    else `uvm_error("controller", "Flushing pipeline when the LSU have outstanding transactions")
+
   // assert that NMI's are not reported on irq_ack
   // Exception for the case where the core wakes from SLEEP due to an interrupt
   //   - in that case the interrupt is honored while there may be a pending nmi.

sva/cv32e40x_load_store_unit_sva.sv

@@ -120,6 +120,19 @@ module cv32e40x_load_store_unit_sva
   a_no_spurious_rvalid :
     assert property(p_no_spurious_rvalid) else `uvm_error("load_store_unit", "Assertion a_no_spurious_rvalid failed")
 
+  // Check that the address/we/be/atop does not contain X when request is sent
+  property p_address_phase_signals_defined;
+    @(posedge clk) (m_c_obi_data_if.s_req.req == 1'b1) |->
+                    (!($isunknown(m_c_obi_data_if.req_payload.addr) ||
+                      $isunknown(m_c_obi_data_if.req_payload.we)    ||
+                      $isunknown(m_c_obi_data_if.req_payload.be)    ||
+                      $isunknown(m_c_obi_data_if.req_payload.atop)));
+  endproperty
+
+  a_address_phase_signals_defined :
+    assert property(p_address_phase_signals_defined)
+      else `uvm_error("load_store_unit", "Assertion a_address_phase_signals_defined failed")
+
   // No transaction allowd if EX is halted or killed
   a_lsu_halt_kill:
     assert property (@(posedge clk) disable iff (!rst_n)

sva/cv32e40x_rvfi_sva.sv

@@ -124,6 +124,20 @@ module cv32e40x_rvfi_sva
     `uvm_error("rvfi",
       $sformatf("Every irq_ack should be followed by the corresponding rvfi_intr"));
 
+  // rvfi_intr.intr shall also have rvfi_intr.exception or rvfi_intr.interrupt set at the same time
+  property p_rvfi_intr_interrupt_exception;
+    @(posedge clk_i) disable iff (!rst_ni)
+    rvfi_intr.intr
+      |->
+        (rvfi_intr.interrupt ||
+        rvfi_intr.exception);
+  endproperty : p_rvfi_intr_interrupt_exception
+
+  a_rvfi_intr_interrupt_exception: assert property (p_rvfi_intr_interrupt_exception)
+  else
+    `uvm_error("rvfi",
+      $sformatf("rvfi_intr.intr set without rvfi_intr.exception or rvfi_intr.interrupt"));
+
 
   // Sequence used to locate rvfi_valid following rvfi_valid with prereq set
   sequence s_goto_next_rvfi_valid(prereq);