[fpv/padctrl] Add backward assertions
Add backward assertions for padctrl and padring's outputs
Fix small symbolic variable usage in padring
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv b/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv
index 9bb44f5..fb7585f 100644
--- a/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv
+++ b/hw/ip/padctrl/fpv/vip/padctrl_assert_fpv.sv
@@ -18,7 +18,7 @@
input clk_i,
input rst_ni,
// Bus Interface (device)
- input tlul_pkg::tl_h2d_t tl_i,
+ input tlul_pkg::tl_h2d_t tl_i,
input tlul_pkg::tl_d2h_t tl_o,
// pad attributes to chip level instance
input logic[padctrl_reg_pkg::NMioPads-1:0]
@@ -45,12 +45,20 @@
!(|mio_attr_o[mio_sel][padctrl_reg_pkg::AttrDw-1:6]))
`ASSERT(MioAttr_A, padctrl.reg2hw.mio_pads[mio_sel].qe |=>
mio_attr_o[mio_sel][5:0] == $past(padctrl.reg2hw.mio_pads[mio_sel].q[5:0]))
+ `ASSERT(MioBackwardCheck_A, ##2 !$stable(mio_attr_o[mio_sel]) |->
+ !$stable(padctrl.reg2hw.mio_pads[mio_sel].q[5:0]) ||
+ $rose($past(padctrl.reg2hw.mio_pads[mio_sel].qe)))
+
end else if (Impl == ImplXilinx) begin : gen_mio_xilinx
`ASSERT(MioWarl_A, padctrl.reg2hw.mio_pads[mio_sel].qe |=>
!(|padctrl.mio_attr_q[mio_sel][padctrl_reg_pkg::AttrDw-1:2]))
`ASSERT(MioAttr_A, padctrl.reg2hw.mio_pads[mio_sel].qe |=>
mio_attr_o[mio_sel][1:0] ==
$past(padctrl.reg2hw.mio_pads[mio_sel].q[1:0]))
+ `ASSERT(MioBackwardCheck_A, ##2 !$stable(mio_attr_o[mio_sel]) |->
+ !$stable(padctrl.reg2hw.mio_pads[mio_sel].q[1:0]) ||
+ $rose($past(padctrl.reg2hw.mio_pads[mio_sel].qe)))
+
end else begin : gen_mio_failure
`ASSERT_INIT(UnknownImpl_A, 0)
end
@@ -66,12 +74,20 @@
!(|dio_attr_o[dio_sel][padctrl_reg_pkg::AttrDw-1:6]))
`ASSERT(DioAttr_A, padctrl.reg2hw.dio_pads[dio_sel].qe |=>
dio_attr_o[dio_sel][5:0] == $past(padctrl.reg2hw.dio_pads[dio_sel].q[5:0]))
+ `ASSERT(DioBackwardCheck_A, ##2 !$stable(dio_attr_o[dio_sel]) |->
+ !$stable(padctrl.reg2hw.dio_pads[dio_sel].q[5:0]) ||
+ $rose($past(padctrl.reg2hw.dio_pads[dio_sel].qe)))
+
end else if (Impl == ImplXilinx) begin : gen_dio_xilinx
`ASSERT(DioWarl_A, padctrl.reg2hw.dio_pads[dio_sel].qe |=>
!(|padctrl.dio_attr_q[dio_sel][5:2]))
`ASSERT(DioAttr_A, padctrl.reg2hw.dio_pads[dio_sel].qe |=>
dio_attr_o[dio_sel][1:0] ==
$past(padctrl.reg2hw.dio_pads[dio_sel].q[1:0]))
+ `ASSERT(DioBackwardCheck_A, ##2 !$stable(dio_attr_o[dio_sel]) |->
+ !$stable(padctrl.reg2hw.dio_pads[dio_sel].q[1:0]) ||
+ $rose($past(padctrl.reg2hw.dio_pads[dio_sel].qe)))
+
end else begin : gen_dio_failure
`ASSERT_INIT(UnknownImpl_A, 0)
end
diff --git a/hw/ip/padctrl/fpv/vip/padring_assert_fpv.sv b/hw/ip/padctrl/fpv/vip/padring_assert_fpv.sv
index dcca3c2..2c83ad1 100644
--- a/hw/ip/padctrl/fpv/vip/padring_assert_fpv.sv
+++ b/hw/ip/padctrl/fpv/vip/padring_assert_fpv.sv
@@ -35,19 +35,24 @@
///////////////////////////////////////////////////////
`ASSERT(Clk_A, clk_pad_i === clk_o, clk_pad_i, !rst_pad_ni)
- `ASSERT(Rstpad__A, rst_pad_ni === rst_no, clk_pad_i, !rst_pad_ni)
+ `ASSERT(Rstpad_A, rst_pad_ni === rst_no, clk_pad_i, !rst_pad_ni)
/////////////////////////
// Check muxed IO pads //
/////////////////////////
`ASSUME(NMioRange_M, mio_sel < padctrl_reg_pkg::NMioPads, clk_pad_i, !rst_pad_ni)
+ `ASSUME(NMioStable_M, ##1 $stable(mio_sel), clk_pad_i, !rst_pad_ni)
// attribute 0 is the input/output inversion bit
logic mio_output_value;
assign mio_output_value = mio_out_i[mio_sel] ^ mio_attr_i[mio_sel][0];
- `ASSERT(MioIn_A, mio_in_o[mio_sel] == mio_pad_io[mio_sel] ^ mio_attr_i[mio_sel][0],
+ `ASSERT(MioIn_A, mio_in_o[mio_sel] == mio_pad_io[mio_sel] ^ mio_attr_i[mio_sel][0],
+ clk_pad_i, !rst_pad_ni)
+
+ `ASSERT(MioInBackwardCheck_A, ##1 !$stable(mio_in_o[mio_sel]) |->
+ !$stable(mio_pad_io[mio_sel]) || !$stable(mio_attr_i[mio_sel][0]),
clk_pad_i, !rst_pad_ni)
`ASSERT(MioOutNormal_A, mio_oe_i[mio_sel] && !mio_attr_i[mio_sel][1] |->
@@ -75,6 +80,7 @@
/////////////////////////////
`ASSUME(NDioRange_M, dio_sel < padctrl_reg_pkg::NDioPads, clk_pad_i, !rst_pad_ni)
+ `ASSUME(NDioStable_M, ##1 $stable(dio_sel), clk_pad_i, !rst_pad_ni)
// attribute 0 is the input/output inversion bit
logic dio_output_value;
@@ -83,6 +89,10 @@
`ASSERT(DioIn_A, dio_in_o[dio_sel] == dio_pad_io[dio_sel] ^ dio_attr_i[dio_sel][0],
clk_pad_i, !rst_pad_ni)
+ `ASSERT(DioInBackwardCheck_A, ##1 !$stable(dio_in_o[dio_sel]) |->
+ !$stable(dio_pad_io[dio_sel]) || !$stable(dio_attr_i[dio_sel][0]),
+ clk_pad_i, !rst_pad_ni)
+
`ASSERT(DioOutNormal_A, dio_oe_i[dio_sel] && !dio_attr_i[dio_sel][1] |->
dio_output_value == dio_pad_io[dio_sel], clk_pad_i, !rst_pad_ni)
