[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