[alert,fpv] Dramatic improvements to the async alert fpv #27557
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
rswarbrick
added
Component:FPV
Contributor
Author
|
Hmm. I've just reconsidered about adding the assertion to |
rswarbrick
force-pushed
the
async-alert-fpv
branch
3 times, most recently
from
b023be7 to
bf92b99
Compare
Contributor
|
Just a question about last commit ( |
rswarbrick
force-pushed
the
async-alert-fpv
branch
from
bf92b99 to
4d38377
Compare
Contributor
Author
|
I think you're probably right (and, if not, it will need a bit of thought!) I've just rebased and dropped that commit. |
rswarbrick
force-pushed
the
async-alert-fpv
branch
from
4d38377 to
a118fee
Compare
rswarbrick
force-pushed
the
async-alert-fpv
branch
2 times, most recently
from
c2758f7 to
e9f9283
Compare
Contributor
Author
|
The latest force-push gets things working properly again (fixing a botched rebase I did a few minutes ago, plus a changed variable name in |
Contributor
marnovandermaas
left a comment
marnovandermaas
left a comment
There was a problem hiding this comment.
Some initial comments from a code read through. I should run these properties through before approving.
Contributor
|
I just ran the proof, there are:
|
marnovandermaas
approved these changes
Jan 27, 2026
Contributor
marnovandermaas
left a comment
marnovandermaas
left a comment
There was a problem hiding this comment.
Approving this because the proof runs correctly. It would be nice to get some of the nits resolved before merging though.
If you have a sequence that looks like "A ##1 B ##1 C ##1 D", Jasper turns out to take quite a long time to compile it. This is rather annoying, and you can actually hit a timeout. It seems that the Cadence engineers realised that they could do things more efficiently and put it behind a flag (presumably because the change pessimizes some other example). Ask for the new behaviour, provided we are on a version of Jasper that supports it. The magic regex should hopefully match properly. I tested it with the following shell script: pattern="^\(20[3-9][0-9]\)\|\(202[4-9]\)\|\(2023\.\(0[69]\)\|12\)" echo -e '2023.05\n2023.06\n2023.12\n2024\n2031' | grep $pattern This is like the regex in the TCL file, except that a TCL regex needs "\" before the square brackets (not what we want for grep, because "\[" would match a literal "[") And this gives the results you'd hope for: 2023.06 2023.12 2024 2031 Signed-off-by: Rupert Swarbrick <[email protected]> Signed-off-by: Rupert Swarbrick <[email protected]>
This is important if you want to apply a stopat to some assertion, so put that assertion in a task, but need that assertion to count towards coverage for the run. Signed-off-by: Rupert Swarbrick <[email protected]>
rswarbrick
force-pushed
the
async-alert-fpv
branch
from
e9f9283 to
de45f80
Compare
rswarbrick
commented
Jan 30, 2026
When doing FPV, the model checker can end up searching in an unreachable state where it happens to have started with a differential decoder in state 2'b11. To avoid it wasting lots of time looking at "stuck" unreachable states, prove that this can't happen. The "after_load" script registers this property as a helper, which should mean state space exploration for things driven by the level of this signal doesn't get stuck looking at unreachable states where state_q is a constant 2'b11. Signed-off-by: Rupert Swarbrick <[email protected]>
No functional change, but this should make things a little easier to read. Signed-off-by: Rupert Swarbrick <[email protected]>
Signed-off-by: Rupert Swarbrick <[email protected]>
The old version of this assertion had a bit of a hole in it. Digging
into the SVA, we see:
$rose(prim_alert_rxtx_async_tb.alert_pd) ##[3:6]
$rose(prim_alert_rxtx_async_tb.ack_pd) &&
$stable(prim_alert_rxtx_async_tb.alert_pd) ##[3:6] ....
This says "alert_p rises and then in between 3 and 6 cycles ack_p
rises and alert_p is stable at that point". That's not quite what we
want!
We really want to say "alert_p rises and then stays stable for up to 6
cycles at which point ack_p rises."
I've rephrased it slightly and also been a bit more careful about
differential signals and who is seeing what. Now, the FullHandshake_S
sequence is explicitly from the alert sender's point of view.
Signed-off-by: Rupert Swarbrick <[email protected]>
No change in meaning, but the result is a bit less verbose. Signed-off-by: Rupert Swarbrick <[email protected]>
This has an equivalent meaning, except that I added an extra disable condition to AlertReqAck_A. That extra condition shouldn't really be a problem: this is saying that if I ask an alert sender to send an alert then it will eventually get a response. Of course, that's not true if someone cut the wires! But we don't care because the receiver will eventually see a failed ping. Signed-off-by: Rupert Swarbrick <[email protected]>
This is equivalent, but rather less complicated! The trick is that all the !error_present items in the preconditions are implied by the fact that error_present is part of the disable iff. As a plus, this also tidies up an embarrassing bug that I added in commit 373d8ba. Signed-off-by: Rupert Swarbrick <[email protected]>
The original version of this assertion said "if I ask the alert sender for an alert then eventually the alert receiver will report it". Commit c8fb0e6 made this rather more complicated by requiring the sender to go back to the idle state before that happens. This may well be true, but I can't really see any need (and it rather mixes the two ends' timelines). Simplify the assertion again. Signed-off-by: Rupert Swarbrick <[email protected]>
The code is completely equivalent, but there's now some proper documentation about what it means. The non-macro version of the assertion is also rather easier to read because the "disable bit" is easier to recognise. Signed-off-by: Rupert Swarbrick <[email protected]>
This assertion wasn't true because a skew on e.g. the ack signal from the alert receiver to the alert sender can completely lock up communication between them. It seems that Jasper didn't manage to find the loop it would need for a counterexample with this sort of liveness proof, so it just hung. With the extra condition (which, in hindsight, is definitely required), the proof goes through nicely. Signed-off-by: Rupert Swarbrick <[email protected]>
Signed-off-by: Rupert Swarbrick <[email protected]>
This is equivalent, but a bit easier to read (as a bonus, it also avoids making s_eventually look like a function name). Signed-off-by: Rupert Swarbrick <[email protected]>
rswarbrick
force-pushed
the
async-alert-fpv
branch
from
b33b756 to
0c5dbb8
Compare
Contributor
Author
|
Force-push has just run through CI. I don't believe it can possibly have affected FPGA results, so am merging. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This testing was failing before the change in PR #27531 (the first commit in this PR). But that change is still rather unsatisfying: the test contemplates life for a few hours without finding a counterexample, but doesn't complete the proofs.
The remainder of these commits make the proofs actually complete. Amusingly, the assertions still weren't quite all true (see "[alert,fpv] Make AlertCheck1_A actually true for async alerts", but Jasper didn't manage to find a counterexample to the liveness property). That PR tweaks the assertion to make it work properly.
Finally, the last two commits are driven by trying to close coverage, and they get us to 100%.
Note that there are two commits in this PR that are not specifically about alerts (commits 2 and 3).
FullHandshake_Swas compiled very slowly for the async testbench. That was annoying before the change, so it seems like a good idea to tell Jasper to be quicker!