[rtl] Rework assertions

This commit modifies the assertions to not fire as long as the reset
is active. Also, it updates some assertions.

This resolves lowRISC/ibex#274.

Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>

rtl/ibex_fetch_fifo.sv

@@ -220,8 +220,9 @@ module ibex_fetch_fifo #(
   // Assertions //
   ////////////////
 `ifndef VERILATOR
-  assert property (
+  // must not push to FIFO when full
-    @(posedge clk_i) disable iff (!rst_ni)
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    (in_valid_i) |-> ((valid_q[DEPTH-1] == 1'b0) || (clear_i == 1'b1)) );
+      (in_valid_i) |-> (!valid_q[DEPTH-1] || clear_i)) else
+    $display("Must not push when FIFO full");
 `endif
 endmodule

rtl/ibex_id_stage.sv

@@ -608,28 +608,27 @@ module ibex_id_stage #(
   ////////////////
 
 `ifndef VERILATOR
-  // make sure that branch decision is valid when jumping
+  // branch decision must be valid when jumping
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (branch_decision_i !== 1'bx || branch_in_dec == 1'b0) ) else
+      (branch_decision_i !== 1'bx || !branch_in_dec)) else
-      $display("Branch decision is X");
+    $display("Branch decision is X");
 
 `ifdef CHECK_MISALIGNED
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (~lsu_addr_incr_req_i) ) else
+      (!lsu_addr_incr_req_i)) else
-      $display("Misaligned memory access at %x",pc_id_i);
+    $display("Misaligned memory access at %x",pc_id_i);
 `endif
 
-  // the instruction delivered to the ID stage should always be valid
+  // instruction delivered to ID stage must always be valid
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (instr_valid_i & ~(illegal_c_insn_i | instr_fetch_err_i)) |->
+      (instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) |->
-        (!$isunknown(instr_rdata_i)) ) else
+      (!$isunknown(instr_rdata_i))) else
-      $display("Instruction is valid, but has at least one X");
+    $display("Instruction is valid, but has at least one X");
-
-  // make sure multicycles enable signals are unique
-  assert property (
-    @(posedge clk_i) ~(data_req_dec & multdiv_en_dec)) else
-      $display("Multicycles enable signals are not unique");
 
+  // multicycle enable signals must be unique
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
+      ($onehot0({data_req_dec, multdiv_en_dec, branch_in_dec, jump_in_dec}))) else
+    $display("Multicycle enable signals are not unique");
 `endif
 
 endmodule

rtl/ibex_if_stage.sv

@@ -256,15 +256,15 @@ module ibex_if_stage #(
   // Assertions //
   ////////////////
 `ifndef VERILATOR
-  // the boot address needs to be aligned to 256 bytes
+  // boot address must be aligned to 256 bytes
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (boot_addr_i[7:0] == 8'h00) ) else
+      (boot_addr_i[7:0] == 8'h00)) else
-      $error("The provided boot address is not aligned to 256 bytes");
+    $error("Provided boot address not aligned to 256 bytes");
 
-  // assert that the address is word aligned when request is sent
+  // address must be word aligned when request is sent
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (instr_req_o) |-> (instr_addr_o[1:0] == 2'b00) ) else
+      (instr_req_o) |-> (instr_addr_o[1:0] == 2'b00)) else
-      $display("Instruction address not word aligned");
+    $display("Instruction address not word aligned");
 `endif
 
 endmodule

rtl/ibex_load_store_unit.sv

@@ -483,25 +483,25 @@ module ibex_load_store_unit (
   ////////////////
 
 `ifndef VERILATOR
-  // there should not be an rvalid unless the FSM is handlling it
+  // there must not be an rvalid unless the FSM is handlling it
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (data_rvalid_i) |-> ((ls_fsm_cs == WAIT_RVALID) ||
+      (data_rvalid_i) |-> ((ls_fsm_cs == WAIT_RVALID) ||
-        (ls_fsm_cs == WAIT_RVALID_MIS) || (ls_fsm_cs == WAIT_RVALID_DONE)) ) else
+      (ls_fsm_cs == WAIT_RVALID_MIS) || (ls_fsm_cs == WAIT_RVALID_DONE))) else
-      $display("Data response valid received without expecting it");
+    $display("Data response valid received without expecting it");
 
-  // assert that errors are only sent at the same time as rvalid
+  // errors must only be sent together with rvalid
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (data_err_i) |-> (data_rvalid_i) ) else
+      (data_err_i) |-> (data_rvalid_i)) else
-      $display("Data error not sent with rvalid");
+    $display("Data error not sent with rvalid");
 
-  // assert that the address does not contain X when request is sent
+  // address must not contain X when request is sent
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (data_req_o) |-> (!$isunknown(data_addr_o)) ) else
+      (data_req_o) |-> (!$isunknown(data_addr_o))) else
-      $display("Data address not valid");
+    $display("Data address not valid");
 
-  // assert that the address is word aligned when request is sent
+  // address must be word aligned when request is sent
-  assert property (
+  assert property (@(posedge clk_i) disable iff (!rst_ni)
-    @(posedge clk_i) (data_req_o) |-> (data_addr_o[1:0] == 2'b00) ) else
+      (data_req_o) |-> (data_addr_o[1:0] == 2'b00)) else
-      $display("Data address not word aligned");
+    $display("Data address not word aligned");
 `endif
 endmodule