[prim_lfsr] Add external seed input and update port names
This adds an external seed input and updates the port names such that
they are more descriptive. The corresponding FPV and DV testbenches are
updated, and two more SVAs are added in order to bring FPV coverage to
100%.
Signed-off-by: Michael Schaffner <msf@opentitan.org>
diff --git a/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv b/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv
index 87e1e94..d034358 100644
--- a/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv
+++ b/hw/ip/alert_handler/rtl/alert_handler_ping_timer.sv
@@ -55,16 +55,18 @@
logic [31:0] lfsr_state, perm_state;
prim_lfsr #(
- .LfsrDw ( 32 ),
- .InDw ( 1 ),
- .OutDw ( 32 ),
- .Seed ( alert_pkg::LfsrSeed )
+ .LfsrDw ( 32 ),
+ .EntropyDw ( 1 ),
+ .StateOutDw ( 32 ),
+ .DefaultSeed ( alert_pkg::LfsrSeed )
) i_prim_lfsr (
.clk_i,
.rst_ni,
- .en_i ( lfsr_en ),
- .data_i ( entropy_i ),
- .data_o ( lfsr_state )
+ .seed_en_i ( 1'b0 ),
+ .seed_i ( '0 ),
+ .lfsr_en_i ( lfsr_en ),
+ .entropy_i,
+ .state_o ( lfsr_state )
);
for (genvar k = 0; k < 32; k++) begin : gen_perm
diff --git a/hw/ip/prim/doc/prim_lfsr.md b/hw/ip/prim/doc/prim_lfsr.md
index 31b7ad4..627e2f4 100644
--- a/hw/ip/prim/doc/prim_lfsr.md
+++ b/hw/ip/prim/doc/prim_lfsr.md
@@ -18,49 +18,57 @@
## Parameters
-Name | type | Description
-----------|--------|----------------------------------------------------------
-LfsrType | string | LFSR form, can be `"GAL_XOR"` or `"FIB_XNOR"`
-LfsrDw | int | Width of the LFSR
-InDw | int | Width of the entropy input
-OutDw | int | Width of the LFSR state to be output (`lfsr_q[OutDw-1:0]`)
-Seed | logic | Initial state of the LFSR, must be nonzero for XOR and non-all-ones for XNOR forms.
-Custom | logic | Custom polynomial coefficients of length LfsrDw.
-MaxLenSVA | bit | Enables maximum length assertions, use only in sim and FPV.
+Name | type | Description
+-------------|--------|----------------------------------------------------------
+LfsrType | string | LFSR form, can be `"GAL_XOR"` or `"FIB_XNOR"`
+LfsrDw | int | Width of the LFSR
+EntropyDw | int | Width of the entropy input
+StateOutDw | int | Width of the LFSR state to be output (`lfsr_q[StateOutDw-1:0]`)
+DefaultSeed | logic | Initial state of the LFSR, must be nonzero for XOR and non-all-ones for XNOR forms.
+CustomCoeffs | logic | Custom polynomial coefficients of length LfsrDw.
+MaxLenSVA | bit | Enables maximum length assertions, use only in sim and FPV.
## Signal Interfaces
-Name | In/Out | Description
---------------|--------|---------------------------------
-en_i | input | Lfsr enable
-data_i[InDw] | input | Entropy input
-data_o[OutDw] | output | LFSR state output.
+Name | In/Out | Description
+---------------------|--------|---------------------------------
+seed_en_i | input | External seed input enable
+seed_i[LfsrDw] | input | External seed input
+lfsr_en_i | input | Lfsr enable
+entropy_i[EntropyDw] | input | Entropy input
+state_o[StateOutDw] | output | LFSR state output.
# Theory of Opeations
```
- /-----------\
-en_i | |
----------->| lfsr |
- | |
-data_i | LfsrDw | data_o
-=====/====>| LfsrType |=======/=======>
- [InDw] | InDw | [OutDw]
- | OutDw |
- | Seed |
- | Custom |
- | MaxLenSVA |
- | |
- \-----------/
+ /----------------\
+seed_en_i | |
+------------>| lfsr |
+seed_i | |
+=====/======>| LfsrDw |
+ [LfsrDw] | LfsrType |
+lfsr_en_i | EntropyDw |
+------------>| StateOutDw |
+entropy_i | DefaultSeed | state_o
+=====/======>| CustomCoeffs |=====/=======>
+ [EntropyDw] | MaxLenSVA | [StateOutDw]
+ | |
+ \----------------/
```
The LFSR module has an enable input and an additional entropy input that is
-XOR'ed into the LFSR state (connect to zero if this feature is unused). The data
-output contains the lower bits of the LFSR state from `OutDw-1` downto `0`. As
-the entropy input may cause the LFSR to jump into its parasitic state
-(all-zero for XOR, all-ones for XNOR), the LFSR state transition function
-contains a lockup protection which re-seeds the state once this condition is
-detected.
+XOR'ed into the LFSR state (connect to zero if this feature is unused). The
+state output contains the lower bits of the LFSR state from `StateOutDw-1`
+downto `0`. As the entropy input may cause the LFSR to jump into its parasitic
+state (all-zero for XOR, all-ones for XNOR), the LFSR state transition function
+contains a lockup protection which re-seeds the state with `DefaultSeed` once
+this condition is detected.
+
+The LFSR contains an external seed input `seed_i` which can be used to load a
+custom seed into the LFSR by asserting `seed_en_i`. This operation takes
+precedence over internal state updates. If the external seed happens to be a
+parasitic state, the lockup protection feature explained above will reseed the
+LFSR with the `DefaultSeed` in the next cycle.
The LFSR coefficients are taken from an internal set of lookup tables with
precomputed coefficients. Alternatively, a custom polynomial can be provided
diff --git a/hw/ip/prim/dv/prim_lfsr_sim.core b/hw/ip/prim/dv/prim_lfsr_sim.core
index 83eaf03..03b28b2 100644
--- a/hw/ip/prim/dv/prim_lfsr_sim.core
+++ b/hw/ip/prim/dv/prim_lfsr_sim.core
@@ -16,6 +16,7 @@
- lowrisc:dv:common_ifs
files:
- tb/prim_lfsr_tb.sv
+ - tb/prim_lfsr_bind.sv
file_type: systemVerilogSource
targets:
diff --git a/hw/ip/prim/dv/tb/prim_lfsr_bind.sv b/hw/ip/prim/dv/tb/prim_lfsr_bind.sv
new file mode 100644
index 0000000..c90b3ed
--- /dev/null
+++ b/hw/ip/prim/dv/tb/prim_lfsr_bind.sv
@@ -0,0 +1,9 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+module prim_lfsr_bind;
+
+ // nothing to bind here yet
+
+endmodule : prim_lfsr_bind
diff --git a/hw/ip/prim/dv/tb/prim_lfsr_tb.sv b/hw/ip/prim/dv/tb/prim_lfsr_tb.sv
index 70373f2..b0e3522 100644
--- a/hw/ip/prim/dv/tb/prim_lfsr_tb.sv
+++ b/hw/ip/prim/dv/tb/prim_lfsr_tb.sv
@@ -49,30 +49,31 @@
// DUTs
//////////////////////////////////////////////////////
- logic [MaxLfsrDw:0] en, err;
- logic [MaxLfsrDw:MinLfsrDw][MaxLfsrDw-1:0] data_out;
+ logic [MaxLfsrDw:0] lfsr_en, err;
+ logic [MaxLfsrDw:MinLfsrDw][MaxLfsrDw-1:0] state_out;
logic [MaxLfsrDw:MinLfsrDw][MaxLfsrDw-1:0] lfsr_periods;
for (genvar k = MinLfsrDw; k <= MaxLfsrDw; k++) begin : gen_duts
prim_lfsr #(
- .LfsrType(LfsrType),
- .LfsrDw(k),
- .InDw(1),
- .OutDw(k),
- .Seed(k'(SEED)),
- .Custom('0),
+ .LfsrType ( LfsrType ),
+ .LfsrDw ( k ),
+ .EntropyDw ( 1 ),
+ .StateOutDw ( k ),
+ .DefaultSeed ( k'(SEED) ),
// enable internal max length check
- .MaxLenSVA(1'b1)
+ .MaxLenSVA ( 1'b1 )
) i_prim_lfsr (
- .clk_i(clk),
- .rst_ni(rst_n),
- .en_i(en[k]),
- .data_i(1'b0),
- .data_o(data_out[k][k-1:0])
+ .clk_i ( clk ),
+ .rst_ni ( rst_n ),
+ .seed_en_i ( 1'b0 ),
+ .seed_i ( '0 ),
+ .lfsr_en_i ( lfsr_en[k] ),
+ .entropy_i ( 1'b0 ),
+ .state_o ( state_out[k][k-1:0] )
);
if (k < MaxLfsrDw) begin : gen_tie_off
- assign data_out[k][MaxLfsrDw-1:k] = '0;
+ assign state_out[k][MaxLfsrDw-1:k] = '0;
end
// calculate period of LFSR:
@@ -84,8 +85,8 @@
//////////////////////////////////////////////////////
initial begin : p_stimuli
- en = '0;
- err = '0;
+ lfsr_en = '0;
+ err = '0;
main_clk.set_period_ns(CLK_PERIOD);
main_clk.set_active();
@@ -97,7 +98,7 @@
main_clk.wait_clks(10);
// enable all LFSRs
- en = '1;
+ lfsr_en = '1;
$display("Running for 2**%0d-1 cycles...", MaxLfsrDw);
for (longint unsigned k = 0; k <= lfsr_periods[MaxLfsrDw]; k++ ) begin
@@ -106,10 +107,10 @@
for (int unsigned j = MinLfsrDw; j <= MaxLfsrDw; j++) begin
// check if we reached the initial state again
- if (data_out[j] == MaxLfsrDw'(SEED) && en[j]) begin
+ if (state_out[j] == MaxLfsrDw'(SEED) && lfsr_en[j]) begin
// $display("cycle: %d -- lfsr: %d -- %x ?= %x, %x",
- // k, j, data_out[j], SEED, en);
- en[j] = 1'b0;
+ // k, j, state_out[j], SEED, lfsr_en);
+ lfsr_en[j] = 1'b0;
// we expect this to occur only after the maximum length period
if (lfsr_periods[j] == k) begin
$display("Maxlen check for LFSR %0d succeeded!", j);
@@ -124,7 +125,7 @@
main_clk.wait_clks(10);
for (int unsigned j = MinLfsrDw; j <= MaxLfsrDw; j++) begin
- if (en[j]) begin
+ if (lfsr_en[j]) begin
$error("Error LFSR %0d never got back to initial state!", j);
err[j] = 1'b1;
end
diff --git a/hw/ip/prim/fpv/tb/prim_lfsr_fpv.sv b/hw/ip/prim/fpv/tb/prim_lfsr_fpv.sv
index 03a5072..b747edd 100644
--- a/hw/ip/prim/fpv/tb/prim_lfsr_fpv.sv
+++ b/hw/ip/prim/fpv/tb/prim_lfsr_fpv.sv
@@ -5,59 +5,70 @@
// Testbench module for prim_lfsr. Intended to be used with a formal tool.
module prim_lfsr_fpv #(
- parameter int unsigned InDw = 1,
- parameter int unsigned OutDw = 1,
- parameter int unsigned GalXorMinLfsrDw = 4,
- parameter int unsigned GalXorMaxLfsrDw = 64,
- parameter int unsigned FibXnorMinLfsrDw = 3,
- parameter int unsigned FibXnorMaxLfsrDw = 168,
- parameter int unsigned NumDuts = FibXnorMaxLfsrDw - FibXnorMinLfsrDw + 1 +
- GalXorMaxLfsrDw - GalXorMinLfsrDw + 1,
+ // LFSR entropy and output bitwidths (set to 1 here as they are unused)
+ parameter int unsigned EntropyDw = 1,
+ parameter int unsigned StateOutDw = 1,
+ // this specifies the range of differently
+ // parameterized LFSRs to instantiate and check
+ parameter int unsigned GalXorMinLfsrDw = 4,
+ parameter int unsigned GalXorMaxLfsrDw = 64,
+ parameter int unsigned FibXnorMinLfsrDw = 3,
+ parameter int unsigned FibXnorMaxLfsrDw = 168,
// LFSRs up to this bitwidth are checked for maximum length
- parameter int unsigned MaxLenSVAThresh = 10
+ parameter int unsigned MaxLenSVAThresh = 10,
+ // derived params
+ localparam int unsigned GalMaxGtFibMax = GalXorMaxLfsrDw > FibXnorMaxLfsrDw,
+ localparam int unsigned MaxLfsrDw = GalXorMaxLfsrDw * GalMaxGtFibMax +
+ FibXnorMaxLfsrDw * (1 - GalMaxGtFibMax),
+ localparam int unsigned NumDuts = FibXnorMaxLfsrDw - FibXnorMinLfsrDw + 1 +
+ GalXorMaxLfsrDw - GalXorMinLfsrDw + 1
) (
- input clk_i,
- input rst_ni,
- input [NumDuts-1:0] en_i,
- input [NumDuts-1:0][InDw-1:0] data_i,
- output logic [NumDuts-1:0][OutDw-1:0] data_o
+ input clk_i,
+ input rst_ni,
+ input [NumDuts-1:0] load_ext_en_i,
+ input [NumDuts-1:0][MaxLfsrDw-1:0] seed_ext_i,
+ input [NumDuts-1:0] lfsr_en_i,
+ input [NumDuts-1:0][EntropyDw-1:0] entropy_i,
+ output logic [NumDuts-1:0][StateOutDw-1:0] state_o
);
for (genvar k = GalXorMinLfsrDw; k <= GalXorMaxLfsrDw; k++) begin : gen_gal_xor_duts
- prim_lfsr #(
- .LfsrType("GAL_XOR"),
- .LfsrDw(k),
- .InDw(InDw),
- .OutDw(OutDw),
- .Seed(1),
- .Custom('0),
+ localparam int unsigned idx = k - GalXorMinLfsrDw;
+ prim_lfsr #(.LfsrType("GAL_XOR"),
+ .LfsrDw ( k ),
+ .EntropyDw ( EntropyDw ),
+ .StateOutDw ( StateOutDw ),
+ .DefaultSeed ( 1 ),
// disabled for large LFSRs since this becomes prohibitive in runtime
- .MaxLenSVA(k <= MaxLenSVAThresh)
+ .MaxLenSVA ( k <= MaxLenSVAThresh )
) i_prim_lfsr (
.clk_i,
.rst_ni,
- .en_i(en_i[k-GalXorMinLfsrDw]),
- .data_i(data_i[k-GalXorMinLfsrDw]),
- .data_o(data_o[k-GalXorMinLfsrDw])
+ .seed_en_i ( load_ext_en_i[idx] ),
+ .seed_i ( k'(seed_ext_i[idx]) ),
+ .lfsr_en_i ( lfsr_en_i[idx] ),
+ .entropy_i ( entropy_i[idx] ),
+ .state_o ( state_o[idx] )
);
end
for (genvar k = FibXnorMinLfsrDw; k <= FibXnorMaxLfsrDw; k++) begin : gen_fib_xnor_duts
- prim_lfsr #(
- .LfsrType("FIB_XNOR"),
- .LfsrDw(k),
- .InDw(InDw),
- .OutDw(OutDw),
- .Seed(1),
- .Custom('0),
+ localparam int unsigned idx = k - FibXnorMinLfsrDw + GalXorMaxLfsrDw - GalXorMinLfsrDw + 1;
+ prim_lfsr #(.LfsrType("FIB_XNOR"),
+ .LfsrDw ( k ),
+ .EntropyDw ( EntropyDw ),
+ .StateOutDw ( StateOutDw ),
+ .DefaultSeed ( 1 ),
// disabled for large LFSRs since this becomes prohibitive in runtime
- .MaxLenSVA(k <= MaxLenSVAThresh)
+ .MaxLenSVA ( k <= MaxLenSVAThresh )
) i_prim_lfsr (
.clk_i,
.rst_ni,
- .en_i(en_i[k - FibXnorMinLfsrDw + GalXorMaxLfsrDw - GalXorMinLfsrDw + 1]),
- .data_i(data_i[k - FibXnorMinLfsrDw + GalXorMaxLfsrDw - GalXorMinLfsrDw + 1]),
- .data_o(data_o[k - FibXnorMinLfsrDw + GalXorMaxLfsrDw - GalXorMinLfsrDw + 1])
+ .seed_en_i ( load_ext_en_i[idx] ),
+ .seed_i ( k'(seed_ext_i[idx]) ),
+ .lfsr_en_i ( lfsr_en_i[idx] ),
+ .entropy_i ( entropy_i[idx] ),
+ .state_o ( state_o[idx] )
);
end
diff --git a/hw/ip/prim/rtl/prim_lfsr.sv b/hw/ip/prim/rtl/prim_lfsr.sv
index bb36fe9..de09f7d 100644
--- a/hw/ip/prim/rtl/prim_lfsr.sv
+++ b/hw/ip/prim/rtl/prim_lfsr.sv
@@ -13,7 +13,10 @@
//
// 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.
+// 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.
//
@@ -23,25 +26,27 @@
module prim_lfsr #(
// Lfsr Type, can be FIB_XNOR or GAL_XOR
- parameter LfsrType = "GAL_XOR",
+ parameter LfsrType = "GAL_XOR",
// Lfsr width
- parameter int unsigned LfsrDw = 32,
- // Width of input to be XOR'd into state (lfsr_q[InDw-1:0])
- parameter int unsigned InDw = 8,
- // Width of output tap (from lfsr_q[OutDw-1:0])
- parameter int unsigned OutDw = 8,
+ parameter int unsigned LfsrDw = 32,
+ // 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] Seed = LfsrDw'(1),
+ parameter logic [LfsrDw-1:0] DefaultSeed = LfsrDw'(1),
// Custom polynomial coeffs
- parameter logic [LfsrDw-1:0] Custom = '0,
+ parameter logic [LfsrDw-1:0] CustomCoeffs = '0,
// Enable this for DV, disable this for long LFSRs in FPV
- parameter bit MaxLenSVA = 1'b1
+ parameter bit MaxLenSVA = 1'b1
) (
- input clk_i,
- input rst_ni,
- input en_i,
- input [InDw-1:0] data_i,
- output logic [OutDw-1:0] data_o
+ 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 get-lfsr-coeffs.py script
@@ -290,8 +295,8 @@
if (LfsrType == "GAL_XOR") begin : gen_gal_xor
// if custom polynomial is provided
- if (Custom) begin : gen_custom
- assign coeffs = Custom[LfsrDw-1:0];
+ if (CustomCoeffs) 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
@@ -300,13 +305,13 @@
end
// calculate next state using internal XOR feedback and entropy input
- assign next_lfsr_state = LfsrDw'(data_i) ^ ({LfsrDw{lfsr_q[0]}} & coeffs) ^ (lfsr_q >> 1);
+ 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(SeedNzCheck_A, |Seed)
+ `ASSERT_INIT(DefaultSeedNzCheck_A, |DefaultSeed)
////////////////////
@@ -315,8 +320,8 @@
end else if (LfsrType == "FIB_XNOR") begin : gen_fib_xnor
// if custom polynomial is provided
- if (Custom) begin : gen_custom
- assign coeffs = Custom[LfsrDw-1:0];
+ if (CustomCoeffs) 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
@@ -325,13 +330,13 @@
end
// calculate next state using external XNOR feedback and entropy input
- assign next_lfsr_state = LfsrDw'(data_i) ^ {lfsr_q[LfsrDw-2:0], ~(^(lfsr_q & coeffs))};
+ 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(SeedNzCheck_A, !(&Seed))
+ `ASSERT_INIT(DefaultSeedNzCheck_A, !(&DefaultSeed))
/////////////
@@ -346,15 +351,16 @@
// Shared logic //
//////////////////
- assign lfsr_d = (en_i && lockup) ? Seed :
- (en_i) ? next_lfsr_state :
- lfsr_q;
+ assign lfsr_d = (seed_en_i) ? seed_i :
+ (lfsr_en_i && lockup) ? DefaultSeed :
+ (lfsr_en_i) ? next_lfsr_state :
+ lfsr_q;
- assign data_o = lfsr_q[OutDw-1:0];
+ assign state_o = lfsr_q[StateOutDw-1:0];
always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
if (!rst_ni) begin
- lfsr_q <= Seed;
+ lfsr_q <= DefaultSeed;
end else begin
lfsr_q <= lfsr_d;
end
@@ -365,32 +371,32 @@
// shared assertions //
///////////////////////
- `ASSERT_KNOWN(DataKnownO_A, data_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(DataKnownO_A, state_o, clk_i, !rst_ni)
- function automatic logic[LfsrDw-1:0] compute_next_state(logic[LfsrDw-1:0] coeffs,
- logic[InDw-1:0] data,
- logic[LfsrDw-1:0] state);
+ function automatic logic[LfsrDw-1:0] compute_next_state(logic[LfsrDw-1:0] coeffs,
+ logic[EntropyDw-1:0] entropy,
+ logic[LfsrDw-1:0] state);
logic state0;
// Galois XOR
if (LfsrType == "GAL_XOR") begin
if (!state) begin
- state = Seed;
+ state = DefaultSeed;
end else begin
state0 = state[0];
state = state >> 1;
if (state0) state ^= coeffs;
- state ^= LfsrDw'(data);
+ state ^= LfsrDw'(entropy);
end
// Fibonacci XNOR
end else if (LfsrType == "FIB_XNOR") begin
if (&state) begin
- state = Seed;
+ state = DefaultSeed;
end else begin
state0 = ~(^(state & coeffs));
state = state << 1;
state[0] = state0;
- state ^= LfsrDw'(data);
+ state ^= LfsrDw'(entropy);
end
end else begin
$error("unknown lfsr type");
@@ -399,18 +405,27 @@
return state;
endfunction : compute_next_state
- `ASSERT_INIT(InputWidth_A, LfsrDw >= InDw)
- `ASSERT_INIT(OutputWidth_A, LfsrDw >= OutDw)
+ `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw)
+ `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw)
// check that a stuck LFSR is correctly reseeded
- `ASSERT(LfsrLockupCheck_A, en_i && lockup |=> !lockup, clk_i, !rst_ni)
+ `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup,
+ clk_i, !rst_ni)
// MSB must be one in any case
`ASSERT(CoeffCheck_A, coeffs[LfsrDw-1], clk_i, !rst_ni)
// check whether next state is computed correctly
- `ASSERT(NextStateCheck_A, en_i |=> lfsr_q ==
- compute_next_state(coeffs, $past(data_i,1), $past(lfsr_q,1)),
+ `ASSERT(NextStateCheck_A, lfsr_en_i && !seed_en_i |=> lfsr_q ==
+ compute_next_state(coeffs, $past(entropy_i,1), $past(lfsr_q,1)),
clk_i, !rst_ni )
+ // check that external seed is correctly loaded into the state
+ `ASSERT(ExtDefaultSeedInputCheck_A, seed_en_i |=> lfsr_q == $past(seed_i),
+ clk_i, !rst_ni)
+
+ // output check
+ `ASSERT_KNOWN(OutputKnown_A, state_o, clk_i, !rst_ni)
+ `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q), clk_i, !rst_ni)
+
// the code below is not meant to be synthesized,
// but it is intended to be used in simulation and FPV
// the formal tool defines SYNTHESIS, hence this workaround
@@ -428,29 +443,31 @@
// 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 data_set_d, data_set_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 = (en_i && lockup) ? '0 :
- (en_i && (cnt_q == cmp_val)) ? '0 :
- (en_i) ? cnt_q + 1'b1 :
- cnt_q;
+ 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 data_set_d = data_set_q | (|data_i);
+ 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;
- data_set_q <= 1'b0;
+ cnt_q <= '0;
+ perturbed_q <= 1'b0;
end else begin
- cnt_q <= cnt_d;
- data_set_q <= data_set_d;
+ cnt_q <= cnt_d;
+ perturbed_q <= perturbed_d;
end
end
- `ASSERT(MaximalLengthCheck0_A, cnt_q == 0 |-> lfsr_q == Seed, clk_i, !rst_ni || data_set_q)
- `ASSERT(MaximalLengthCheck1_A, cnt_q != 0 |-> lfsr_q != Seed, clk_i, !rst_ni || data_set_q)
+ `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)
end
endmodule
