Module prim_count

prim_count #( .Width(Width), .ResetValue(ResetValue), .EnableAlertTriggerSVA(EnableAlertTriggerSVA), .PossibleActions(PossibleActions) ) u_prim_count ( .clk_i(clk_i), .rst_ni(rst_ni), .clr_i(clr_i), .set_i(set_i), .set_cnt_i(set_cnt_i), .incr_en_i(incr_en_i), .decr_en_i(decr_en_i), .step_i(step_i), .commit_i(commit_i), .cnt_o(cnt_o), .cnt_after_commit_o(cnt_after_commit_o), .err_o(err_o) );

Block Diagram of prim_count

Hardened counter primitive

This internally uses a cross counter scheme with primary and a secondary counter, where the secondary counter counts in reverse direction. The sum of both counters must remain constant and equal to 2**Width-1 or otherwise an err_o will be asserted.

This counter supports a generic clear / set / increment / decrement interface

clr_i: This clears the primary counter to ResetValue and adjusts the secondary counter to match (i.e. 2Width-1-ResetValue). Clear has priority over set, increment and decrement. set_i: This sets the primary counter to set_cnt_i and adjusts the secondary counter to match (i.e. 2Width-1-set_cnt_i). Set has priority over increment and decrement. incr_en_i: Increments the primary counter by step_i, and decrements the secondary by step_i. decr_en_i: Decrements the primary counter by step_i, and increments the secondary by step_i. commit_i: Counter changes only take effect when commit_i is set. This does not effect the cnt_after_commit_o output which gives the next counter state if the change is committed.

Note that if both incr_en_i and decr_en_i are asserted at the same time, the counter remains unchanged. The counter is also protected against under- and overflows.

Parameters

Name	Default	Description
Width	2
ResetValue	'0	Can be used to reset the counter to a different value than 0, for example when the counter is used as a down-counter.
EnableAlertTriggerSVA	1	This should only be disabled in special circumstances, for example in non-comportable IPs where an error does not trigger an alert.
PossibleActions	{$bits(action_mask_t){1'b1}}	We have some assertions below with preconditions that depend on particular input actions (clear, set, incr, decr). If the design has instantiated prim_count with one of these actions tied to zero, the preconditions for the associated assertions will not be satisfiable. The result is an unreachable item, which we treat as a failed assertion in the report. To avoid this, we the instantiation to specify the actions which might happen. If this is not '1, we will have an assertion which assert the corresponding action is never triggered. We can then use this to avoid the unreachable assertions.

Ports

Name	Type	Direction	Description
clk_i	wire logic	input
rst_ni	wire logic	input
clr_i	wire logic	input
set_i	wire logic	input
set_cnt_i	wire logic [Width - 1 : 0]	input	Set value for the counter.
incr_en_i	wire logic	input
decr_en_i	wire logic	input
step_i	wire logic [Width - 1 : 0]	input	Increment/decrement step when enabled.
commit_i	wire logic	input
cnt_o	var logic [Width - 1 : 0]	output	Current counter state
cnt_after_commit_o	var logic [Width - 1 : 0]	output	Next counter state if committed
err_o	var logic	output

Assertions

Name	Kind	Description
prim_count.ClrNeverTrue_A	concurent assert	disable iff((!rst_ni)!=='0)(clr_i !== 1'b1)
prim_count.SetNeverTrue_A	concurent assert	disable iff((!rst_ni)!=='0)(set_i !== 1'b1)
prim_count.IncrNeverTrue_A	concurent assert	disable iff((!rst_ni)!=='0)(incr_en_i !== 1'b1)
prim_count.DecrNeverTrue_A	concurent assert	disable iff((!rst_ni)!=='0)(decr_en_i !== 1'b1)
prim_count.CntNext_A	concurent assert	Cnt next disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(rst_ni |=> ($past(! commit_i) || (cnt_o == $past(cnt_after_commit_o))))
prim_count.ClrFwd_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(((rst_ni && commit_i) && clr_i) |=> ((cnt_o == ResetValue) && (cnt_q[1] == ({Width{1'b1}} - ResetValue))))
prim_count.SetFwd_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && commit_i) && set_i) && ! clr_i) |=> ((cnt_o == $past(set_cnt_i)) && (cnt_q[1] == ({Width{1'b1}} - $past(set_cnt_i)))))
prim_count.IncrDecrUpDnCnt_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && decr_en_i) && ! (clr_i || set_i)) |=> ($stable(cnt_o) && $stable(cnt_q[1])))
prim_count.IncrUpCnt_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && ! ((clr_i || set_i) || decr_en_i)) && commit_i) |=> (cnt_o == min(($past(cnt_o) + $past({2'b0, step_i})), {2'b0, {Width{1'b1}}})))
prim_count.IncrDnCnt_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && ! ((clr_i || set_i) || decr_en_i)) && commit_i) |=> (cnt_q[1] == max(($past((signed ' {2'b0, cnt_q[1]})) - $past({2'b0, step_i})), '0)))
prim_count.UpCntIncrStable_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(((incr_en_i && ! ((clr_i || set_i) || decr_en_i)) && (cnt_o == {Width{1'b1}})) |=> $stable(cnt_o))
prim_count.DnCntIncrStable_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && incr_en_i) && ! ((clr_i || set_i) || decr_en_i)) && (cnt_q[1] == '0)) |=> $stable(cnt_q[1]))
prim_count.DecrUpCnt_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && decr_en_i) && ! ((clr_i || set_i) || incr_en_i)) && commit_i) |=> (cnt_o == max(($past((signed ' {2'b0, cnt_o})) - $past({2'b0, step_i})), '0)))
prim_count.DecrDnCnt_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && decr_en_i) && ! ((clr_i || set_i) || incr_en_i)) && commit_i) |=> (cnt_q[1] == min(($past(cnt_q[1]) + $past({2'b0, step_i})), {2'b0, {Width{1'b1}}})))
prim_count.UpCntDecrStable_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(((decr_en_i && ! ((clr_i || set_i) || incr_en_i)) && (cnt_o == '0)) |=> $stable(cnt_o))
prim_count.DnCntDecrStable_A	concurent assert	disable iff((err_o||fpv_err_present||!rst_ni)!=='0)((((rst_ni && decr_en_i) && ! ((clr_i || set_i) || incr_en_i)) && (cnt_q[1] == {Width{1'b1}})) |=> $stable(cnt_q[1]))
prim_count.ChangeBackward_A	concurent assert	A backwards check for count changes. This asserts that the count only changes if one of the inputs that should tell it to change (clear, set, increment, decrement) does so. disable iff((err_o||fpv_err_present||!rst_ni)!=='0)(rst_ni ## 1 (($changed(cnt_o) && $changed(cnt_q[1])) |-> $past(((clr_i || set_i) || (commit_i && (incr_en_i || decr_en_i))))))
prim_count.CntErrReported_A	concurent assert	Check that count errors are reported properly in err_o disable iff((!rst_ni)!=='0)(((cnt_q[1] + cnt_q[0]) != {Width{1'b1}}) == err_o)
prim_count.AssertConnected_A	immediate assert	((unused_assert_connected === 1'b1) || ! EnableAlertTriggerSVA)

Functions

function logic signed[Width+1:0]

max(logic signed[Width+1:0] a, logic signed[Width+1:0] b)

Helper functions for assertions.

Parameters:

• a (logic signed[Width+1:0])

• b (logic signed[Width+1:0])

function logic signed[Width+1:0]

min(logic signed[Width+1:0] a, logic signed[Width+1:0] b)

Parameters:

• a (logic signed[Width+1:0])

• b (logic signed[Width+1:0])

×