Write the hold rule as an assertion and catch two sources that break it while stalled.
Hardware context: Protocol assertions for a synchronous request/response interface. Assert the read-channel hold rule and catch sources that change a stalled offer.
A read source offers a beat with rvalid and waits for rready. Until the beat transfers, the offer must not change: rvalid stays 1 and rdata stays the same. A DUT that changes either one while stalled can make a consumer take the wrong data.
Write rd_rules: a checker module with one assertion for this rule, counting each failure in errors. A copy of it watches the correct source and two buggy ones, and the same four scenarios drive all three.
You pass when your count stays at 0 on the correct source and goes up on both buggy ones. One scenario resets the source while a beat is stalled: the correct source drops rvalid then, and that is not a failure.
Signals in the timeline
| Signal | Width | Role |
|---|---|---|
clk | 1 | stimulus, the same for every design |
rst_n | 1 | stimulus, the same for every design |
arvalid | 1 | stimulus, the same for every design |
arid | 4 | stimulus, the same for every design |
rvalid | 1 | output of the design under test |
rready | 1 | stimulus, the same for every design |
rlast | 1 | output of the design under test |
rid | 4 | output of the design under test |
rdata | 8 | output of the design under test |
your errors | 32 | your checker's error count |
Full specification
module rd_rules (
input logic clk, rst_n,
input logic arvalid,
input logic [3:0] arid,
input logic [7:0] araddr,
input logic rvalid, rready, rlast,
input logic [3:0] rid,
input logic [7:0] rdata,
output int errors
);
// your assertions
endmodule
| Rule of the read source | Detail |
|---|---|
| Request | arvalid = 1 at an edge asks for a burst of four beats. The stimulus asks only when no burst is in progress. |
| First beat | rvalid rises within 1 to 3 edges of the request (the correct source takes 2). |
| Hold | While rvalid = 1 and rready = 0, rvalid stays 1 and rdata stays the same at the next edge. |
| Beats | A transfer is an edge with rvalid && rready. rlast is 1 on the fourth transfer and 0 on the first three. |
| rlast | rlast is 1 only while rvalid is 1. |
| Data | Beat b (0 to 3) carries rdata = (araddr + b) ^ 8'hA5 and rid = arid of its request. |
| Nothing extra | rvalid is 1 only while a burst is outstanding: from the request until its fourth transfer. |
| Reset | rst_n = 0 at an edge ends any burst: rvalid is 0 at the next edge, even if reset is still held. |
Only the Hold rule is graded here; the other rules of the table describe what the correct source does.
Every scenario starts with a start-up edge (cycle 1) and a reset edge (cycle 2). Scenarios: 1. Two bursts, rready always high; 2. Long stalls; 3. Reset during a stalled offer; 4. Three requests, random rready. Inputs change at falling edges and hold across the next rising edge.
Count each failure in errors from the else action of your assertion (errors++). errors never goes down. For each source you get alarm = yes or no; for the correct source, also the scenario and cycle of your first alarm.
Simulator note: The grading simulator runs a measured subset of SVA. Goto [->n], [=n], sequence or, first_match, intersect, within, cover, ranged delays in an antecedent, a ranged repetition followed by more sequence, and $error/$fatal/$stop are refused before simulation, with a suggested alternative. Every assertion needs an else action.
Examples
Example 1
The correct source must not raise an alarm- Input
Source: the correct design Scenarios: 4
- Output
alarm = no
In scenario 3 a reset lands on a stalled beat and the source drops rvalid. With disable iff, that attempt is disabled, not failed.
Example 2
A dropped offer must be caught- Input
Source: rvalid drops while stalled Scenarios: 4
- Output
alarm = yes
In scenario 2 the beat stalls for three edges; on the third this source lowers rvalid.
Example 3
Changing data must be caught- Input
Source: rdata changes while stalled Scenarios: 4
- Output
alarm = yes
In scenario 2 this source changes rdata while the beat waits.
Constraints and contract
- Use only your ports and concurrent assertions with small auxiliary models.
- Every assertion has an else action that counts the failure in errors.
- Stay inside the supported SVA subset described in the specification.
Hints
Hint 1
The rule starts at an edge where the beat is offered but not taken. What must be true at the next edge?
Hint 2
$stable(x) compares this edge’s sample of x with the previous edge’s.
Hint 3
Start an attempt only on edges where the beat waits, and check the following edge. Leave reset to the default disable iff, so a reset ends the attempt instead of failing it.
What this judge verifies: Your checker runs against the correct read source and 2 variants with one planted bug each, over 4 fixed scenarios. Passing shows it catches these bugs on this stimulus, not every possible protocol bug.
3 checks on Verilator · local server. Run the examples first, then check the full regression. The suite is local and inspectable. A passing result establishes the tested cases, not a proof for all possible inputs.
See all 13 steps and the final capstone