[fpv] alert_rx/tx updates
Add support for alert_rx/tx new interface ports: `alert_req_i`,
`alert_ack_o`.
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_bind_fpv.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_bind_fpv.sv
index 3afa607..6e96ee6 100644
--- a/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_bind_fpv.sv
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_bind_fpv.sv
@@ -18,7 +18,8 @@
.alert_err_pi,
.alert_err_ni,
.alert_skew_i,
- .alert_i,
+ .alert_req_i,
+ .alert_ack_o,
.ping_req_i,
.ping_ok_o,
.integ_fail_o,
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_fpv.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_fpv.sv
index d98bbc0..786345f 100644
--- a/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_fpv.sv
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_async_fpv.sv
@@ -22,8 +22,9 @@
input alert_err_ni,
input [1:0] alert_skew_i,
// normal I/Os
- input alert_i,
+ input alert_req_i,
input ping_req_i,
+ output logic alert_ack_o,
output logic ping_ok_o,
output logic integ_fail_o,
output logic alert_o
@@ -68,9 +69,10 @@
prim_alert_sender #(
.AsyncOn ( AsyncOn )
) i_prim_alert_sender (
- .clk_i ,
- .rst_ni ,
- .alert_i ,
+ .clk_i ,
+ .rst_ni ,
+ .alert_req_i,
+ .alert_ack_o,
.alert_rx_i ( alert_rx_in ),
.alert_tx_o ( alert_tx_out )
);
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_bind_fpv.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_bind_fpv.sv
index a46902c..18071d1 100644
--- a/hw/ip/prim/fpv/tb/prim_alert_rxtx_bind_fpv.sv
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_bind_fpv.sv
@@ -15,7 +15,8 @@
.ack_err_ni,
.alert_err_pi,
.alert_err_ni,
- .alert_i,
+ .alert_req_i,
+ .alert_ack_o,
.ping_req_i,
.ping_ok_o,
.integ_fail_o,
diff --git a/hw/ip/prim/fpv/tb/prim_alert_rxtx_fpv.sv b/hw/ip/prim/fpv/tb/prim_alert_rxtx_fpv.sv
index 23f3c1f..a202340 100644
--- a/hw/ip/prim/fpv/tb/prim_alert_rxtx_fpv.sv
+++ b/hw/ip/prim/fpv/tb/prim_alert_rxtx_fpv.sv
@@ -19,8 +19,9 @@
input alert_err_pi,
input alert_err_ni,
// normal I/Os
- input alert_i,
+ input alert_req_i,
input ping_req_i,
+ output logic alert_ack_o,
output logic ping_ok_o,
output logic integ_fail_o,
output logic alert_o
@@ -43,9 +44,10 @@
prim_alert_sender #(
.AsyncOn ( AsyncOn )
) i_prim_alert_sender (
- .clk_i ,
- .rst_ni ,
- .alert_i ,
+ .clk_i ,
+ .rst_ni ,
+ .alert_req_i,
+ .alert_ack_o,
.alert_rx_i ( alert_rx_in ),
.alert_tx_o ( alert_tx_out )
);
diff --git a/hw/ip/prim/fpv/vip/prim_alert_rxtx_assert_fpv.sv b/hw/ip/prim/fpv/vip/prim_alert_rxtx_assert_fpv.sv
index 8f444dc..70cfd6a 100644
--- a/hw/ip/prim/fpv/vip/prim_alert_rxtx_assert_fpv.sv
+++ b/hw/ip/prim/fpv/vip/prim_alert_rxtx_assert_fpv.sv
@@ -18,7 +18,8 @@
input alert_err_pi,
input alert_err_ni,
// normal I/Os
- input alert_i,
+ input alert_req_i,
+ input alert_ack_o,
input ping_req_i,
input ping_ok_o,
input integ_fail_o,
@@ -38,9 +39,9 @@
// 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_req_i && ping_ok_o |=> !ping_req_i, clk_i, !rst_ni)
- `ASSUME_FPV(PingEnStaysAsserted0_M, ping_req_i |=> (ping_req_i && !ping_ok_o) or
- (ping_req_i && ping_ok_o ##1 $fell(ping_req_i)), clk_i, !rst_ni || error_present)
-
+ `ASSUME_FPV(PingEn_M, $rose(ping_req_i) |-> ping_req_i throughout
+ (ping_ok_o || error_present)[->1] ##1 $fell(ping_req_i),
+ clk_i, !rst_ni)
sequence FullHandshake_S;
$rose(prim_alert_rxtx_fpv.alert_tx_out.alert_p) ##1
$rose(prim_alert_rxtx_fpv.alert_rx_out.ack_p) &&
@@ -55,27 +56,37 @@
// only take place if both FSMs are in a sane state
`ASSERT(PingHs_A, ##1 $changed(prim_alert_rxtx_fpv.alert_rx_out.ping_p) &&
(prim_alert_rxtx_fpv.i_prim_alert_sender.state_q ==
- prim_alert_rxtx_fpv.i_prim_alert_sender.Idle ) &&
+ prim_alert_rxtx_fpv.i_prim_alert_sender.Idle) &&
(prim_alert_rxtx_fpv.i_prim_alert_receiver.state_q ==
- prim_alert_rxtx_fpv.i_prim_alert_receiver.Idle )|=> FullHandshake_S,
+ prim_alert_rxtx_fpv.i_prim_alert_receiver.Idle)|=> FullHandshake_S,
clk_i, !rst_ni || error_present)
- `ASSERT(AlertHs_A, alert_i &&
+ `ASSERT(AlertHs_A, alert_req_i &&
(prim_alert_rxtx_fpv.i_prim_alert_sender.state_q ==
prim_alert_rxtx_fpv.i_prim_alert_sender.Idle) &&
(prim_alert_rxtx_fpv.i_prim_alert_receiver.state_q ==
prim_alert_rxtx_fpv.i_prim_alert_receiver.Idle) |=>
- FullHandshake_S, clk_i, !rst_ni || error_present)
+ FullHandshake_S |-> alert_ack_o, clk_i, !rst_ni || error_present)
// transmission of pings
- `ASSERT(AlertPing_A, !error_present ##1 $rose(ping_req_i) |->
+ // note: the complete transmission of pings only happen when no ping handshake is in progress
+ `ASSERT(AlertPingOk_A, !(prim_alert_rxtx_fpv.i_prim_alert_sender.state_q inside {
+ prim_alert_rxtx_fpv.i_prim_alert_sender.PingHsPhase1,
+ prim_alert_rxtx_fpv.i_prim_alert_sender.PingHsPhase2}) && $rose(ping_req_i) |->
##[1:9] ping_ok_o, clk_i, !rst_ni || error_present)
+ `ASSERT(AlertPingIgnored_A, (prim_alert_rxtx_fpv.i_prim_alert_sender.state_q inside {
+ prim_alert_rxtx_fpv.i_prim_alert_sender.PingHsPhase1,
+ prim_alert_rxtx_fpv.i_prim_alert_sender.PingHsPhase2}) && $rose(ping_req_i) |->
+ ping_ok_o == 0 throughout ping_req_i [->1], clk_i, !rst_ni || error_present)
// transmission of alerts in case of no collision with ping enable
- `ASSERT(AlertCheck0_A, !ping_req_i [*3] ##0 $rose(alert_i) &&
+ `ASSERT(AlertCheck0_A, !ping_req_i [*3] ##0 $rose(alert_req_i) &&
(prim_alert_rxtx_fpv.i_prim_alert_sender.state_q ==
prim_alert_rxtx_fpv.i_prim_alert_sender.Idle) |=>
alert_o, clk_i, !rst_ni || error_present || ping_req_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)
+ // transmission of alerts in the general case which can include continous ping collisions
+ `ASSERT(AlertCheck1_A, alert_req_i |=>
+ strong(##[1:$] ((prim_alert_rxtx_fpv.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_fpv.i_prim_alert_sender.Idle) && !ping_req_i) ##1 alert_o),
+ clk_i, !rst_ni || error_present || alert_ack_o)
// basic liveness of FSMs in case no errors are present
`ASSERT(FsmLivenessSender_A,
diff --git a/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv b/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv
index 07dc1f5..c1cf394 100644
--- a/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv
+++ b/hw/ip/prim/fpv/vip/prim_alert_rxtx_async_assert_fpv.sv
@@ -21,7 +21,8 @@
input alert_err_ni,
input [1:0] alert_skew_i,
// normal I/Os
- input alert_i,
+ input alert_req_i,
+ input alert_ack_o,
input ping_req_i,
input ping_ok_o,
input integ_fail_o,
@@ -57,10 +58,9 @@
// 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_req_i && ping_ok_o |=> !ping_req_i, clk_i, !rst_ni)
- `ASSUME_FPV(PingEnStaysAsserted0_M, ping_req_i |=>
- (ping_req_i && !ping_ok_o) or
- (ping_req_i && ping_ok_o ##1 $fell(ping_req_i)),
- clk_i, !rst_ni || error_present)
+ `ASSUME_FPV(PingEn_M, $rose(ping_req_i) |-> ping_req_i throughout
+ (ping_ok_o || error_present)[->1] ##1 $fell(ping_req_i),
+ clk_i, !rst_ni)
// 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.
@@ -83,26 +83,37 @@
(prim_alert_rxtx_async_fpv.i_prim_alert_receiver.state_q ==
prim_alert_rxtx_async_fpv.i_prim_alert_receiver.Idle) |-> ##[0:5] FullHandshake_S,
clk_i, !rst_ni || error_setreg_q)
- `ASSERT(AlertHs_A, alert_i &&
+ `ASSERT(AlertHs_A, alert_req_i &&
(prim_alert_rxtx_async_fpv.i_prim_alert_sender.state_q ==
prim_alert_rxtx_async_fpv.i_prim_alert_sender.Idle) &&
(prim_alert_rxtx_async_fpv.i_prim_alert_receiver.state_q ==
- prim_alert_rxtx_async_fpv.i_prim_alert_receiver.Idle) |-> ##[0:5] FullHandshake_S,
+ prim_alert_rxtx_async_fpv.i_prim_alert_receiver.Idle) |-> ##[0:5] FullHandshake_S
+ ##[0:5] alert_ack_o,
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_req_i) |-> ##[1:23] ping_ok_o,
- clk_i, !rst_ni || error_setreg_q)
+ // note: the complete transmission of pings only happen when no ping handshake is in progress
+ `ASSERT(AlertPingOk_A, !(prim_alert_rxtx_async_fpv.i_prim_alert_sender.state_q inside {
+ prim_alert_rxtx_async_fpv.i_prim_alert_sender.PingHsPhase1,
+ prim_alert_rxtx_async_fpv.i_prim_alert_sender.PingHsPhase2}) && $rose(ping_req_i) |->
+ ##[1:23] ping_ok_o, clk_i, !rst_ni || error_setreg_q)
+ `ASSERT(AlertPingIgnored_A, (prim_alert_rxtx_async_fpv.i_prim_alert_sender.state_q inside {
+ prim_alert_rxtx_async_fpv.i_prim_alert_sender.PingHsPhase1,
+ prim_alert_rxtx_async_fpv.i_prim_alert_sender.PingHsPhase2}) && $rose(ping_req_i) |->
+ ping_ok_o == 0 throughout ping_req_i[->1], clk_i, !rst_ni || error_setreg_q)
// transmission of first alert assertion (no ping collision)
- `ASSERT(AlertCheck0_A, !ping_req_i [*10] ##1 $rose(alert_i) &&
+ `ASSERT(AlertCheck0_A, !ping_req_i [*10] ##1 $rose(alert_req_i) &&
(prim_alert_rxtx_async_fpv.i_prim_alert_sender.state_q ==
prim_alert_rxtx_async_fpv.i_prim_alert_sender.Idle) |->
##[3:5] alert_o, clk_i, !rst_ni || ping_req_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)
+ // eventual transmission of alerts in the general case which can include continous ping
+ // collisions
+ `ASSERT(AlertCheck1_A, alert_req_i |->
+ strong(##[1:$] (prim_alert_rxtx_async_fpv.i_prim_alert_sender.state_q ==
+ prim_alert_rxtx_async_fpv.i_prim_alert_sender.Idle && !ping_req_i) ##[3:5] alert_o),
+ clk_i, !rst_ni || error_setreg_q || alert_ack_o)
// basic liveness of FSMs in case no errors are present
`ASSERT(FsmLivenessSender_A, !error_present [*2] ##1 !error_present &&
