[padctrl/fpv] Initial FPV testbench for padctrl
diff --git a/hw/formal/formal.core b/hw/formal/formal.core
index 406bf7f..3208c92 100644
--- a/hw/formal/formal.core
+++ b/hw/formal/formal.core
@@ -23,6 +23,7 @@
- lowrisc:tlul:socket_1n
- lowrisc:tlul:socket_m1
- lowrisc:fpv:pinmux_fpv
+ - lowrisc:fpv:padctrl_fpv
targets:
sim:
diff --git a/hw/formal/fpv_all b/hw/formal/fpv_all
index 43acd7b..af67f96 100755
--- a/hw/formal/fpv_all
+++ b/hw/formal/fpv_all
@@ -31,6 +31,7 @@
"prim_alert_rxtx_async_tb"
"prim_esc_rxtx_tb"
"pinmux_tb"
+ "padctrl_tb"
)
#-------------------------------------------------------------------------
diff --git a/hw/ip/padctrl/fpv/padctrl_fpv.core b/hw/ip/padctrl/fpv/padctrl_fpv.core
new file mode 100644
index 0000000..875fc73
--- /dev/null
+++ b/hw/ip/padctrl/fpv/padctrl_fpv.core
@@ -0,0 +1,23 @@
+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:padctrl_fpv:0.1"
+description: "PADCTRL FPV target"
+filesets:
+ files_fpv:
+ depend:
+ - lowrisc:ip:padctrl
+ files:
+ - tb/padctrl_tb.sv
+ - tb/padctrl_bind.sv
+ - vip/padring_assert.sv
+ file_type: systemVerilogSource
+
+targets:
+ default: &default_target
+ toplevel:
+ - tb/padctrl_tb.sv
+ filesets:
+ - files_fpv
+ default_tool: jg
diff --git a/hw/ip/padctrl/fpv/tb/padctrl_bind.sv b/hw/ip/padctrl/fpv/tb/padctrl_bind.sv
new file mode 100644
index 0000000..fe236ac
--- /dev/null
+++ b/hw/ip/padctrl/fpv/tb/padctrl_bind.sv
@@ -0,0 +1,16 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+
+module padctrl_bind;
+
+ bind padring padring_assert padring_assert (
+ // symbolic inputs for FPV
+ .mio_sel_i(padctrl_tb.mio_sel_i),
+ .dio_sel_i(padctrl_tb.dio_sel_i),
+ // normal connections to padring
+ .*
+ );
+
+endmodule : padctrl_bind
diff --git a/hw/ip/padctrl/fpv/tb/padctrl_tb.sv b/hw/ip/padctrl/fpv/tb/padctrl_tb.sv
new file mode 100644
index 0000000..d7658d1
--- /dev/null
+++ b/hw/ip/padctrl/fpv/tb/padctrl_tb.sv
@@ -0,0 +1,60 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Testbench module for padctrl. Intended to use with a formal tool.
+
+module padctrl_tb #(
+ parameter Impl = "generic"
+) (
+ input wire clk_i,
+ input wire rst_ni,
+ output logic clk_o,
+ output logic rst_no,
+ input tlul_pkg::tl_h2d_t tl_i,
+ output tlul_pkg::tl_d2h_t tl_o,
+ inout wire [padctrl_reg_pkg::NMioPads-1:0] mio_io,
+ inout wire [padctrl_reg_pkg::NDioPads-1:0] dio_io,
+ input [padctrl_reg_pkg::NMioPads-1:0] mio_out_i,
+ input [padctrl_reg_pkg::NMioPads-1:0] mio_oe_i,
+ output logic [padctrl_reg_pkg::NMioPads-1:0] mio_in_o,
+ input [padctrl_reg_pkg::NDioPads-1:0] dio_out_i,
+ input [padctrl_reg_pkg::NDioPads-1:0] dio_oe_i,
+ output logic [padctrl_reg_pkg::NDioPads-1:0] dio_in_o,
+ // symbolic inputs for FPV
+ input [$clog2(padctrl_reg_pkg::NMioPads)-1:0] mio_sel_i,
+ input [$clog2(padctrl_reg_pkg::NDioPads)-1:0] dio_sel_i
+);
+
+ logic [padctrl_reg_pkg::NMioPads-1:0][padctrl_reg_pkg::AttrDw-1:0] mio_attr;
+ logic [padctrl_reg_pkg::NDioPads-1:0][padctrl_reg_pkg::AttrDw-1:0] dio_attr;
+
+ padctrl i_padctrl (
+ .clk_i ,
+ .rst_ni ,
+ .tl_i ,
+ .tl_o ,
+ .mio_attr_o(mio_attr),
+ .dio_attr_o(dio_attr)
+ );
+
+ padring #(
+ .Impl(Impl)
+ ) i_padring (
+ .clk_i ,
+ .rst_ni ,
+ .clk_o ,
+ .rst_no ,
+ .mio_io ,
+ .dio_io ,
+ .mio_out_i ,
+ .mio_oe_i ,
+ .mio_in_o ,
+ .dio_out_i ,
+ .dio_oe_i ,
+ .dio_in_o ,
+ .mio_attr_i(mio_attr),
+ .dio_attr_i(dio_attr)
+ );
+
+endmodule : padctrl_tb
diff --git a/hw/ip/padctrl/fpv/vip/padring_assert.sv b/hw/ip/padctrl/fpv/vip/padring_assert.sv
new file mode 100644
index 0000000..1ebc172
--- /dev/null
+++ b/hw/ip/padctrl/fpv/vip/padring_assert.sv
@@ -0,0 +1,103 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Assertions for padring. Intended to use with a formal tool.
+// Note that only the mandatory pad attributes are tested here.
+
+module padring_assert (
+ input clk_i,
+ input rst_ni,
+ input clk_o,
+ input rst_no,
+ input [padctrl_reg_pkg::NMioPads-1:0] mio_io,
+ input [padctrl_reg_pkg::NDioPads-1:0] dio_io,
+ input [padctrl_reg_pkg::NMioPads-1:0] mio_out_i,
+ input [padctrl_reg_pkg::NMioPads-1:0] mio_oe_i,
+ input [padctrl_reg_pkg::NMioPads-1:0] mio_in_o,
+ input [padctrl_reg_pkg::NDioPads-1:0] dio_out_i,
+ input [padctrl_reg_pkg::NDioPads-1:0] dio_oe_i,
+ input [padctrl_reg_pkg::NDioPads-1:0] dio_in_o,
+ input [padctrl_reg_pkg::NMioPads-1:0]
+ [padctrl_reg_pkg::AttrDw-1:0] mio_attr_i,
+ input [padctrl_reg_pkg::NDioPads-1:0]
+ [padctrl_reg_pkg::AttrDw-1:0] dio_attr_i,
+ // symbolic inputs for FPV
+ input [$clog2(padctrl_reg_pkg::NMioPads)-1:0] mio_sel_i,
+ input [$clog2(padctrl_reg_pkg::NDioPads)-1:0] dio_sel_i
+);
+
+ //////////////////////////////////////////////////////
+ // Check main connectivity of infrastructure signals
+ //////////////////////////////////////////////////////
+
+ `ASSERT(Clk_A, clk_i == clk_o, clk_i, !rst_ni)
+ `ASSERT(Rst_A, rst_ni == rst_no, clk_i, !rst_ni)
+
+ //////////////////////////////////////////////////////
+ // Check muxed IO pads
+ //////////////////////////////////////////////////////
+
+ `ASSUME(NMioRange_M, mio_sel_i < padctrl_reg_pkg::NMioPads, clk_i, !rst_ni)
+
+ // attribute 0 is the input/output inversion bit
+ logic mio_output_value;
+ assign mio_output_value = mio_out_i[mio_sel_i] ^ mio_attr_i[mio_sel_i][0];
+
+ `ASSERT(MioIn_A, mio_in_o[mio_sel_i] == mio_io[mio_sel_i] ^ mio_attr_i[mio_sel_i][0],
+ clk_i, !rst_ni)
+
+ `ASSERT(MioOutNormal_A, mio_oe_i[mio_sel_i] && !mio_attr_i[mio_sel_i][1] |->
+ mio_output_value == mio_io[mio_sel_i], clk_i, !rst_ni)
+
+ `ASSERT(MioOutOd0_A, mio_oe_i[mio_sel_i] && mio_attr_i[mio_sel_i][1] && !mio_output_value |->
+ mio_io[mio_sel_i] == 1'b0, clk_i, !rst_ni)
+
+ // TODO: find a better way to test high-Z?
+ `ASSERT(MioOutOd1_A, mio_oe_i[mio_sel_i] && mio_attr_i[mio_sel_i][1] && mio_output_value |->
+ mio_io[mio_sel_i] === 1'b0 ||
+ mio_io[mio_sel_i] === 1'b1 ||
+ mio_io[mio_sel_i] === 1'bz ||
+ mio_io[mio_sel_i] === 1'bx, clk_i, !rst_ni)
+
+ // TODO: find a better way to test high-Z?
+ `ASSERT(MioOe_A, !mio_oe_i[mio_sel_i] |->
+ mio_io[mio_sel_i] === 1'b0 ||
+ mio_io[mio_sel_i] === 1'b1 ||
+ mio_io[mio_sel_i] === 1'bz ||
+ mio_io[mio_sel_i] === 1'bx, clk_i, !rst_ni)
+
+ //////////////////////////////////////////////////////
+ // Check dedicated IO pads
+ //////////////////////////////////////////////////////
+
+ `ASSUME(NDioRange_M, dio_sel_i < padctrl_reg_pkg::NDioPads, clk_i, !rst_ni)
+
+ // attribute 0 is the input/output inversion bit
+ logic dio_output_value;
+ assign dio_output_value = dio_out_i[dio_sel_i] ^ dio_attr_i[dio_sel_i][0];
+
+ `ASSERT(DioIn_A, dio_in_o[dio_sel_i] == dio_io[dio_sel_i] ^ dio_attr_i[dio_sel_i][0],
+ clk_i, !rst_ni)
+
+ `ASSERT(DioOutNormal_A, dio_oe_i[dio_sel_i] && !dio_attr_i[dio_sel_i][1] |->
+ dio_output_value == dio_io[dio_sel_i], clk_i, !rst_ni)
+
+ `ASSERT(DioOutOd0_A, dio_oe_i[dio_sel_i] && dio_attr_i[dio_sel_i][1] && !dio_output_value |->
+ dio_io[dio_sel_i] == 1'b0, clk_i, !rst_ni)
+
+ // TODO: find a better way to test high-Z?
+ `ASSERT(DioOutOd1_A, dio_oe_i[dio_sel_i] && dio_attr_i[dio_sel_i][1] && dio_output_value |->
+ dio_io[dio_sel_i] === 1'b0 ||
+ dio_io[dio_sel_i] === 1'b1 ||
+ dio_io[dio_sel_i] === 1'bz ||
+ dio_io[dio_sel_i] === 1'bx, clk_i, !rst_ni)
+
+ // TODO: find a better way to test high-Z?
+ `ASSERT(DioOe_A, !dio_oe_i[dio_sel_i] |->
+ dio_io[dio_sel_i] === 1'b0 ||
+ dio_io[dio_sel_i] === 1'b1 ||
+ dio_io[dio_sel_i] === 1'bz ||
+ dio_io[dio_sel_i] === 1'bx, clk_i, !rst_ni)
+
+endmodule : padring_assert
diff --git a/hw/ip/padctrl/rtl/padring.sv b/hw/ip/padctrl/rtl/padring.sv
index 212f2c2..77290ce 100644
--- a/hw/ip/padctrl/rtl/padring.sv
+++ b/hw/ip/padctrl/rtl/padring.sv
@@ -10,8 +10,8 @@
parameter Impl = "generic" // this determines the pad implementation
) (
// pad input
- inout wire clk_i,
- inout wire rst_ni,
+ input wire clk_i,
+ input wire rst_ni,
// to clocking/reset infrastructure
output logic clk_o,
output logic rst_no,
