| // Copyright lowRISC contributors. |
| // Licensed under the Apache License, Version 2.0, see LICENSE for details. |
| // SPDX-License-Identifier: Apache-2.0 |
| // |
| // This module implements different LFSR types: |
| // |
| // 0) Galois XOR type LFSR ([1], internal XOR gates, very fast). |
| // Parameterizable width from 4 to 64 bits. |
| // Coefficients obtained from [2]. |
| // |
| // 1) Fibonacci XNOR type LFSR, parameterizable from 3 to 168 bits. |
| // Coefficients obtained from [3]. |
| // |
| // All flavors have an additional entropy input and lockup protection, which |
| // reseeds the state once it has accidentally fallen into the all-zero (XOR) or |
| // all-one (XNOR) state. Further, an external seed can be loaded into the LFSR |
| // state at runtime. If that seed is all-zero (XOR case) or all-one (XNOR case), |
| // the state will be reseeded in the next cycle using the lockup protection mechanism. |
| // Note that the external seed input takes precedence over internal state updates. |
| // |
| // All polynomials up to 34 bit in length have been verified in simulation. |
| // |
| // Refs: [1] https://en.wikipedia.org/wiki/Linear-feedback_shift_register |
| // [2] https://users.ece.cmu.edu/~koopman/lfsr/ |
| // [3] https://www.xilinx.com/support/documentation/application_notes/xapp052.pdf |
| |
| `include "prim_assert.sv" |
| |
| module prim_lfsr #( |
| // Lfsr Type, can be FIB_XNOR or GAL_XOR |
| parameter LfsrType = "GAL_XOR", |
| // Lfsr width |
| parameter int unsigned LfsrDw = 32, |
| // Derived parameter, do not override |
| localparam int unsigned LfsrIdxDw = $clog2(LfsrDw), |
| // Width of the entropy input to be XOR'd into state (lfsr_q[EntropyDw-1:0]) |
| parameter int unsigned EntropyDw = 8, |
| // Width of output tap (from lfsr_q[StateOutDw-1:0]) |
| parameter int unsigned StateOutDw = 8, |
| // Lfsr reset state, must be nonzero! |
| parameter logic [LfsrDw-1:0] DefaultSeed = LfsrDw'(1), |
| // Custom polynomial coeffs |
| parameter logic [LfsrDw-1:0] CustomCoeffs = '0, |
| // If StatePermEn is set to 1, the custom permutation specified via StatePerm is applied to the |
| // state output, in order to break linear shifting patterns of the LFSR. Note that this |
| // permutation represents a way of customizing the LFSR via a random netlist constant. This is |
| // different from the NonLinearOut feature below which just transforms the output non-linearly |
| // with a fixed function. In most cases, designers should consider enabling StatePermEn as it |
| // comes basically "for free" in terms of area and timing impact. NonLinearOut on the other hand |
| // has area and timing implications and designers should consider whether the use of that feature |
| // is justified. |
| parameter bit StatePermEn = 1'b0, |
| parameter logic [LfsrDw-1:0][LfsrIdxDw-1:0] StatePerm = '0, |
| // Enable this for DV, disable this for long LFSRs in FPV |
| parameter bit MaxLenSVA = 1'b1, |
| // Can be disabled in cases where seed and entropy |
| // inputs are unused in order to not distort coverage |
| // (the SVA will be unreachable in such cases) |
| parameter bit LockupSVA = 1'b1, |
| parameter bit ExtSeedSVA = 1'b1, |
| // Introduce non-linearity to lfsr output. Note, unlike StatePermEn, this feature is not "for |
| // free". Please double check that this feature is indeed required. Also note that this feature |
| // is only available for LFSRs that have a power-of-two width greater or equal 16bit. |
| parameter bit NonLinearOut = 1'b0 |
| ) ( |
| input clk_i, |
| input rst_ni, |
| input seed_en_i, // load external seed into the state (takes precedence) |
| input [LfsrDw-1:0] seed_i, // external seed input |
| input lfsr_en_i, // enables the LFSR |
| input [EntropyDw-1:0] entropy_i, // additional entropy to be XOR'ed into the state |
| output logic [StateOutDw-1:0] state_o // (partial) LFSR state output |
| ); |
| |
| // automatically generated with util/design/get-lfsr-coeffs.py script |
| localparam int unsigned GAL_XOR_LUT_OFF = 4; |
| localparam logic [63:0] GAL_XOR_COEFFS [61] = |
| '{ 64'h9, |
| 64'h12, |
| 64'h21, |
| 64'h41, |
| 64'h8E, |
| 64'h108, |
| 64'h204, |
| 64'h402, |
| 64'h829, |
| 64'h100D, |
| 64'h2015, |
| 64'h4001, |
| 64'h8016, |
| 64'h10004, |
| 64'h20013, |
| 64'h40013, |
| 64'h80004, |
| 64'h100002, |
| 64'h200001, |
| 64'h400010, |
| 64'h80000D, |
| 64'h1000004, |
| 64'h2000023, |
| 64'h4000013, |
| 64'h8000004, |
| 64'h10000002, |
| 64'h20000029, |
| 64'h40000004, |
| 64'h80000057, |
| 64'h100000029, |
| 64'h200000073, |
| 64'h400000002, |
| 64'h80000003B, |
| 64'h100000001F, |
| 64'h2000000031, |
| 64'h4000000008, |
| 64'h800000001C, |
| 64'h10000000004, |
| 64'h2000000001F, |
| 64'h4000000002C, |
| 64'h80000000032, |
| 64'h10000000000D, |
| 64'h200000000097, |
| 64'h400000000010, |
| 64'h80000000005B, |
| 64'h1000000000038, |
| 64'h200000000000E, |
| 64'h4000000000025, |
| 64'h8000000000004, |
| 64'h10000000000023, |
| 64'h2000000000003E, |
| 64'h40000000000023, |
| 64'h8000000000004A, |
| 64'h100000000000016, |
| 64'h200000000000031, |
| 64'h40000000000003D, |
| 64'h800000000000001, |
| 64'h1000000000000013, |
| 64'h2000000000000034, |
| 64'h4000000000000001, |
| 64'h800000000000000D }; |
| |
| // automatically generated with get-lfsr-coeffs.py script |
| localparam int unsigned FIB_XNOR_LUT_OFF = 3; |
| localparam logic [167:0] FIB_XNOR_COEFFS [166] = |
| '{ 168'h6, |
| 168'hC, |
| 168'h14, |
| 168'h30, |
| 168'h60, |
| 168'hB8, |
| 168'h110, |
| 168'h240, |
| 168'h500, |
| 168'h829, |
| 168'h100D, |
| 168'h2015, |
| 168'h6000, |
| 168'hD008, |
| 168'h12000, |
| 168'h20400, |
| 168'h40023, |
| 168'h90000, |
| 168'h140000, |
| 168'h300000, |
| 168'h420000, |
| 168'hE10000, |
| 168'h1200000, |
| 168'h2000023, |
| 168'h4000013, |
| 168'h9000000, |
| 168'h14000000, |
| 168'h20000029, |
| 168'h48000000, |
| 168'h80200003, |
| 168'h100080000, |
| 168'h204000003, |
| 168'h500000000, |
| 168'h801000000, |
| 168'h100000001F, |
| 168'h2000000031, |
| 168'h4400000000, |
| 168'hA000140000, |
| 168'h12000000000, |
| 168'h300000C0000, |
| 168'h63000000000, |
| 168'hC0000030000, |
| 168'h1B0000000000, |
| 168'h300003000000, |
| 168'h420000000000, |
| 168'hC00000180000, |
| 168'h1008000000000, |
| 168'h3000000C00000, |
| 168'h6000C00000000, |
| 168'h9000000000000, |
| 168'h18003000000000, |
| 168'h30000000030000, |
| 168'h40000040000000, |
| 168'hC0000600000000, |
| 168'h102000000000000, |
| 168'h200004000000000, |
| 168'h600003000000000, |
| 168'hC00000000000000, |
| 168'h1800300000000000, |
| 168'h3000000000000030, |
| 168'h6000000000000000, |
| 168'hD800000000000000, |
| 168'h10000400000000000, |
| 168'h30180000000000000, |
| 168'h60300000000000000, |
| 168'h80400000000000000, |
| 168'h140000028000000000, |
| 168'h300060000000000000, |
| 168'h410000000000000000, |
| 168'h820000000001040000, |
| 168'h1000000800000000000, |
| 168'h3000600000000000000, |
| 168'h6018000000000000000, |
| 168'hC000000018000000000, |
| 168'h18000000600000000000, |
| 168'h30000600000000000000, |
| 168'h40200000000000000000, |
| 168'hC0000000060000000000, |
| 168'h110000000000000000000, |
| 168'h240000000480000000000, |
| 168'h600000000003000000000, |
| 168'h800400000000000000000, |
| 168'h1800000300000000000000, |
| 168'h3003000000000000000000, |
| 168'h4002000000000000000000, |
| 168'hC000000000000000018000, |
| 168'h10000000004000000000000, |
| 168'h30000C00000000000000000, |
| 168'h600000000000000000000C0, |
| 168'hC00C0000000000000000000, |
| 168'h140000000000000000000000, |
| 168'h200001000000000000000000, |
| 168'h400800000000000000000000, |
| 168'hA00000000001400000000000, |
| 168'h1040000000000000000000000, |
| 168'h2004000000000000000000000, |
| 168'h5000000000028000000000000, |
| 168'h8000000004000000000000000, |
| 168'h18600000000000000000000000, |
| 168'h30000000000000000C00000000, |
| 168'h40200000000000000000000000, |
| 168'hC0300000000000000000000000, |
| 168'h100010000000000000000000000, |
| 168'h200040000000000000000000000, |
| 168'h5000000000000000A0000000000, |
| 168'h800000010000000000000000000, |
| 168'h1860000000000000000000000000, |
| 168'h3003000000000000000000000000, |
| 168'h4010000000000000000000000000, |
| 168'hA000000000140000000000000000, |
| 168'h10080000000000000000000000000, |
| 168'h30000000000000000000180000000, |
| 168'h60018000000000000000000000000, |
| 168'hC0000000000000000300000000000, |
| 168'h140005000000000000000000000000, |
| 168'h200000001000000000000000000000, |
| 168'h404000000000000000000000000000, |
| 168'h810000000000000000000000000102, |
| 168'h1000040000000000000000000000000, |
| 168'h3000000000000006000000000000000, |
| 168'h5000000000000000000000000000000, |
| 168'h8000000004000000000000000000000, |
| 168'h18000000000000000000000000030000, |
| 168'h30000000030000000000000000000000, |
| 168'h60000000000000000000000000000000, |
| 168'hA0000014000000000000000000000000, |
| 168'h108000000000000000000000000000000, |
| 168'h240000000000000000000000000000000, |
| 168'h600000000000C00000000000000000000, |
| 168'h800000040000000000000000000000000, |
| 168'h1800000000000300000000000000000000, |
| 168'h2000000000000010000000000000000000, |
| 168'h4008000000000000000000000000000000, |
| 168'hC000000000000000000000000000000600, |
| 168'h10000080000000000000000000000000000, |
| 168'h30600000000000000000000000000000000, |
| 168'h4A400000000000000000000000000000000, |
| 168'h80000004000000000000000000000000000, |
| 168'h180000003000000000000000000000000000, |
| 168'h200001000000000000000000000000000000, |
| 168'h600006000000000000000000000000000000, |
| 168'hC00000000000000006000000000000000000, |
| 168'h1000000000000100000000000000000000000, |
| 168'h3000000000000006000000000000000000000, |
| 168'h6000000003000000000000000000000000000, |
| 168'h8000001000000000000000000000000000000, |
| 168'h1800000000000000000000000000C000000000, |
| 168'h20000000000001000000000000000000000000, |
| 168'h48000000000000000000000000000000000000, |
| 168'hC0000000000000006000000000000000000000, |
| 168'h180000000000000000000000000000000000000, |
| 168'h280000000000000000000000000000005000000, |
| 168'h60000000C000000000000000000000000000000, |
| 168'hC00000000000000000000000000018000000000, |
| 168'h1800000600000000000000000000000000000000, |
| 168'h3000000C00000000000000000000000000000000, |
| 168'h4000000080000000000000000000000000000000, |
| 168'hC000300000000000000000000000000000000000, |
| 168'h10000400000000000000000000000000000000000, |
| 168'h30000000000000000000006000000000000000000, |
| 168'h600000000000000C0000000000000000000000000, |
| 168'hC0060000000000000000000000000000000000000, |
| 168'h180000006000000000000000000000000000000000, |
| 168'h3000000000C0000000000000000000000000000000, |
| 168'h410000000000000000000000000000000000000000, |
| 168'hA00140000000000000000000000000000000000000 }; |
| |
| logic lockup; |
| logic [LfsrDw-1:0] lfsr_d, lfsr_q; |
| logic [LfsrDw-1:0] next_lfsr_state, coeffs; |
| |
| |
| //////////////// |
| // Galois XOR // |
| //////////////// |
| if (64'(LfsrType) == 64'("GAL_XOR")) begin : gen_gal_xor |
| |
| // if custom polynomial is provided |
| if (CustomCoeffs > 0) begin : gen_custom |
| assign coeffs = CustomCoeffs[LfsrDw-1:0]; |
| end else begin : gen_lut |
| assign coeffs = GAL_XOR_COEFFS[LfsrDw-GAL_XOR_LUT_OFF][LfsrDw-1:0]; |
| // check that the most significant bit of polynomial is 1 |
| `ASSERT_INIT(MinLfsrWidth_A, LfsrDw >= $low(GAL_XOR_COEFFS)+GAL_XOR_LUT_OFF) |
| `ASSERT_INIT(MaxLfsrWidth_A, LfsrDw <= $high(GAL_XOR_COEFFS)+GAL_XOR_LUT_OFF) |
| end |
| |
| // calculate next state using internal XOR feedback and entropy input |
| assign next_lfsr_state = LfsrDw'(entropy_i) ^ ({LfsrDw{lfsr_q[0]}} & coeffs) ^ (lfsr_q >> 1); |
| |
| // lockup condition is all-zero |
| assign lockup = ~(|lfsr_q); |
| |
| // check that seed is not all-zero |
| `ASSERT_INIT(DefaultSeedNzCheck_A, |DefaultSeed) |
| |
| |
| //////////////////// |
| // Fibonacci XNOR // |
| //////////////////// |
| end else if (64'(LfsrType) == "FIB_XNOR") begin : gen_fib_xnor |
| |
| // if custom polynomial is provided |
| if (CustomCoeffs > 0) begin : gen_custom |
| assign coeffs = CustomCoeffs[LfsrDw-1:0]; |
| end else begin : gen_lut |
| assign coeffs = FIB_XNOR_COEFFS[LfsrDw-FIB_XNOR_LUT_OFF][LfsrDw-1:0]; |
| // check that the most significant bit of polynomial is 1 |
| `ASSERT_INIT(MinLfsrWidth_A, LfsrDw >= $low(FIB_XNOR_COEFFS)+FIB_XNOR_LUT_OFF) |
| `ASSERT_INIT(MaxLfsrWidth_A, LfsrDw <= $high(FIB_XNOR_COEFFS)+FIB_XNOR_LUT_OFF) |
| end |
| |
| // calculate next state using external XNOR feedback and entropy input |
| assign next_lfsr_state = LfsrDw'(entropy_i) ^ {lfsr_q[LfsrDw-2:0], ~(^(lfsr_q & coeffs))}; |
| |
| // lockup condition is all-ones |
| assign lockup = &lfsr_q; |
| |
| // check that seed is not all-ones |
| `ASSERT_INIT(DefaultSeedNzCheck_A, !(&DefaultSeed)) |
| |
| |
| ///////////// |
| // Unknown // |
| ///////////// |
| end else begin : gen_unknown_type |
| assign coeffs = '0; |
| assign next_lfsr_state = '0; |
| assign lockup = 1'b0; |
| `ASSERT_INIT(UnknownLfsrType_A, 0) |
| end |
| |
| |
| ////////////////// |
| // Shared logic // |
| ////////////////// |
| |
| assign lfsr_d = (seed_en_i) ? seed_i : |
| (lfsr_en_i && lockup) ? DefaultSeed : |
| (lfsr_en_i) ? next_lfsr_state : |
| lfsr_q; |
| |
| logic [LfsrDw-1:0] sbox_out; |
| if (NonLinearOut) begin : gen_out_non_linear |
| // The "aligned" permutation ensures that adjacent bits do not go into the same SBox. It is |
| // different from the state permutation that can be specified via the StatePerm parameter. The |
| // permutation taps out 4 SBox input bits at regular stride intervals. E.g., for a 16bit |
| // vector, the input assignment looks as follows: |
| // |
| // SBox0: 0, 4, 8, 12 |
| // SBox1: 1, 5, 9, 13 |
| // SBox2: 2, 6, 10, 14 |
| // SBox3: 3, 7, 11, 15 |
| // |
| // Note that this permutation can be produced by filling the input vector into matrix columns |
| // and reading out the SBox inputs as matrix rows. |
| localparam int NumSboxes = LfsrDw / 4; |
| // Fill in the input vector in col-major order. |
| logic [3:0][NumSboxes-1:0][LfsrIdxDw-1:0] matrix_indices; |
| for (genvar j = 0; j < LfsrDw; j++) begin : gen_input_idx_map |
| assign matrix_indices[j / NumSboxes][j % NumSboxes] = j; |
| end |
| // Due to the LFSR shifting pattern, the above permutation has the property that the output of |
| // SBox(n) is going to be equal to SBox(n+1) in the subsequent cycle (unless the LFSR polynomial |
| // modifies some of the associated shifted bits via an XOR tap). |
| // We therefore tweak this permutation by rotating and reversing some of the assignment matrix |
| // columns. The rotation and reversion operations have been chosen such that this |
| // generalizes to all power of two widths supported by the LFSR primitive. For 16bit, this |
| // looks as follows: |
| // |
| // SBox0: 0, 6, 11, 14 |
| // SBox1: 1, 7, 10, 13 |
| // SBox2: 2, 4, 9, 12 |
| // SBox3: 3, 5, 8, 15 |
| // |
| // This can be achieved by: |
| // 1) down rotating the second column by NumSboxes/2 |
| // 2) reversing the third column |
| // 3) down rotating the fourth column by 1 and reversing it |
| // |
| logic [3:0][NumSboxes-1:0][LfsrIdxDw-1:0] matrix_rotrev_indices; |
| typedef logic [NumSboxes-1:0][LfsrIdxDw-1:0] matrix_col_t; |
| |
| // left-rotates a matrix column by the shift amount |
| function automatic matrix_col_t lrotcol(matrix_col_t col, integer shift); |
| matrix_col_t out; |
| for (int k = 0; k < NumSboxes; k++) begin |
| out[(k + shift) % NumSboxes] = col[k]; |
| end |
| return out; |
| endfunction : lrotcol |
| |
| // reverses a matrix column |
| function automatic matrix_col_t revcol(matrix_col_t col); |
| return {<<LfsrIdxDw{col}}; |
| endfunction : revcol |
| |
| always_comb begin : p_rotrev |
| matrix_rotrev_indices[0] = matrix_indices[0]; |
| matrix_rotrev_indices[1] = lrotcol(matrix_indices[1], NumSboxes/2); |
| matrix_rotrev_indices[2] = revcol(matrix_indices[2]); |
| matrix_rotrev_indices[3] = revcol(lrotcol(matrix_indices[3], 1)); |
| end |
| |
| // Read out the matrix rows and linearize. |
| logic [LfsrDw-1:0][LfsrIdxDw-1:0] sbox_in_indices; |
| for (genvar k = 0; k < LfsrDw; k++) begin : gen_reverse_upper |
| assign sbox_in_indices[k] = matrix_rotrev_indices[k % 4][k / 4]; |
| end |
| |
| `ifndef SYNTHESIS |
| // Check that the permutation is indeed a permutation. |
| logic [LfsrDw-1:0] sbox_perm_test; |
| always_comb begin : p_perm_check |
| sbox_perm_test = '0; |
| for (int k = 0; k < LfsrDw; k++) begin |
| sbox_perm_test[sbox_in_indices[k]] = 1'b1; |
| end |
| end |
| // All bit positions must be marked with 1. |
| `ASSERT(SboxPermutationCheck_A, &sbox_perm_test) |
| `endif |
| |
| `ifdef FPV_ON |
| // Verify that the permutation indeed breaks linear shifting patterns of 4bit input groups. |
| // The symbolic variables let the FPV tool select all sbox index combinations and linear shift |
| // offsets. |
| int shift; |
| int unsigned sk, sj; |
| `ASSUME(SjSkRange_M, (sj < NumSboxes) && (sk < NumSboxes)) |
| `ASSUME(SjSkDifferent_M, sj != sk) |
| `ASSUME(SjSkStable_M, ##1 $stable(sj) && $stable(sk) && $stable(shift)) |
| `ASSERT(SboxInputIndexGroupIsUnique_A, |
| !((((sbox_in_indices[sj * 4 + 0] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 0]) && |
| (((sbox_in_indices[sj * 4 + 1] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 1]) && |
| (((sbox_in_indices[sj * 4 + 2] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 2]) && |
| (((sbox_in_indices[sj * 4 + 3] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 3]))) |
| |
| // this checks that the permutations does not preserve neighboring bit positions. |
| // i.e. no two neighboring bits are mapped to neighboring bit positions. |
| int y; |
| int unsigned ik; |
| `ASSUME(IkYRange_M, (ik < LfsrDw) && (y == 1 || y == -1)) |
| `ASSUME(IkStable_M, ##1 $stable(ik) && $stable(y)) |
| `ASSERT(IndicesNotAdjacent_A, (sbox_in_indices[ik] - sbox_in_indices[(ik + y) % LfsrDw]) != 1) |
| `endif |
| |
| // Use the permutation indices to create the SBox layer |
| for (genvar k = 0; k < NumSboxes; k++) begin : gen_sboxes |
| logic [3:0] sbox_in; |
| assign sbox_in = {lfsr_q[sbox_in_indices[k*4 + 3]], |
| lfsr_q[sbox_in_indices[k*4 + 2]], |
| lfsr_q[sbox_in_indices[k*4 + 1]], |
| lfsr_q[sbox_in_indices[k*4 + 0]]}; |
| assign sbox_out[k*4 +: 4] = prim_cipher_pkg::PRINCE_SBOX4[sbox_in]; |
| end |
| end else begin : gen_out_passthru |
| assign sbox_out = lfsr_q; |
| end |
| |
| // Random output permutation, defined at compile time |
| if (StatePermEn) begin : gen_state_perm |
| |
| for (genvar k = 0; k < StateOutDw; k++) begin : gen_perm_loop |
| assign state_o[k] = sbox_out[StatePerm[k]]; |
| end |
| |
| // if lfsr width is greater than the output, then by definition |
| // not every bit will be picked |
| if (LfsrDw > StateOutDw) begin : gen_tieoff_unused |
| logic unused_sbox_out; |
| assign unused_sbox_out = ^sbox_out; |
| end |
| |
| end else begin : gen_no_state_perm |
| assign state_o = StateOutDw'(sbox_out); |
| end |
| |
| always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg |
| if (!rst_ni) begin |
| lfsr_q <= DefaultSeed; |
| end else begin |
| lfsr_q <= lfsr_d; |
| end |
| end |
| |
| |
| /////////////////////// |
| // shared assertions // |
| /////////////////////// |
| |
| `ASSERT_KNOWN(DataKnownO_A, state_o) |
| |
| // the code below is not meant to be synthesized, |
| // but it is intended to be used in simulation and FPV |
| `ifndef SYNTHESIS |
| function automatic logic [LfsrDw-1:0] compute_next_state(logic [LfsrDw-1:0] lfsrcoeffs, |
| logic [EntropyDw-1:0] entropy, |
| logic [LfsrDw-1:0] current_state); |
| logic state0; |
| logic [LfsrDw-1:0] next_state; |
| |
| next_state = current_state; |
| |
| // Galois XOR |
| if (64'(LfsrType) == 64'("GAL_XOR")) begin |
| if (next_state == 0) begin |
| next_state = DefaultSeed; |
| end else begin |
| state0 = next_state[0]; |
| next_state = next_state >> 1; |
| if (state0) next_state ^= lfsrcoeffs; |
| next_state ^= LfsrDw'(entropy); |
| end |
| // Fibonacci XNOR |
| end else if (64'(LfsrType) == "FIB_XNOR") begin |
| if (&next_state) begin |
| next_state = DefaultSeed; |
| end else begin |
| state0 = ~(^(next_state & lfsrcoeffs)); |
| next_state = next_state << 1; |
| next_state[0] = state0; |
| next_state ^= LfsrDw'(entropy); |
| end |
| end else begin |
| $error("unknown lfsr type"); |
| end |
| |
| return next_state; |
| endfunction : compute_next_state |
| |
| // check whether next state is computed correctly |
| // we shift the assertion by one clock cycle (##1) in order to avoid |
| // erroneous SVA triggers right after reset deassertion in cases where |
| // the precondition is true throughout the reset. |
| // this can happen since the disable_iff evaluates using unsampled values, |
| // meaning that the assertion may already read rst_ni == 1 on an active |
| // clock edge while the flops in the design have not yet changed state. |
| `ASSERT(NextStateCheck_A, ##1 lfsr_en_i && !seed_en_i |=> lfsr_q == |
| compute_next_state(coeffs, $past(entropy_i), $past(lfsr_q))) |
| |
| // Only check this if enabled. |
| if (StatePermEn) begin : gen_perm_check |
| // Check that the supplied permutation is valid. |
| logic [LfsrDw-1:0] lfsr_perm_test; |
| initial begin : p_perm_check |
| lfsr_perm_test = '0; |
| for (int k = 0; k < LfsrDw; k++) begin |
| lfsr_perm_test[StatePerm[k]] = 1'b1; |
| end |
| // All bit positions must be marked with 1. |
| `ASSERT_I(PermutationCheck_A, &lfsr_perm_test) |
| end |
| end |
| |
| `endif |
| |
| `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw) |
| `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw) |
| |
| // MSB must be one in any case |
| `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1]) |
| |
| // output check |
| `ASSERT_KNOWN(OutputKnown_A, state_o) |
| if (!StatePermEn && !NonLinearOut) begin : gen_output_sva |
| `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q)) |
| end |
| // if no external input changes the lfsr state, a lockup must not occur (by design) |
| //`ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni) |
| `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup) |
| |
| // this can be disabled if unused in order to not distort coverage |
| if (ExtSeedSVA) begin : gen_ext_seed_sva |
| // check that external seed is correctly loaded into the state |
| // rst_ni is used directly as part of the pre-condition since the usage of rst_ni |
| // in disable_iff is unsampled. See #1985 for more details |
| `ASSERT(ExtDefaultSeedInputCheck_A, (seed_en_i && rst_ni) |=> lfsr_q == $past(seed_i)) |
| end |
| |
| // if the external seed mechanism is not used, |
| // there is theoretically no way we end up in a lockup condition |
| // in order to not distort coverage, this SVA can be disabled in such cases |
| if (LockupSVA) begin : gen_lockup_mechanism_sva |
| // check that a stuck LFSR is correctly reseeded |
| `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup) |
| end |
| |
| // If non-linear output requested, the LFSR width must be a power of 2 and greater than 16. |
| if(NonLinearOut) begin : gen_nonlinear_align_check_sva |
| `ASSERT_INIT(SboxByteAlign_A, 2**$clog2(LfsrDw) == LfsrDw && LfsrDw >= 16) |
| end |
| |
| if (MaxLenSVA) begin : gen_max_len_sva |
| `ifndef SYNTHESIS |
| // the code below is a workaround to enable long sequences to be checked. |
| // some simulators do not support SVA sequences longer than 2**32-1. |
| logic [LfsrDw-1:0] cnt_d, cnt_q; |
| logic perturbed_d, perturbed_q; |
| logic [LfsrDw-1:0] cmp_val; |
| |
| assign cmp_val = {{(LfsrDw-1){1'b1}}, 1'b0}; // 2**LfsrDw-2 |
| assign cnt_d = (lfsr_en_i && lockup) ? '0 : |
| (lfsr_en_i && (cnt_q == cmp_val)) ? '0 : |
| (lfsr_en_i) ? cnt_q + 1'b1 : |
| cnt_q; |
| |
| assign perturbed_d = perturbed_q | (|entropy_i) | seed_en_i; |
| |
| always_ff @(posedge clk_i or negedge rst_ni) begin : p_max_len |
| if (!rst_ni) begin |
| cnt_q <= '0; |
| perturbed_q <= 1'b0; |
| end else begin |
| cnt_q <= cnt_d; |
| perturbed_q <= perturbed_d; |
| end |
| end |
| |
| `ASSERT(MaximalLengthCheck0_A, cnt_q == 0 |-> lfsr_q == DefaultSeed, |
| clk_i, !rst_ni || perturbed_q) |
| `ASSERT(MaximalLengthCheck1_A, cnt_q != 0 |-> lfsr_q != DefaultSeed, |
| clk_i, !rst_ni || perturbed_q) |
| `endif |
| end |
| |
| endmodule |
