[fpv] Add KNOWN assertions to outputs to pinmux, padctrl, alert_handler
diff --git a/hw/ip/alert_handler/rtl/alert_handler.sv b/hw/ip/alert_handler/rtl/alert_handler.sv
index 8d875a5..20cb4ab 100644
--- a/hw/ip/alert_handler/rtl/alert_handler.sv
+++ b/hw/ip/alert_handler/rtl/alert_handler.sv
@@ -199,6 +199,17 @@
// Assertions
//////////////////////////////////////////////////////
+ // check whether all outputs have a good known state after reset
+ `ASSERT_KNOWN(TlKnownO_A, tl_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(IrqKnownO_A, irq_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(CrashdumpKnownO_A, crashdump_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(PingPKnownO_A, ping_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(PingNKnownO_A, ping_no, clk_i, !rst_ni)
+ `ASSERT_KNOWN(AckPKnownO_A, ack_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(AckNKnownO_A, ack_no, clk_i, !rst_ni)
+ `ASSERT_KNOWN(EscPKnownO_A, esc_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(EscNKnownO_A, esc_no, clk_i, !rst_ni)
+
// this restriction is due to specifics in the ping selection mechanism
`ASSERT_INIT(CheckNAlerts,
alert_pkg::NAlerts < (256 - alert_pkg::N_CLASSES))
diff --git a/hw/ip/padctrl/rtl/padctrl.sv b/hw/ip/padctrl/rtl/padctrl.sv
index 2824779..fe11028 100644
--- a/hw/ip/padctrl/rtl/padctrl.sv
+++ b/hw/ip/padctrl/rtl/padctrl.sv
@@ -106,4 +106,12 @@
assign hw2reg.mio_pads[k].d = mio_attr_q[k] & warl_mask;
end
+ //////////////////////////////////////////////////////
+ // Assertions
+ //////////////////////////////////////////////////////
+
+ `ASSERT_KNOWN(TlKnownO_A, tl_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(MioKnownO_A, mio_attr_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(DioKnownO_A, dio_attr_o, clk_i, !rst_ni)
+
endmodule : padctrl
diff --git a/hw/ip/padctrl/rtl/padring.sv b/hw/ip/padctrl/rtl/padring.sv
index 9a3ac11..a731bb4 100644
--- a/hw/ip/padctrl/rtl/padring.sv
+++ b/hw/ip/padctrl/rtl/padring.sv
@@ -107,4 +107,15 @@
);
end
+ //////////////////////////////////////////////////////
+ // Assertions
+ //////////////////////////////////////////////////////
+
+ `ASSERT_KNOWN(ClkKnownIO_A, clk_o, clk_pad_i, !rst_pad_ni)
+ `ASSERT_KNOWN(RstKnownIO_A, rst_no, clk_pad_i, !rst_pad_ni)
+ `ASSERT_KNOWN(MioPadKnownIO_A, mio_pad_io, clk_pad_i, !rst_pad_ni)
+ `ASSERT_KNOWN(DioPadKnownIO_A, dio_pad_io, clk_pad_i, !rst_pad_ni)
+ `ASSERT_KNOWN(MioInKnownO_A, mio_in_o, clk_pad_i, !rst_pad_ni)
+ `ASSERT_KNOWN(DioInKnownO_A, dio_in_o, clk_pad_i, !rst_pad_ni)
+
endmodule : padring
diff --git a/hw/ip/pinmux/rtl/pinmux.sv b/hw/ip/pinmux/rtl/pinmux.sv
index 09f6953..7283a2c 100644
--- a/hw/ip/pinmux/rtl/pinmux.sv
+++ b/hw/ip/pinmux/rtl/pinmux.sv
@@ -68,4 +68,13 @@
`ASSUME(OutSelRange_A, reg2hw.mio_outsel[k].q < pinmux_reg_pkg::NPeriphOut + 3, clk_i, !rst_ni)
end
+ //////////////////////////////////////////////////////
+ // Assertions
+ //////////////////////////////////////////////////////
+
+ `ASSERT_KNOWN(TlKnownO_A, tl_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(MioToPeriphKnownO_A, mio_to_periph_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(MioOutKnownO_A, mio_out_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(MioOeKnownO_A, mio_oe_o, clk_i, !rst_ni)
+
endmodule : pinmux
diff --git a/hw/ip/prim/rtl/prim_alert_receiver.sv b/hw/ip/prim/rtl/prim_alert_receiver.sv
index 3093eb5..cd408f1 100644
--- a/hw/ip/prim/rtl/prim_alert_receiver.sv
+++ b/hw/ip/prim/rtl/prim_alert_receiver.sv
@@ -171,7 +171,15 @@
// assertions
//////////////////////////////////////////////////////
- // shared assertions
+ // check whether all outputs have a good known state after reset
+ `ASSERT_KNOWN(PingOkKnownO_A, ping_ok_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(IntegFailKnownO_A, integ_fail_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(AlertKnownO_A, alert_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(PingPKnownO_A, ping_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(PingNKnownO_A, ping_no, clk_i, !rst_ni)
+ `ASSERT_KNOWN(AckPKnownO_A, ack_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(AckNKnownO_A, ack_no, clk_i, !rst_ni)
+
// check encoding of outgoing diffpairs
`ASSERT(PingDiffOk_A, ping_po ^ ping_no, clk_i, !rst_ni)
`ASSERT(AckDiffOk_A, ack_po ^ ack_no, clk_i, !rst_ni)
diff --git a/hw/ip/prim/rtl/prim_alert_sender.sv b/hw/ip/prim/rtl/prim_alert_sender.sv
index 814a5cc..fb5bd58 100644
--- a/hw/ip/prim/rtl/prim_alert_sender.sv
+++ b/hw/ip/prim/rtl/prim_alert_sender.sv
@@ -190,6 +190,10 @@
// assertions
//////////////////////////////////////////////////////
+ // check whether all outputs have a good known state after reset
+ `ASSERT_KNOWN(AlertPKnownO_A, alert_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(AlertNKnownO_A, alert_no, clk_i, !rst_ni)
+
if (AsyncOn) begin : gen_async_assert
// check propagation of sigint issues to output within three cycles
`ASSERT(SigIntPing_A, ping_pi == ping_ni [*2] |-> ##3 alert_po == alert_no, clk_i, !rst_ni)
diff --git a/hw/ip/prim/rtl/prim_esc_receiver.sv b/hw/ip/prim/rtl/prim_esc_receiver.sv
index 4c5ac7d..201342c 100644
--- a/hw/ip/prim/rtl/prim_esc_receiver.sv
+++ b/hw/ip/prim/rtl/prim_esc_receiver.sv
@@ -158,6 +158,11 @@
// assertions
//////////////////////////////////////////////////////
+ // check whether all outputs have a good known state after reset
+ `ASSERT_KNOWN(EscEnKnownO_A, esc_en_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(RespPKnownO_A, resp_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(RespNKnownO_A, resp_no, clk_i, !rst_ni)
+
`ASSERT(SigIntCheck0_A, esc_pi == esc_ni |=> resp_po == resp_no, clk_i, !rst_ni)
`ASSERT(SigIntCheck1_A, esc_pi == esc_ni |=> state_q == SigInt, clk_i, !rst_ni)
// correct diff encoding
diff --git a/hw/ip/prim/rtl/prim_esc_sender.sv b/hw/ip/prim/rtl/prim_esc_sender.sv
index bf8affb..e4bb10e 100644
--- a/hw/ip/prim/rtl/prim_esc_sender.sv
+++ b/hw/ip/prim/rtl/prim_esc_sender.sv
@@ -217,6 +217,12 @@
// assertions
//////////////////////////////////////////////////////
+ // check whether all outputs have a good known state after reset
+ `ASSERT_KNOWN(PingOkKnownO_A, ping_ok_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(IntegFailKnownO_A, integ_fail_o, clk_i, !rst_ni)
+ `ASSERT_KNOWN(EscPKnownO_A, esc_po, clk_i, !rst_ni)
+ `ASSERT_KNOWN(EscNKnownO_A, esc_no, clk_i, !rst_ni)
+
// diff encoding of output
`ASSERT(DiffEncCheck_A, esc_po ^ esc_no, clk_i, !rst_ni)
// signal integrity check propagation
diff --git a/hw/ip/prim/rtl/prim_lfsr.sv b/hw/ip/prim/rtl/prim_lfsr.sv
index b76f825..ee3c640 100644
--- a/hw/ip/prim/rtl/prim_lfsr.sv
+++ b/hw/ip/prim/rtl/prim_lfsr.sv
@@ -358,6 +358,8 @@
// shared assertions
//////////////////////////////////////////////////////
+ `ASSERT_KNOWN(DataKnownO_A, data_o, clk_i, !rst_ni)
+
function automatic logic[LfsrDw-1:0] compute_next_state(logic[LfsrDw-1:0] coeffs,
logic[InDw-1:0] data,
logic[LfsrDw-1:0] state);
