[prim_lfsr] Add FPV testbench
diff --git a/hw/formal/formal.core b/hw/formal/formal.core
index 4f056fa..979b6b9 100644
--- a/hw/formal/formal.core
+++ b/hw/formal/formal.core
@@ -10,6 +10,7 @@
filesets:
files_rtl_generic:
depend:
+ - lowrisc:fpv:prim_lfsr_fpv
- lowrisc:ip:rv_timer
- lowrisc:ip:hmac
- lowrisc:systems:top_earlgrey
diff --git a/hw/ip/prim/fpv/prim_lfsr_fpv.core b/hw/ip/prim/fpv/prim_lfsr_fpv.core
new file mode 100644
index 0000000..4103c79
--- /dev/null
+++ b/hw/ip/prim/fpv/prim_lfsr_fpv.core
@@ -0,0 +1,21 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+name: "lowrisc:fpv:prim_lfsr_fpv:0.1"
+description: "ALERT_HANDLER FPV target"
+filesets:
+ files_fpv:
+ depend:
+ - lowrisc:prim:all
+ files:
+ - tb/prim_lfsr_tb.sv
+ file_type: systemVerilogSource
+
+targets:
+ default: &default_target
+ toplevel:
+ - tb/prim_lfsr_tb.sv
+ filesets:
+ - files_fpv
+ default_tool: jg
diff --git a/hw/ip/prim/fpv/tb/prim_lfsr_tb.sv b/hw/ip/prim/fpv/tb/prim_lfsr_tb.sv
new file mode 100644
index 0000000..f582c29
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_lfsr_tb.sv
@@ -0,0 +1,64 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Testbench module for prim_lfsr. Intended to use with a formal tool.
+
+module prim_lfsr_tb #(
+ 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,
+ // LFSRs up to this bitwidth are checked for maximum length
+ parameter int unsigned MaxLenSVAThresh = 10
+) (
+ 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
+);
+
+ 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),
+ // disabled for large LFSRs since this becomes prohibitive in runtime
+ .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])
+ );
+ 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),
+ // disabled for large LFSRs since this becomes prohibitive in runtime
+ .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])
+ );
+ end
+
+endmodule : prim_lfsr_tb
