Skip to content

[alert,fpv] Remove nonsense AlertPingIgnored_A assertion#29647

Open
rswarbrick wants to merge 1 commit intolowRISC:masterfrom
rswarbrick:silly-alert-assertion
Open

[alert,fpv] Remove nonsense AlertPingIgnored_A assertion#29647
rswarbrick wants to merge 1 commit intolowRISC:masterfrom
rswarbrick:silly-alert-assertion

Conversation

@rswarbrick
Copy link
Copy Markdown
Contributor

The AlertPingIgnored_A assertion in the code before this commit didn't make all that much sense.

It says:

"If the alert sender is in the middle of replying to a ping and the
alert receiver gets asked to send a new ping then the receiver's
ping_ok_o output will be false until (and including) the first time
that the receiver is being asked to send a ping"

That's a rather convoluted way of saying:

"If the alert sender is in the middle of replying to a ping and the
alert receiver gets asked to send a new ping then the receiver's
ping_ok_o output will be false".

Since requests to the alert receiver are under the control of the environment in the formal testbench, this can be simplified to:

"If the alert sender is in the middle of replying to a ping then the
receiver's ping_ok_o output will be false".

That is true, and it means that the receiver won't ever manufacture extra ping_ok_o signals. But doing so isn't really a concern: they would cause the spurious_alert_ping signal in alert_handler_ping_timer to go high, which is treated as a ping failure.

I'm not entirely sure what the author intended from the assertion (added in c8fb0e6), but I can't really see any benefit to the code that's here.

The AlertPingIgnored_A assertion in the code before this commit didn't
make all that much sense.

It says:

  "If the alert sender is in the middle of replying to a ping and the
  alert receiver gets asked to send a new ping then the receiver's
  ping_ok_o output will be false until (and including) the first time
  that the receiver is being asked to send a ping"

That's a rather convoluted way of saying:

  "If the alert sender is in the middle of replying to a ping and the
  alert receiver gets asked to send a new ping then the receiver's
  ping_ok_o output will be false".

Since requests to the alert receiver are under the control of the
environment in the formal testbench, *this* can be simplified to:

  "If the alert sender is in the middle of replying to a ping then the
  receiver's ping_ok_o output will be false".

That is true, and it means that the receiver won't ever manufacture
extra ping_ok_o signals. But doing so isn't really a concern: they
would cause the spurious_alert_ping signal in alert_handler_ping_timer
to go high, which is treated as a ping failure.

I'm not entirely sure what the author intended from the
assertion (added in c8fb0e6), but I can't really see any benefit
to the code that's here.

Signed-off-by: Rupert Swarbrick <rswarbrick@lowrisc.org>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Component:FPV FPV issue: formal testbench, property, etc IP:alert_handler

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant