[fpv] Fix some assumptions in prim_count
This PR fixes some assumptions in prim_count for cross mode.
1). The down counter underflow assumption used `%` that could be very
complex for FPV. I slightly change the assumption to avoid `%`.
2). Underflow and overflow assumptions should apply to all cross
counters because they have up and down counters.
3). ASSERT_INIT for FPV is only used for parameters and constants, thus
does not apply to the wire. Excluded that assertion check for simulation
only.
Signed-off-by: Cindy Chen <chencindy@opentitan.org>
diff --git a/hw/ip/prim/rtl/prim_count.sv b/hw/ip/prim/rtl/prim_count.sv
index 1d5a06c..229368f 100644
--- a/hw/ip/prim/rtl/prim_count.sv
+++ b/hw/ip/prim/rtl/prim_count.sv
@@ -132,6 +132,19 @@
`ASSERT(CrossCntErrBackward_A, err_o |->
(cmp_valid == CmpValid) && ((down_cnt + up_cnt_q[0]) != {1'b0, max_val}))
+ // Down counter assumption to control underflow
+ // We can also constrain the down counter underflow via `down_cnt % step_i == 0`.
+ // However, modulo operation can be very complex for formal analysis.
+ `ASSUME(DownCntStepInt_A, cmp_valid == CmpValid |-> down_cnt == 0 || down_cnt >= step_i)
+
+ // Up counter assumption to control overflow
+ logic [Width:0] unused_cnt;
+ assign unused_cnt = up_cnt_q[0] + step_i;
+ logic unused_incr_cnt;
+ assign unused_incr_cnt = (cmp_valid == CmpValid) & !clr_i & !set_i;
+
+ `ASSUME(UpCntOverFlow_A, unused_incr_cnt && !err |-> ~unused_cnt[Width])
+
end else if (CntStyle == DupCnt) begin : gen_dup_cnt_hardening
// duplicate count compare is always valid
assign cmp_valid = CmpValid;
@@ -147,20 +160,6 @@
(cmp_valid == CmpInvalid) ? '0 : 1'b1;
// ASSERTIONS AND ASSUMPTIONS
-
- // Down counter assumption to control underflow
- if (CntStyle == CrossCnt && OutSelDnCnt) begin : gen_down_cnter_assumptions
- `ASSUME(DownCntStepInt_A, cmp_valid == CmpValid |-> max_val % step_i == 0)
- // Up counter assumption to control overflow
- end else begin : gen_up_cnter_assumptions
- logic [Width:0] unused_cnt;
- assign unused_cnt = up_cnt_q[0] + step_i;
- logic unused_incr_cnt;
- assign unused_incr_cnt = (cmp_valid == CmpValid) & !clr_i & !set_i;
-
- `ASSUME(UpCntOverFlow_A, unused_incr_cnt && !err |-> ~unused_cnt[Width])
- end
-
`ifdef INC_ASSERT
// Helper variables to hold the previous valid `cnt_o` and `step_i` when `en_i` is set.
logic [Width-1:0] past_cnt_o, past_step_i;
@@ -199,8 +198,12 @@
// is used in design without adding this assertion check.
`ifdef INC_ASSERT
logic unused_assert_connected;
+
+ // ASSERT_INIT can only be used for paramters/constants in FPV.
+ `ifdef SIMULATION
`ASSERT_INIT(AssertConnected_A, unused_assert_connected === 1'b1)
`endif
+ `endif
endmodule // prim_count
`define ASSERT_PRIM_COUNT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 5) \
