[alert_handler/prim] Add FPV testbenches for diff rx/tx prims
diff --git a/hw/formal/formal.core b/hw/formal/formal.core
index 979b6b9..15bc5a0 100644
--- a/hw/formal/formal.core
+++ b/hw/formal/formal.core
@@ -11,6 +11,8 @@
files_rtl_generic:
depend:
- lowrisc:fpv:prim_lfsr_fpv
+ - lowrisc:fpv:prim_alert_rxtx_fpv
+ - lowrisc:fpv:prim_esc_rxtx_fpv
- lowrisc:ip:rv_timer
- lowrisc:ip:hmac
- lowrisc:systems:top_earlgrey
diff --git a/hw/ip/prim/fpv/prim_alert_rxtx_fpv.core b/hw/ip/prim/fpv/prim_alert_rxtx_fpv.core
new file mode 100644
index 0000000..81b534a
--- /dev/null
+++ b/hw/ip/prim/fpv/prim_alert_rxtx_fpv.core
@@ -0,0 +1,27 @@
+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_alert_rxtx_fpv:0.1"
+description: "ALERT_HANDLER FPV target"
+filesets:
+ files_fpv:
+ depend:
+ - lowrisc:prim:all
+ files:
+ - vip/prim_alert_rxtx_async_assert.sv
+ - vip/prim_alert_rxtx_assert.sv
+ - tb/prim_alert_rxtx_async_tb.sv
+ - tb/prim_alert_rxtx_tb.sv
+ - tb/prim_alert_rxtx_async_bind.sv
+ - tb/prim_alert_rxtx_bind.sv
+ file_type: systemVerilogSource
+
+targets:
+ default: &default_target
+ toplevel:
+ - prim_alert_rxtx_async_tb
+ - prim_alert_rxtx_tb
+ filesets:
+ - files_fpv
+ default_tool: jg
diff --git a/hw/ip/prim/fpv/prim_esc_rxtx_fpv.core b/hw/ip/prim/fpv/prim_esc_rxtx_fpv.core
new file mode 100644
index 0000000..d65b9d2
--- /dev/null
+++ b/hw/ip/prim/fpv/prim_esc_rxtx_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:prim_esc_rxtx_fpv:0.1"
+description: "ALERT_HANDLER FPV target"
+filesets:
+ files_fpv:
+ depend:
+ - lowrisc:prim:all
+ files:
+ - vip/prim_esc_rxtx_assert.sv
+ - tb/prim_esc_rxtx_bind.sv
+ - tb/prim_esc_rxtx_tb.sv
+ file_type: systemVerilogSource
+
+targets:
+ default: &default_target
+ toplevel:
+ - prim_esc_rxtx_tb
+ filesets:
+ - files_fpv
+ default_tool: jg
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_bind.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_bind.sv
new file mode 100644
index 0000000..9b6f65b
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_bind.sv
@@ -0,0 +1,27 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+
+module prim_alert_rxtx_async_bind;
+
+ bind prim_alert_rxtx_async_tb prim_alert_rxtx_async_assert prim_alert_rxtx_async_assert (
+ .clk_i,
+ .rst_ni,
+ .ping_err_pi,
+ .ping_err_ni,
+ .ping_skew_i,
+ .ack_err_pi,
+ .ack_err_ni,
+ .ack_skew_i,
+ .alert_err_pi,
+ .alert_err_ni,
+ .alert_skew_i,
+ .alert_i,
+ .ping_en_i,
+ .ping_ok_o,
+ .integ_fail_o,
+ .alert_o
+ );
+
+endmodule : prim_alert_rxtx_async_bind
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_tb.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_tb.sv
new file mode 100644
index 0000000..c8439d3
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_tb.sv
@@ -0,0 +1,97 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Testbench module for alert sender/receiver pair. Intended to use with
+// a formal tool.
+
+module prim_alert_rxtx_async_tb (
+ input clk_i,
+ input rst_ni,
+ // for sigint error and skew injection only
+ input ping_err_pi,
+ input ping_err_ni,
+ input [1:0] ping_skew_i,
+ input ack_err_pi,
+ input ack_err_ni,
+ input [1:0] ack_skew_i,
+ input alert_err_pi,
+ input alert_err_ni,
+ input [1:0] alert_skew_i,
+ // normal I/Os
+ input alert_i,
+ input ping_en_i,
+ output logic ping_ok_o,
+ output logic integ_fail_o,
+ output logic alert_o
+);
+
+ // asynchronous case
+ localparam bit AsyncOn = 1'b1;
+
+ logic ping_pd;
+ logic ping_nd;
+ logic ack_pd;
+ logic ack_nd;
+ logic alert_pd;
+ logic alert_nd;
+ logic [1:0] ping_pq;
+ logic [1:0] ping_nq;
+ logic [1:0] ack_pq;
+ logic [1:0] ack_nq;
+ logic [1:0] alert_pq;
+ logic [1:0] alert_nq;
+
+ // for the purposes of FPV, we currently emulate the asynchronous transition
+ // only in terms of the skew it may introduce (which is limited to +- 1 cycle)
+
+ prim_alert_sender #(
+ .AsyncOn ( AsyncOn )
+ ) i_prim_alert_sender (
+ .clk_i ,
+ .rst_ni ,
+ .alert_i ,
+ .ping_pi ( ping_pq[ping_skew_i[0]] ^ ping_err_pi ),
+ .ping_ni ( ping_nq[ping_skew_i[1]] ^ ping_err_ni ),
+ .ack_pi ( ack_pq[ack_skew_i[0]] ^ ack_err_pi ),
+ .ack_ni ( ack_nq[ack_skew_i[1]] ^ ack_err_ni ),
+ .alert_po ( alert_pd ),
+ .alert_no ( alert_nd )
+ );
+
+ prim_alert_receiver #(
+ .AsyncOn ( AsyncOn )
+ ) i_prim_alert_receiver (
+ .clk_i ,
+ .rst_ni ,
+ .ping_en_i ,
+ .ping_ok_o ,
+ .integ_fail_o ,
+ .alert_o ,
+ .ping_po ( ping_pd ),
+ .ping_no ( ping_nd ),
+ .ack_po ( ack_pd ),
+ .ack_no ( ack_nd ),
+ .alert_pi ( alert_pq[alert_skew_i[0]] ^ alert_err_pi ),
+ .alert_ni ( alert_nq[alert_skew_i[1]] ^ alert_err_ni )
+ );
+
+ always_ff @(posedge clk_i or negedge rst_ni) begin : p_skew_delay
+ if (!rst_ni) begin
+ ping_pq <= '0;
+ ping_nq <= '1;
+ ack_pq <= '0;
+ ack_nq <= '1;
+ alert_pq <= '0;
+ alert_nq <= '1;
+ end else begin
+ ping_pq <= {ping_pq [$high(ping_pq )-1:0], ping_pd};
+ ping_nq <= {ping_nq [$high(ping_nq )-1:0], ping_nd};
+ ack_pq <= {ack_pq [$high(ack_pq )-1:0], ack_pd};
+ ack_nq <= {ack_nq [$high(ack_nq )-1:0], ack_nd};
+ alert_pq <= {alert_pq[$high(alert_pq)-1:0], alert_pd};
+ alert_nq <= {alert_nq[$high(alert_nq)-1:0], alert_nd};
+ end
+ end
+
+endmodule : prim_alert_rxtx_async_tb
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_bind.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_bind.sv
new file mode 100644
index 0000000..3081b6e
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_bind.sv
@@ -0,0 +1,24 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+
+module prim_alert_rxtx_bind;
+
+ bind prim_alert_rxtx_tb prim_alert_rxtx_assert prim_alert_rxtx_assert (
+ .clk_i,
+ .rst_ni,
+ .ping_err_pi,
+ .ping_err_ni,
+ .ack_err_pi,
+ .ack_err_ni,
+ .alert_err_pi,
+ .alert_err_ni,
+ .alert_i,
+ .ping_en_i,
+ .ping_ok_o,
+ .integ_fail_o,
+ .alert_o
+ );
+
+endmodule : prim_alert_rxtx_bind
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_tb.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_tb.sv
new file mode 100644
index 0000000..25fd560
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_tb.sv
@@ -0,0 +1,67 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Testbench module for alert sender/receiver pair. Intended to use with
+// a formal tool.
+
+module prim_alert_rxtx_tb (
+ input clk_i,
+ input rst_ni,
+ // for sigint error injection only
+ input ping_err_pi,
+ input ping_err_ni,
+ input ack_err_pi,
+ input ack_err_ni,
+ input alert_err_pi,
+ input alert_err_ni,
+ // normal I/Os
+ input alert_i,
+ input ping_en_i,
+ output logic ping_ok_o,
+ output logic integ_fail_o,
+ output logic alert_o
+);
+
+ // synchronous case
+ localparam bit AsyncOn = 1'b0;
+
+ logic ping_p;
+ logic ping_n;
+ logic ack_p;
+ logic ack_n;
+ logic alert_p;
+ logic alert_n;
+
+ prim_alert_sender #(
+ .AsyncOn ( AsyncOn )
+ ) i_prim_alert_sender (
+ .clk_i ,
+ .rst_ni ,
+ .alert_i ,
+ .ping_pi ( ping_p ^ ping_err_pi ),
+ .ping_ni ( ping_n ^ ping_err_ni ),
+ .ack_pi ( ack_p ^ ack_err_pi ),
+ .ack_ni ( ack_n ^ ack_err_ni ),
+ .alert_po ( alert_p ),
+ .alert_no ( alert_n )
+ );
+
+ prim_alert_receiver #(
+ .AsyncOn ( AsyncOn )
+ ) i_prim_alert_receiver (
+ .clk_i ,
+ .rst_ni ,
+ .ping_en_i ,
+ .ping_ok_o ,
+ .integ_fail_o ,
+ .alert_o ,
+ .ping_po ( ping_p ),
+ .ping_no ( ping_n ),
+ .ack_po ( ack_p ),
+ .ack_no ( ack_n ),
+ .alert_pi ( alert_p ^ alert_err_pi ),
+ .alert_ni ( alert_n ^ alert_err_ni )
+ );
+
+endmodule : prim_alert_rxtx_tb
diff --git a/hw/ip/prim/fpv/tb/prim_esc_rxtx_bind.sv b/hw/ip/prim/fpv/tb/prim_esc_rxtx_bind.sv
new file mode 100644
index 0000000..698e17d
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_esc_rxtx_bind.sv
@@ -0,0 +1,22 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+
+module prim_esc_rxtx_bind;
+
+ bind prim_esc_rxtx_tb prim_esc_rxtx_assert prim_esc_rxtx_assert (
+ .clk_i ,
+ .rst_ni ,
+ .resp_err_pi ,
+ .resp_err_ni ,
+ .esc_err_pi ,
+ .esc_err_ni ,
+ .esc_en_i ,
+ .ping_en_i ,
+ .ping_ok_o ,
+ .integ_fail_o,
+ .esc_en_o
+ );
+
+endmodule : prim_esc_rxtx_bind
diff --git a/hw/ip/prim/fpv/tb/prim_esc_rxtx_tb.sv b/hw/ip/prim/fpv/tb/prim_esc_rxtx_tb.sv
new file mode 100644
index 0000000..86ce372
--- /dev/null
+++ b/hw/ip/prim/fpv/tb/prim_esc_rxtx_tb.sv
@@ -0,0 +1,52 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Testbench module for escalation sender/receiver pair. Intended to use with
+// a formal tool.
+
+module prim_esc_rxtx_tb (
+ input clk_i,
+ input rst_ni,
+ // for sigint error injection only
+ input resp_err_pi,
+ input resp_err_ni,
+ input esc_err_pi,
+ input esc_err_ni,
+ // normal I/Os
+ input esc_en_i,
+ input ping_en_i,
+ output logic ping_ok_o,
+ output logic integ_fail_o,
+ output logic esc_en_o
+);
+
+ logic resp_p;
+ logic resp_n;
+ logic esc_p;
+ logic esc_n;
+
+ prim_esc_sender i_prim_esc_sender (
+ .clk_i ,
+ .rst_ni ,
+ .ping_en_i ,
+ .ping_ok_o ,
+ .integ_fail_o ,
+ .esc_en_i ,
+ .resp_pi ( resp_p ^ resp_err_pi ),
+ .resp_ni ( resp_n ^ resp_err_ni ),
+ .esc_po ( esc_p ),
+ .esc_no ( esc_n )
+ );
+
+ prim_esc_receiver i_prim_esc_receiver (
+ .clk_i ,
+ .rst_ni ,
+ .esc_en_o ,
+ .resp_po ( resp_p ),
+ .resp_no ( resp_n ),
+ .esc_pi ( esc_p ^ esc_err_pi ),
+ .esc_ni ( esc_n ^ esc_err_ni )
+ );
+
+endmodule : prim_esc_rxtx_tb
diff --git a/hw/ip/prim/fpv/vip/prim_alert_rxtx_assert.sv b/hw/ip/prim/fpv/vip/prim_alert_rxtx_assert.sv
new file mode 100644
index 0000000..abf3b20
--- /dev/null
+++ b/hw/ip/prim/fpv/vip/prim_alert_rxtx_assert.sv
@@ -0,0 +1,87 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Assertions for alert sender/receiver pair. Intended to use with
+// a formal tool.
+
+module prim_alert_rxtx_assert (
+ input clk_i,
+ input rst_ni,
+ // for sigint error injection only
+ input ping_err_pi,
+ input ping_err_ni,
+ input ack_err_pi,
+ input ack_err_ni,
+ input alert_err_pi,
+ input alert_err_ni,
+ // normal I/Os
+ input alert_i,
+ input ping_en_i,
+ input ping_ok_o,
+ input integ_fail_o,
+ input alert_o
+);
+
+ logic error_present;
+ assign error_present = ping_err_pi | ping_err_ni |
+ ack_err_pi | ack_err_ni |
+ alert_err_pi | alert_err_ni;
+
+ // note: we can only detect sigint errors where one wire is flipped.
+ `ASSUME_FPV(PingErrorsAreOH_M, $onehot0({ping_err_pi, ping_err_ni}), clk_i, !rst_ni)
+ `ASSUME_FPV(AckErrorsAreOH_M, $onehot0({ack_err_pi, ack_err_ni}), clk_i, !rst_ni)
+ `ASSUME_FPV(AlertErrorsAreOH_M, $onehot0({alert_err_pi, alert_err_ni}), clk_i, !rst_ni)
+
+ // ping will stay high until ping ok received, then it must be deasserted
+ // TODO: this excludes the case where no ping ok will be returned due to an error
+ `ASSUME_FPV(PingDeassert_M, ping_en_i && ping_ok_o |=> !ping_en_i, clk_i, !rst_ni)
+ `ASSUME_FPV(PingEnStaysAsserted0_M, ping_en_i |=> (ping_en_i && !ping_ok_o) or
+ (ping_en_i && ping_ok_o ##1 $fell(ping_en_i)), clk_i, !rst_ni || error_present)
+
+ sequence FullHandshake_S;
+ $rose(prim_alert_rxtx_tb.alert_p) ##1
+ $rose(prim_alert_rxtx_tb.ack_p) && $stable(prim_alert_rxtx_tb.alert_p) ##1
+ $fell(prim_alert_rxtx_tb.alert_p) && $stable(prim_alert_rxtx_tb.ack_p) ##1
+ $fell(prim_alert_rxtx_tb.ack_p) && $stable(prim_alert_rxtx_tb.alert_p) ;
+ endsequence
+
+ // note: injected errors may lockup the FSMs, and hence the full HS can
+ // only take place if both FSMs are in a sane state
+ `ASSERT(PingHs_A, ##1 $changed(prim_alert_rxtx_tb.ping_p) &&
+ (prim_alert_rxtx_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_tb.i_prim_alert_sender.Idle ) &&
+ (prim_alert_rxtx_tb.i_prim_alert_receiver.state_q ==
+ prim_alert_rxtx_tb.i_prim_alert_receiver.Idle )|=> FullHandshake_S,
+ clk_i, !rst_ni || error_present)
+ `ASSERT(AlertHs_A, alert_i &&
+ (prim_alert_rxtx_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_tb.i_prim_alert_sender.Idle) &&
+ (prim_alert_rxtx_tb.i_prim_alert_receiver.state_q ==
+ prim_alert_rxtx_tb.i_prim_alert_receiver.Idle) |=>
+ FullHandshake_S, clk_i, !rst_ni || error_present)
+
+ // transmission of pings
+ `ASSERT(AlertPing_A, !error_present ##1 $rose(ping_en_i) |->
+ ##[1:9] ping_ok_o, clk_i, !rst_ni || error_present)
+ // transmission of alerts in case of no collision with ping enable
+ `ASSERT(AlertCheck0_A, !ping_en_i [*3] ##0 $rose(alert_i) &&
+ (prim_alert_rxtx_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_tb.i_prim_alert_sender.Idle) |=>
+ alert_o, clk_i, !rst_ni || error_present || ping_en_i)
+ // transmission of alerts in the general case which can include ping collisions
+ `ASSERT(AlertCheck1_A, alert_i |-> ##[1:9] alert_o, clk_i, !rst_ni || error_present)
+
+ // basic liveness of FSMs in case no errors are present
+ `ASSERT(FsmLivenessSender_A,
+ (prim_alert_rxtx_tb.i_prim_alert_sender.state_q !=
+ prim_alert_rxtx_tb.i_prim_alert_sender.Idle) |->
+ strong(##[1:$] (prim_alert_rxtx_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_tb.i_prim_alert_sender.Idle)), clk_i, !rst_ni || error_present)
+ `ASSERT(FsmLivenessReceiver_A,
+ (prim_alert_rxtx_tb.i_prim_alert_receiver.state_q !=
+ prim_alert_rxtx_tb.i_prim_alert_receiver.Idle) |->
+ strong(##[1:$] (prim_alert_rxtx_tb.i_prim_alert_receiver.state_q ==
+ prim_alert_rxtx_tb.i_prim_alert_receiver.Idle)),clk_i, !rst_ni || error_present)
+
+endmodule : prim_alert_rxtx_assert
diff --git a/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert.sv b/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert.sv
new file mode 100644
index 0000000..7e8532b
--- /dev/null
+++ b/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert.sv
@@ -0,0 +1,119 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Assertions for alert sender/receiver pair for the asynchronous case.
+// Intended to use with a formal tool.
+
+module prim_alert_rxtx_async_assert (
+ input clk_i,
+ input rst_ni,
+ // for sigint error and skew injection only
+ input ping_err_pi,
+ input ping_err_ni,
+ input [1:0] ping_skew_i,
+ input ack_err_pi,
+ input ack_err_ni,
+ input [1:0] ack_skew_i,
+ input alert_err_pi,
+ input alert_err_ni,
+ input [1:0] alert_skew_i,
+ // normal I/Os
+ input alert_i,
+ input ping_en_i,
+ input ping_ok_o,
+ input integ_fail_o,
+ input alert_o
+);
+
+ logic error_present;
+ assign error_present = ping_err_pi | ping_err_ni |
+ ack_err_pi | ack_err_ni |
+ alert_err_pi | alert_err_ni;
+
+ // used to check that an error has never occured so far
+ // this is used to check the handshake below. the handshake can lock up
+ // the protocol FSMs causing the handshake to never complete.
+ // note that this will block any ping messages and hence it can be
+ // eventually detected by the alert handler.
+ logic error_setreg_d, error_setreg_q;
+ assign error_setreg_d = error_present | error_setreg_q;
+
+ always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
+ if (!rst_ni) begin
+ error_setreg_q <= 1'b0;
+ end else begin
+ error_setreg_q <= error_setreg_d;
+ end
+ end
+
+ // Note: we can only detect sigint errors where one wire is flipped.
+ `ASSUME_FPV(PingErrorsAreOH_M, $onehot0({ping_err_pi, ping_err_ni}), clk_i, !rst_ni)
+ `ASSUME_FPV(AckErrorsAreOH_M, $onehot0({ack_err_pi, ack_err_ni}), clk_i, !rst_ni)
+ `ASSUME_FPV(AlertErrorsAreOH_M, $onehot0({alert_err_pi, alert_err_ni}), clk_i, !rst_ni)
+
+ // ping will stay high until ping ok received, then it must be deasserted
+ // TODO: this excludes the case where no ping ok will be returned due to an error
+ `ASSUME_FPV(PingDeassert_M, ping_en_i && ping_ok_o |=> !ping_en_i, clk_i, !rst_ni)
+ `ASSUME_FPV(PingEnStaysAsserted0_M, ping_en_i |=>
+ (ping_en_i && !ping_ok_o) or
+ (ping_en_i && ping_ok_o ##1 $fell(ping_en_i)),
+ clk_i, !rst_ni || error_present)
+
+ // Note: the sequence lengths of the handshake and the following properties needs to
+ // be parameterized accordingly if different clock ratios are to be used here.
+ // TODO: tighten bounds if possible
+ sequence FullHandshake_S;
+ $rose(prim_alert_rxtx_async_tb.alert_pd) ##[3:5]
+ $rose(prim_alert_rxtx_async_tb.ack_pd) &&
+ $stable(prim_alert_rxtx_async_tb.alert_pd) ##[3:5]
+ $fell(prim_alert_rxtx_async_tb.alert_pd) &&
+ $stable(prim_alert_rxtx_async_tb.ack_pd) ##[3:5]
+ $fell(prim_alert_rxtx_async_tb.ack_pd) &&
+ $stable(prim_alert_rxtx_async_tb.alert_pd);
+ endsequence
+
+ // note: injected errors may lockup the FSMs, and hence the full HS can
+ // only take place if both FSMs are in a sane state
+ `ASSERT(PingHs_A, ##1 $changed(prim_alert_rxtx_async_tb.ping_pd) &&
+ (prim_alert_rxtx_async_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_async_tb.i_prim_alert_sender.Idle) &&
+ (prim_alert_rxtx_async_tb.i_prim_alert_receiver.state_q ==
+ prim_alert_rxtx_async_tb.i_prim_alert_receiver.Idle) |-> ##[0:5] FullHandshake_S,
+ clk_i, !rst_ni || error_setreg_q)
+ `ASSERT(AlertHs_A, alert_i &&
+ (prim_alert_rxtx_async_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_async_tb.i_prim_alert_sender.Idle) &&
+ (prim_alert_rxtx_async_tb.i_prim_alert_receiver.state_q ==
+ prim_alert_rxtx_async_tb.i_prim_alert_receiver.Idle) |-> ##[0:5] FullHandshake_S,
+ clk_i, !rst_ni || error_setreg_q)
+
+ // transmission of pings
+ // this bound is relatively large as in the worst case, we need to resolve
+ // staggered differential signal patterns on all three differential channels
+ `ASSERT(AlertPing_A, $rose(ping_en_i) |-> ##[1:23] ping_ok_o,
+ clk_i, !rst_ni || error_setreg_q)
+ // transmission of first alert assertion (no ping collision)
+ `ASSERT(AlertCheck0_A, !ping_en_i [*10] ##1 $rose(alert_i) &&
+ (prim_alert_rxtx_async_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_async_tb.i_prim_alert_sender.Idle) |->
+ ##[3:5] alert_o, clk_i, !rst_ni || ping_en_i || error_setreg_q)
+ // eventual transmission of alerts in the general case which can include ping collisions
+ `ASSERT(AlertCheck1_A, alert_i |-> ##[1:25] alert_o,
+ clk_i, !rst_ni || error_setreg_q)
+
+ // basic liveness of FSMs in case no errors are present
+ `ASSERT(FsmLivenessSender_A, !error_present [*2] ##1 !error_present &&
+ (prim_alert_rxtx_async_tb.i_prim_alert_sender.state_q !=
+ prim_alert_rxtx_async_tb.i_prim_alert_sender.Idle) |->
+ strong(##[1:$] (prim_alert_rxtx_async_tb.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_async_tb.i_prim_alert_sender.Idle)), clk_i, !rst_ni || error_present)
+ `ASSERT(FsmLivenessReceiver_A, !error_present [*2] ##1 !error_present &&
+ (prim_alert_rxtx_async_tb.i_prim_alert_receiver.state_q !=
+ prim_alert_rxtx_async_tb.i_prim_alert_receiver.Idle) |->
+ strong(##[1:$] (prim_alert_rxtx_async_tb.i_prim_alert_receiver.state_q ==
+ prim_alert_rxtx_async_tb.i_prim_alert_receiver.Idle)),clk_i, !rst_ni || error_present)
+
+ // TODO: add FSM liveness of 3x diff decoder instances
+
+endmodule : prim_alert_rxtx_async_assert
diff --git a/hw/ip/prim/fpv/vip/prim_esc_rxtx_assert.sv b/hw/ip/prim/fpv/vip/prim_esc_rxtx_assert.sv
new file mode 100644
index 0000000..9e2dc01
--- /dev/null
+++ b/hw/ip/prim/fpv/vip/prim_esc_rxtx_assert.sv
@@ -0,0 +1,68 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// Assertions for escalation sender/receiver pair. Intended to use with
+// a formal tool.
+
+module prim_esc_rxtx_assert (
+ input clk_i,
+ input rst_ni,
+ // for sigint error injection only
+ input resp_err_pi,
+ input resp_err_ni,
+ input esc_err_pi,
+ input esc_err_ni,
+ // normal I/Os
+ input esc_en_i,
+ input ping_en_i,
+ input ping_ok_o,
+ input integ_fail_o,
+ input esc_en_o
+);
+
+ logic error_present;
+ assign error_present = resp_err_pi | resp_err_ni |
+ esc_err_pi | esc_err_ni;
+
+ // ping will stay high until ping ok received, then it must be deasserted
+ // TODO: this escludes the case where no ping ok will be returned due to an error
+ `ASSUME_FPV(PingDeassert_M, ping_en_i && ping_ok_o |=> ping_en_i, clk_i, !rst_ni)
+ `ASSUME_FPV(PingEnStaysAsserted0_M, ping_en_i |=>
+ (ping_en_i && !ping_ok_o) or (ping_en_i && ping_ok_o ##1 $fell(ping_en_i)),
+ clk_i, !rst_ni || error_present)
+
+ // assume that the ping enable and escalation enable signals will eventually be deasserted (and
+ // esc will stay low for more than 2 cycles)
+ `ASSUME_FPV(FiniteEsc_M, esc_en_i |-> strong(##[1:$] !esc_en_i [*2]), clk_i, !rst_ni)
+ `ASSUME_FPV(FinitePing_M, ping_en_i |-> strong(##[1:$] !ping_en_i), clk_i, !rst_ni)
+
+ // ping response mus occur within 4 cycles (given that no
+ // error occured within the previous cycles)
+ `ASSERT(PingRespCheck_A, !error_present [*4] ##1 $rose(ping_en_i) |->
+ ##[0:4] ping_ok_o, clk_i, !rst_ni || error_present)
+
+ // be more specific (i.e. use throughout)
+ `ASSERT(EscRespCheck_A, ##1 esc_en_i |-> ##[0:1] prim_esc_rxtx_tb.resp_p ##1
+ !prim_esc_rxtx_tb.resp_p, clk_i, !rst_ni || error_present)
+
+ // check correct transmission of escalation within 0-1 cycles
+ `ASSERT(EscCheck_A, ##1 esc_en_i |-> ##[0:1] esc_en_o, clk_i, !rst_ni || error_present)
+
+ // check that a single error on the diffpairs is detected
+ `ASSERT(SingleSigIntDetected0_A, {esc_err_pi, esc_err_ni} == '0 ##1
+ $onehot({resp_err_pi, resp_err_ni}) |-> integ_fail_o, clk_i, !rst_ni)
+ `ASSERT(SingleSigIntDetected1_A, $onehot({esc_err_pi, esc_err_ni}) ##1
+ {resp_err_pi, resp_err_ni} == '0 |-> integ_fail_o, clk_i, !rst_ni)
+
+ // basic liveness of FSMs in case no errors are present
+ `ASSERT(FsmLivenessSender_A, (prim_esc_rxtx_tb.i_prim_esc_sender.state_q !=
+ prim_esc_rxtx_tb.i_prim_esc_sender.Idle) |->
+ strong(##[1:$] (prim_esc_rxtx_tb.i_prim_esc_sender.state_q
+ == prim_esc_rxtx_tb.i_prim_esc_sender.Idle)), clk_i, !rst_ni || error_present)
+ `ASSERT(FsmLivenessReceiver_A, (prim_esc_rxtx_tb.i_prim_esc_receiver.state_q !=
+ prim_esc_rxtx_tb.i_prim_esc_receiver.Idle) |->
+ strong(##[1:$] (prim_esc_rxtx_tb.i_prim_esc_receiver.state_q
+ == prim_esc_rxtx_tb.i_prim_esc_receiver.Idle)), clk_i, !rst_ni || error_present)
+
+endmodule : prim_esc_rxtx_assert
