hw/ip/prim/rtl/prim_count.sv - 3p/lowrisc/opentitan - Git at Google

 // Copyright lowRISC contributors.
 // Licensed under the Apache License, Version 2.0, see LICENSE for details.
 // SPDX-License-Identifier: Apache-2.0
 //
 // 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. 2**Width-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. 2**Width-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.
 //
 // 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.

 `include "prim_assert.sv"

 module prim_count #(
   parameter int Width = 2,
   // Can be used to reset the counter to a different value than 0, for example when
   // the counter is used as a down-counter.
   parameter logic [Width-1:0] ResetValue = '0,
   // This should only be disabled in special circumstances, for example
   // in non-comportable IPs where an error does not trigger an alert.
   parameter bit EnableAlertTriggerSVA = 1
 ) (
   input clk_i,
   input rst_ni,
   input clr_i,
   input set_i,
   input [Width-1:0] set_cnt_i,         // Set value for the counter.
   input incr_en_i,
   input decr_en_i,
   input [Width-1:0] step_i,            // Increment/decrement step when enabled.
   output logic [Width-1:0] cnt_o,      // Current counter state
   output logic [Width-1:0] cnt_next_o, // Next counter state
   output logic err_o
 );

   ///////////////////
   // Counter logic //
   ///////////////////

   // Reset Values for primary and secondary counters.
   localparam int NumCnt = 2;
   localparam logic [NumCnt-1:0][Width-1:0] ResetValues = {{Width{1'b1}} - ResetValue, // secondary
                                                           ResetValue};                // primary

   logic [NumCnt-1:0][Width-1:0] cnt_d, cnt_q, fpv_force;

 `ifndef FPV_SEC_CM_ON
   // This becomes a free variable in FPV.
   assign fpv_force = '0;
 `endif

   for (genvar k = 0; k < NumCnt; k++) begin : gen_cnts
     // Note that increments / decrements are reversed for the secondary counter.
     logic incr_en, decr_en;
     logic [Width-1:0] set_val;
     if (k == 0) begin : gen_up_cnt
       assign incr_en = incr_en_i;
       assign decr_en = decr_en_i;
       assign set_val = set_cnt_i;
     end else begin : gen_dn_cnt
       assign incr_en = decr_en_i;
       assign decr_en = incr_en_i;
       // The secondary value needs to be adjusted accordingly.
       assign set_val = {Width{1'b1}} - set_cnt_i;
     end

     // Main counter logic
     logic [Width:0] ext_cnt;
     assign ext_cnt = (decr_en) ? {1'b0, cnt_q[k]} - {1'b0, step_i} :
                      (incr_en) ? {1'b0, cnt_q[k]} + {1'b0, step_i} : {1'b0, cnt_q[k]};

     // Saturation logic
     logic uflow, oflow;
     assign oflow = incr_en && ext_cnt[Width];
     assign uflow = decr_en && ext_cnt[Width];
     logic [Width-1:0] cnt_sat;
     assign cnt_sat = (uflow) ? '0            :
                      (oflow) ? {Width{1'b1}} : ext_cnt[Width-1:0];

     // Clock gate flops when in saturation, and do not
     // count if both incr_en and decr_en are asserted.
     logic cnt_en;
     assign cnt_en = (incr_en ^ decr_en) &&
                     ((incr_en && !(&cnt_q[k])) ||
                     (decr_en && !(cnt_q[k] == '0)));

     // Counter muxes
     assign cnt_d[k] = (clr_i)  ? ResetValues[k] :
                       (set_i)  ? set_val        :
                       (cnt_en) ? cnt_sat        : cnt_q[k];

     logic [Width-1:0] cnt_unforced_q;
     prim_flop #(
       .Width(Width),
       .ResetValue(ResetValues[k])
     ) u_cnt_flop (
       .clk_i,
       .rst_ni,
       .d_i(cnt_d[k]),
       .q_o(cnt_unforced_q)
     );

     // fpv_force is only used during FPV.
     assign cnt_q[k] = fpv_force[k] + cnt_unforced_q;
   end

   // The sum of both counters must always equal the counter maximum.
   logic [Width:0] sum;
   assign sum = (cnt_q[0] + cnt_q[1]);
   assign err_o = (sum != {1'b0, {Width{1'b1}}});

   // Output count values
   assign cnt_o      = cnt_q[0];
   assign cnt_next_o = cnt_d[0];

   ////////////////
   // Assertions //
   ////////////////
 `ifdef INC_ASSERT
   //VCS coverage off
   // pragma coverage off

   // We need to disable most assertions in that case using a helper signal.
   // We can't rely on err_o since some error patterns cannot be detected (e.g. all error
   // patterns that still fullfill the sum constraint).
   logic fpv_err_present;
   assign fpv_err_present = |fpv_force;

   // Helper functions for assertions.
   function automatic logic signed [Width+1:0] max(logic signed [Width+1:0] a,
                                                   logic signed [Width+1:0] b);
     return (a > b) ? a : b;
   endfunction

   function automatic logic signed [Width+1:0] min(logic signed [Width+1:0] a,
                                                   logic signed [Width+1:0] b);
     return (a < b) ? a : b;
   endfunction
   //VCS coverage on
   // pragma coverage on

   // Cnt next
   `ASSERT(CntNext_A,
       rst_ni
       |=>
       cnt_o == $past(cnt_next_o),
       clk_i, err_o || fpv_err_present || !rst_ni)

   // Clear
   `ASSERT(ClrFwd_A,
       rst_ni && clr_i
       |=>
       (cnt_o == ResetValue) &&
       (cnt_q[1] == ({Width{1'b1}} - ResetValue)),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(ClrBkwd_A,
       rst_ni && !(incr_en_i || decr_en_i || set_i) ##1
       $changed(cnt_o) && $changed(cnt_q[1])
       |->
       $past(clr_i),
       clk_i, err_o || fpv_err_present || !rst_ni)

   // Set
   `ASSERT(SetFwd_A,
       rst_ni && set_i && !clr_i
       |=>
       (cnt_o == $past(set_cnt_i)) &&
       (cnt_q[1] == ({Width{1'b1}} - $past(set_cnt_i))),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(SetBkwd_A,
       rst_ni && !(incr_en_i || decr_en_i || clr_i) ##1
       $changed(cnt_o) && $changed(cnt_q[1])
       |->
       $past(set_i),
       clk_i, err_o || fpv_err_present || !rst_ni)

   // Do not count if both increment and decrement are asserted.
   `ASSERT(IncrDecrUpDnCnt_A,
       rst_ni && incr_en_i && decr_en_i && !(clr_i || set_i)
       |=>
       $stable(cnt_o) && $stable(cnt_q[1]),
       clk_i, err_o || fpv_err_present || !rst_ni)

   // Up counter
   `ASSERT(IncrUpCnt_A,
       rst_ni && incr_en_i && !(clr_i || set_i || decr_en_i)
       |=>
       cnt_o == min($past(cnt_o) + $past({2'b0, step_i}), {2'b0, {Width{1'b1}}}),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(IncrDnCnt_A,
       rst_ni && incr_en_i && !(clr_i || set_i || decr_en_i)
       |=>
       cnt_q[1] == max($past(signed'({2'b0, cnt_q[1]})) - $past({2'b0, step_i}), '0),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(UpCntIncrStable_A,
       incr_en_i && !(clr_i || set_i || decr_en_i) &&
       cnt_o == {Width{1'b1}}
       |=>
       $stable(cnt_o),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(UpCntDecrStable_A,
       decr_en_i && !(clr_i || set_i || incr_en_i) &&
       cnt_o == '0
       |=>
       $stable(cnt_o),
       clk_i, err_o || fpv_err_present || !rst_ni)

   // Down counter
   `ASSERT(DecrUpCnt_A,
       rst_ni && decr_en_i && !(clr_i || set_i || incr_en_i)
       |=>
       cnt_o == max($past(signed'({2'b0, cnt_o})) - $past({2'b0, step_i}), '0),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(DecrDnCnt_A,
       rst_ni && decr_en_i && !(clr_i || set_i || incr_en_i)
       |=>
       cnt_q[1] == min($past(cnt_q[1]) + $past({2'b0, step_i}), {2'b0, {Width{1'b1}}}),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(DnCntIncrStable_A,
       rst_ni && incr_en_i && !(clr_i || set_i || decr_en_i) &&
       cnt_q[1] == '0
       |=>
       $stable(cnt_q[1]),
       clk_i, err_o || fpv_err_present || !rst_ni)
   `ASSERT(DnCntDecrStable_A,
       rst_ni && decr_en_i && !(clr_i || set_i || incr_en_i) &&
       cnt_q[1] == {Width{1'b1}}
       |=>
       $stable(cnt_q[1]),
       clk_i, err_o || fpv_err_present || !rst_ni)

   // Error
   `ASSERT(CntErrForward_A,
       (cnt_q[1] + cnt_q[0]) != {Width{1'b1}}
       |->
       err_o)
   `ASSERT(CntErrBackward_A,
       err_o
       |->
       (cnt_q[1] + cnt_q[0]) != {Width{1'b1}})

   // This logic that will be assign to one, when user adds macro
   // ASSERT_PRIM_COUNT_ERROR_TRIGGER_ALERT to check the error with alert, in case that prim_count
   // is used in design without adding this assertion check.
   logic unused_assert_connected;

   `ASSERT_INIT_NET(AssertConnected_A, unused_assert_connected === 1'b1 || !EnableAlertTriggerSVA)
 `endif

 endmodule // prim_count
	// Copyright lowRISC contributors.
	// Licensed under the Apache License, Version 2.0, see LICENSE for details.
	// SPDX-License-Identifier: Apache-2.0
	//
	// 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. 2**Width-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. 2**Width-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.
	//
	// 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.

	`include "prim_assert.sv"

	module prim_count #(
	parameter int Width = 2,
	// Can be used to reset the counter to a different value than 0, for example when
	// the counter is used as a down-counter.
	parameter logic [Width-1:0] ResetValue = '0,
	// This should only be disabled in special circumstances, for example
	// in non-comportable IPs where an error does not trigger an alert.
	parameter bit EnableAlertTriggerSVA = 1
	) (
	input clk_i,
	input rst_ni,
	input clr_i,
	input set_i,
	input [Width-1:0] set_cnt_i, // Set value for the counter.
	input incr_en_i,
	input decr_en_i,
	input [Width-1:0] step_i, // Increment/decrement step when enabled.
	output logic [Width-1:0] cnt_o, // Current counter state
	output logic [Width-1:0] cnt_next_o, // Next counter state
	output logic err_o
	);

	///////////////////
	// Counter logic //
	///////////////////

	// Reset Values for primary and secondary counters.
	localparam int NumCnt = 2;
	localparam logic [NumCnt-1:0][Width-1:0] ResetValues = {{Width{1'b1}} - ResetValue, // secondary
	ResetValue}; // primary

	logic [NumCnt-1:0][Width-1:0] cnt_d, cnt_q, fpv_force;

	`ifndef FPV_SEC_CM_ON
	// This becomes a free variable in FPV.
	assign fpv_force = '0;
	`endif

	for (genvar k = 0; k < NumCnt; k++) begin : gen_cnts
	// Note that increments / decrements are reversed for the secondary counter.
	logic incr_en, decr_en;
	logic [Width-1:0] set_val;
	if (k == 0) begin : gen_up_cnt
	assign incr_en = incr_en_i;
	assign decr_en = decr_en_i;
	assign set_val = set_cnt_i;
	end else begin : gen_dn_cnt
	assign incr_en = decr_en_i;
	assign decr_en = incr_en_i;
	// The secondary value needs to be adjusted accordingly.
	assign set_val = {Width{1'b1}} - set_cnt_i;
	end

	// Main counter logic
	logic [Width:0] ext_cnt;
	assign ext_cnt = (decr_en) ? {1'b0, cnt_q[k]} - {1'b0, step_i} :
	(incr_en) ? {1'b0, cnt_q[k]} + {1'b0, step_i} : {1'b0, cnt_q[k]};

	// Saturation logic
	logic uflow, oflow;
	assign oflow = incr_en && ext_cnt[Width];
	assign uflow = decr_en && ext_cnt[Width];
	logic [Width-1:0] cnt_sat;
	assign cnt_sat = (uflow) ? '0 :
	(oflow) ? {Width{1'b1}} : ext_cnt[Width-1:0];

	// Clock gate flops when in saturation, and do not
	// count if both incr_en and decr_en are asserted.
	logic cnt_en;
	assign cnt_en = (incr_en ^ decr_en) &&
	((incr_en && !(&cnt_q[k])) \|\|
	(decr_en && !(cnt_q[k] == '0)));

	// Counter muxes
	assign cnt_d[k] = (clr_i) ? ResetValues[k] :
	(set_i) ? set_val :
	(cnt_en) ? cnt_sat : cnt_q[k];

	logic [Width-1:0] cnt_unforced_q;
	prim_flop #(
	.Width(Width),
	.ResetValue(ResetValues[k])
	) u_cnt_flop (
	.clk_i,
	.rst_ni,
	.d_i(cnt_d[k]),
	.q_o(cnt_unforced_q)
	);

	// fpv_force is only used during FPV.
	assign cnt_q[k] = fpv_force[k] + cnt_unforced_q;
	end

	// The sum of both counters must always equal the counter maximum.
	logic [Width:0] sum;
	assign sum = (cnt_q[0] + cnt_q[1]);
	assign err_o = (sum != {1'b0, {Width{1'b1}}});

	// Output count values
	assign cnt_o = cnt_q[0];
	assign cnt_next_o = cnt_d[0];

	////////////////
	// Assertions //
	////////////////
	`ifdef INC_ASSERT
	//VCS coverage off
	// pragma coverage off

	// We need to disable most assertions in that case using a helper signal.
	// We can't rely on err_o since some error patterns cannot be detected (e.g. all error
	// patterns that still fullfill the sum constraint).
	logic fpv_err_present;
	assign fpv_err_present = \|fpv_force;

	// Helper functions for assertions.
	function automatic logic signed [Width+1:0] max(logic signed [Width+1:0] a,
	logic signed [Width+1:0] b);
	return (a > b) ? a : b;
	endfunction

	function automatic logic signed [Width+1:0] min(logic signed [Width+1:0] a,
	logic signed [Width+1:0] b);
	return (a < b) ? a : b;
	endfunction
	//VCS coverage on
	// pragma coverage on

	// Cnt next
	`ASSERT(CntNext_A,
	rst_ni
	\|=>
	cnt_o == $past(cnt_next_o),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)

	// Clear
	`ASSERT(ClrFwd_A,
	rst_ni && clr_i
	\|=>
	(cnt_o == ResetValue) &&
	(cnt_q[1] == ({Width{1'b1}} - ResetValue)),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(ClrBkwd_A,
	rst_ni && !(incr_en_i \|\| decr_en_i \|\| set_i) ##1
	$changed(cnt_o) && $changed(cnt_q[1])
	\|->
	$past(clr_i),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)

	// Set
	`ASSERT(SetFwd_A,
	rst_ni && set_i && !clr_i
	\|=>
	(cnt_o == $past(set_cnt_i)) &&
	(cnt_q[1] == ({Width{1'b1}} - $past(set_cnt_i))),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(SetBkwd_A,
	rst_ni && !(incr_en_i \|\| decr_en_i \|\| clr_i) ##1
	$changed(cnt_o) && $changed(cnt_q[1])
	\|->
	$past(set_i),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)

	// Do not count if both increment and decrement are asserted.
	`ASSERT(IncrDecrUpDnCnt_A,
	rst_ni && incr_en_i && decr_en_i && !(clr_i \|\| set_i)
	\|=>
	$stable(cnt_o) && $stable(cnt_q[1]),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)

	// Up counter
	`ASSERT(IncrUpCnt_A,
	rst_ni && incr_en_i && !(clr_i \|\| set_i \|\| decr_en_i)
	\|=>
	cnt_o == min($past(cnt_o) + $past({2'b0, step_i}), {2'b0, {Width{1'b1}}}),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(IncrDnCnt_A,
	rst_ni && incr_en_i && !(clr_i \|\| set_i \|\| decr_en_i)
	\|=>
	cnt_q[1] == max($past(signed'({2'b0, cnt_q[1]})) - $past({2'b0, step_i}), '0),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(UpCntIncrStable_A,
	incr_en_i && !(clr_i \|\| set_i \|\| decr_en_i) &&
	cnt_o == {Width{1'b1}}
	\|=>
	$stable(cnt_o),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(UpCntDecrStable_A,
	decr_en_i && !(clr_i \|\| set_i \|\| incr_en_i) &&
	cnt_o == '0
	\|=>
	$stable(cnt_o),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)

	// Down counter
	`ASSERT(DecrUpCnt_A,
	rst_ni && decr_en_i && !(clr_i \|\| set_i \|\| incr_en_i)
	\|=>
	cnt_o == max($past(signed'({2'b0, cnt_o})) - $past({2'b0, step_i}), '0),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(DecrDnCnt_A,
	rst_ni && decr_en_i && !(clr_i \|\| set_i \|\| incr_en_i)
	\|=>
	cnt_q[1] == min($past(cnt_q[1]) + $past({2'b0, step_i}), {2'b0, {Width{1'b1}}}),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(DnCntIncrStable_A,
	rst_ni && incr_en_i && !(clr_i \|\| set_i \|\| decr_en_i) &&
	cnt_q[1] == '0
	\|=>
	$stable(cnt_q[1]),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)
	`ASSERT(DnCntDecrStable_A,
	rst_ni && decr_en_i && !(clr_i \|\| set_i \|\| incr_en_i) &&
	cnt_q[1] == {Width{1'b1}}
	\|=>
	$stable(cnt_q[1]),
	clk_i, err_o \|\| fpv_err_present \|\| !rst_ni)

	// Error
	`ASSERT(CntErrForward_A,
	(cnt_q[1] + cnt_q[0]) != {Width{1'b1}}
	\|->
	err_o)
	`ASSERT(CntErrBackward_A,
	err_o
	\|->
	(cnt_q[1] + cnt_q[0]) != {Width{1'b1}})

	// This logic that will be assign to one, when user adds macro
	// ASSERT_PRIM_COUNT_ERROR_TRIGGER_ALERT to check the error with alert, in case that prim_count
	// is used in design without adding this assertion check.
	logic unused_assert_connected;

	`ASSERT_INIT_NET(AssertConnected_A, unused_assert_connected === 1'b1 \|\| !EnableAlertTriggerSVA)
	`endif

	endmodule // prim_count