[prim_arbiter_fixed/fpv] Add generated FPV testbench
Signed-off-by: Michael Schaffner <msf@google.com>
diff --git a/hw/formal/fpv_all b/hw/formal/fpv_all
index 44ddb0e..67672c3 100755
--- a/hw/formal/fpv_all
+++ b/hw/formal/fpv_all
@@ -36,6 +36,7 @@
# run formal on dedicated FPV testbenches
"prim_arbiter_ppc_fpv"
"prim_arbiter_tree_fpv"
+ "prim_arbiter_fixed_fpv"
"prim_alert_rxtx_fpv"
"prim_alert_rxtx_async_fpv"
"prim_esc_rxtx_fpv"
diff --git a/hw/ip/prim/fpv/prim_arbiter_fixed_fpv.core b/hw/ip/prim/fpv/prim_arbiter_fixed_fpv.core
new file mode 100644
index 0000000..4264fee
--- /dev/null
+++ b/hw/ip/prim/fpv/prim_arbiter_fixed_fpv.core
@@ -0,0 +1,25 @@
+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_arbiter_fixed_fpv:0.1"
+description: "prim_arbiter_fixed FPV target"
+filesets:
+ files_formal:
+ depend:
+ - lowrisc:prim:all
+ files:
+ - tb/prim_arbiter_fixed_fpv.sv
+ file_type: systemVerilogSource
+
+targets:
+ default: &default_target
+ # note, this setting is just used
+ # to generate a file list for jg
+ default_tool: icarus
+ filesets:
+ - files_formal
+ toplevel: prim_arbiter_fixed_fpv
+
+ formal:
+ <<: *default_target
diff --git a/hw/ip/prim/fpv/tb/prim_arbiter_fixed_fpv.sv b/hw/ip/prim/fpv/tb/prim_arbiter_fixed_fpv.sv
new file mode 100644
index 0000000..b21a1b2
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_arbiter_fixed_fpv.sv
@@ -0,0 +1,43 @@
+// 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_arbiter_fixed.
+// Intended to be used with a formal tool.
+
+module prim_arbiter_fixed_fpv #(
+ parameter int N = 8,
+ parameter int DW = 32,
+ parameter bit EnDataPort = 1,
+ localparam int IdxW = $clog2(N)
+) (
+ input clk_i,
+ input rst_ni,
+ input [N-1:0] req_i,
+ input [DW-1:0]data_i [N],
+ output logic[N-1:0] gnt_o,
+ output logic[IdxW-1:0] idx_o,
+ output logic valid_o,
+ output logic[DW-1:0] data_o,
+ input ready_i
+);
+
+
+ prim_arbiter_fixed #(
+ .N(N),
+ .DW(DW),
+ .EnDataPort(EnDataPort)
+ ) i_prim_arbiter_fixed (
+ .clk_i,
+ .rst_ni,
+ .req_i,
+ .data_i,
+ .gnt_o,
+ .idx_o,
+ .valid_o,
+ .data_o,
+ .ready_i
+ );
+
+
+endmodule : prim_arbiter_fixed_fpv
