| // Copyright lowRISC contributors. |
| // Licensed under the Apache License, Version 2.0, see LICENSE for details. |
| // SPDX-License-Identifier: Apache-2.0 |
| // |
| // Primitive hardened counter module |
| // |
| // This module implements two styles of hardened counting |
| // 1. Duplicate count |
| // There are two copies of the relevant counter and they are constantly compared. |
| // 2. Cross count |
| // There is an up count and a down count, and the combined value must always |
| // combine to the same value |
| // |
| // This counter supports a generic clr / set / en interface. |
| // When clr_i is set, the counter clears to 0 |
| // When set_i is set, the down count (if enabled) will set to the max value |
| // When neither of the above is set, increment the up count(s) or decrement the down count. |
| // |
| // Note there are many other flavor of functions that can be added, but this primitive |
| // module initially favors the usage inside keymgr and flash_ctrl. |
| // |
| // The usage of set_cnt_i is as follows: |
| // When doing CrossCnt, set_cnt_i sets the maximum value as well as the starting value of down_cnt. |
| // When doing DupCnt, set_cnt_i sets the starting value of up_cnt. Note during DupCnt, the maximum |
| // value is just the max possible value given the counter width. |
| |
| module prim_count import prim_count_pkg::*; #( |
| parameter int Width = 2, |
| parameter bit OutSelDnCnt = 1, // 0 selects up count |
| parameter prim_count_style_e CntStyle = CrossCnt |
| ) ( |
| input clk_i, |
| input rst_ni, |
| input clr_i, |
| input set_i, |
| input [Width-1:0] set_cnt_i, |
| input en_i, |
| input [Width-1:0] step_i, // increment/decrement step when enabled |
| output logic [Width-1:0] cnt_o, |
| output logic err_o |
| ); |
| |
| // if output selects downcount, it MUST be the cross count style |
| `ASSERT_INIT(CntStyleMatch_A, OutSelDnCnt ? CntStyle == CrossCnt : 1'b1) |
| |
| localparam int CntCopies = (CntStyle == DupCnt) ? 2 : 1; |
| |
| // clear up count whenever there is an explicit clear, or |
| // when the max value is re-set during cross count. |
| logic clr_up_cnt; |
| assign clr_up_cnt = clr_i | |
| set_i & CntStyle == CrossCnt; |
| |
| // set up count to desired value only during duplicate counts. |
| logic set_up_cnt; |
| assign set_up_cnt = set_i & CntStyle == DupCnt; |
| |
| |
| cmp_valid_e cmp_valid; |
| logic [CntCopies-1:0][Width-1:0] up_cnt_d, up_cnt_d_buf; |
| logic [CntCopies-1:0][Width-1:0] up_cnt_q; |
| logic [Width-1:0] max_val; |
| logic err; |
| |
| always_ff @(posedge clk_i or negedge rst_ni) begin |
| if (!rst_ni) begin |
| max_val <= '{default: '1}; |
| end else if (set_i && (CntStyle == CrossCnt)) begin |
| max_val <= set_cnt_i; |
| end |
| end |
| |
| for (genvar i = 0; i < CntCopies; i++) begin : gen_cnts |
| // up-count |
| assign up_cnt_d[i] = (clr_up_cnt) ? '0 : |
| (set_up_cnt) ? set_cnt_i : |
| (en_i & up_cnt_q[i] < max_val) ? up_cnt_q[i] + step_i : |
| up_cnt_q[i]; |
| |
| prim_buf #( |
| .Width(Width) |
| ) u_buf ( |
| .in_i(up_cnt_d[i]), |
| .out_o(up_cnt_d_buf[i]) |
| ); |
| |
| prim_flop #( |
| .Width(Width), |
| .ResetValue('0) |
| ) u_cnt_flop ( |
| .clk_i, |
| .rst_ni, |
| .d_i(up_cnt_d_buf[i]), |
| .q_o(up_cnt_q[i]) |
| ); |
| end |
| |
| if (CntStyle == CrossCnt) begin : gen_cross_cnt_hardening |
| logic [Width-1:0] down_cnt; |
| logic [Width-1:0] sum; |
| |
| always_ff @(posedge clk_i or negedge rst_ni) begin |
| if (!rst_ni) begin |
| cmp_valid <= CmpInvalid; |
| end else if (clr_i) begin |
| cmp_valid <= CmpInvalid; |
| end else if ((cmp_valid == CmpInvalid) && set_i) begin |
| cmp_valid <= CmpValid; |
| end |
| end |
| |
| // down-count |
| always_ff @(posedge clk_i or negedge rst_ni) begin |
| if (!rst_ni) begin |
| down_cnt <= '0; |
| end else if (clr_i) begin |
| down_cnt <= '0; |
| end else if (set_i) begin |
| down_cnt <= set_cnt_i; |
| end else if (en_i && down_cnt > '0) begin |
| down_cnt <= down_cnt - step_i; |
| end |
| end |
| |
| logic msb; |
| assign {msb, sum} = down_cnt + up_cnt_q[0]; |
| assign cnt_o = OutSelDnCnt ? down_cnt : up_cnt_q[0]; |
| assign err = max_val != sum | msb; |
| |
| `ASSERT(CrossCntErrForward_A, |
| (cmp_valid == CmpValid) && ((down_cnt + up_cnt_q[0]) != {1'b0, max_val}) |-> err_o) |
| `ASSERT(CrossCntErrBackward_A, err_o |-> |
| (cmp_valid == CmpValid) && ((down_cnt + up_cnt_q[0]) != {1'b0, max_val})) |
| |
| end else if (CntStyle == DupCnt) begin : gen_dup_cnt_hardening |
| // duplicate count compare is always valid |
| assign cmp_valid = CmpValid; |
| assign cnt_o = up_cnt_q[0]; |
| assign err = (up_cnt_q[0] != up_cnt_q[1]); |
| |
| `ASSERT(DupCntErrForward_A, up_cnt_q[0] != up_cnt_q[1] |-> err_o) |
| `ASSERT(DupCntErrBackward_A, err_o |-> up_cnt_q[0] != up_cnt_q[1]) |
| end |
| |
| // If the compare flag is not a valid enum, treat it like an error |
| assign err_o = (cmp_valid == CmpValid) ? err : |
| (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; |
| always_ff @(posedge clk_i or negedge rst_ni) begin |
| if (!rst_ni) begin |
| past_cnt_o <= cnt_o; |
| past_step_i <= step_i; |
| end else if (en_i) begin |
| past_cnt_o <= cnt_o; |
| past_step_i <= step_i; |
| end |
| end |
| `endif |
| |
| // Clear and set should not be seen at the same time |
| `ASSUME(SimulClrSet_A, clr_i || set_i |-> clr_i != set_i) |
| |
| `ASSERT(OutClr_A, clr_i |=> cnt_o == 0) |
| |
| // When `en_i` is set without `clr_i` and `set_i`, and counter does not reach max/min value, |
| // we expect `cnt_o` to increment or decrement base on `step_i`. |
| `ASSERT(OutStep_A, |
| !(clr_i ||set_i) throughout en_i ##[1:$] en_i && max_val > cnt_o && cnt_o > 0 |-> |
| (CntStyle == DupCnt || !OutSelDnCnt) ? cnt_o - past_cnt_o == past_step_i : |
| past_cnt_o - cnt_o == past_step_i) |
| |
| // When `set_i` is set, at next clock cycle: |
| // 1). For duplicate counter, sets the `cnt_o` to `set_cnt_i`. |
| // 2). For cross up counter, sets the `max_value` to `set_cnt_i`. |
| // 3). For cross down counter, sets the `cnt_o` and `max_value` to `set_cnt_i`. |
| `ASSERT(OutSet_A, ##1 set_i |=> |
| (CntStyle == DupCnt || OutSelDnCnt) ? cnt_o == $past(set_cnt_i) : cnt_o == 0) |
| |
| // 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. |
| `ifdef INC_ASSERT |
| logic unused_assert_connected; |
| `ASSERT_INIT(AssertConnected_A, unused_assert_connected === 1'b1) |
| `endif |
| endmodule // prim_count |
| |
| `define ASSERT_PRIM_COUNT_ERROR_TRIGGER_ALERT(NAME_, PRIM_HIER_, ALERT_, MAX_CYCLES_ = 5) \ |
| `ASSERT(NAME_, $rose(PRIM_HIER_.err_o) |-> ##[1:MAX_CYCLES_] $rose(ALERT_.alert_p)) \ |
| `ifdef INC_ASSERT \ |
| assign PRIM_HIER_.unused_assert_connected = 1'b1; \ |
| `endif |
