A specification says "the router enters a low-power state when idle and wakes when traffic arrives". A verification engineer has to turn that into checks. Idle for how long? What counts as idle: empty FIFOs, no locked outputs, no valid inputs? Wakes how soon? What happens to a packet that arrives while it is going to sleep? Each question is a decision someone must make, and until it is made there is nothing to check.
How do you turn a specification sentence into rules a machine can check?
The obvious approach is to read the sentence, form an impression, and write a check that matches it. The impression fills every gap with an assumption, and the check enforces that assumption. Different engineers fill the gaps differently, and none of the decisions is written down where the designer can see it. The fix is to make each gap a question, and each answer a rule.
Part of a rule | Question | Sleep example |
|---|---|---|
Trigger | When does the rule apply? | After 8 consecutive idle cycles |
Definition | What do the words mean, in signals? | Idle = all FIFOs empty, no output locked, no input valid |
Obligation | What must hold? |
|
Timing | Within how long? | In the next cycle |
Exceptions | When does it not apply? | Not when lp_en is clear |
Consequences | What else follows? | While sleeping, accept nothing and send nothing |
Worked through, the vague sentence becomes several numbered rules:
Prose: "The router enters a low-power state when idle and wakes when traffic arrives."
R13a With lp_en set, if all FIFOs are empty, no output is locked and no in_vld is high
for 8 consecutive cycles, sleeping is high in the next cycle.
R13b sleeping never rises while any output is locked.
R13c While sleeping is high, in_rdy is low on every port and out_vld is low on every port.
R13d If sleeping is high and any in_vld is high, sleeping is low in the next cycle.
R13e Credit returns (out_crd) are counted while sleeping.Each rule now maps to one check. Rules about relations between signals become assertions (Part 5); rules about results become reference-model predictions (lesson 2.3).
// snippet: two of the sleep rules as assertions
// R13c: while asleep, nothing is accepted or sent.
assert property (@(posedge clk) disable iff (rst) sleeping |-> (in_rdy == 4'b0) && (out_vld == 4'b0));
// R13d: any valid input wakes the router in the next cycle.
assert property (@(posedge clk) disable iff (rst) sleeping && (in_vld != 4'b0) |=> !sleeping);Each assertion is one rule, named after it, so a failure points straight to the sentence it enforces.
One idea per rule, numbered, so it can be referenced by checks, coverage and bug reports.
Signals, not words: every term ("idle", "full", "error") is defined in terms of signals and states.
Explicit timing: same cycle, next cycle, within N cycles, or eventually (which needs a bound before simulation can check it, Part 5).
Exceptions stated: modes, resets and configurations where the rule does not apply.
Questions filed: anything the specification does not answer becomes a specification bug (lesson 1.2), answered before the rule is final.
Practice | Purpose |
|---|---|
Numbered requirements in the specification | Every check, coverage point and bug refers to a rule |
Rule extraction as a review step | Designers and verifiers agree the rules before RTL and tests |
Assertion names matching rule numbers | Failures report the rule they break |
DCRouter's three low-power bugs each break one of the rules above: sleeping with an output locked breaks R13b, failing to wake from port 3 breaks R13d, and ignoring credit returns while asleep breaks R13e. With only the prose sentence, none of the three has a check: "wakes when traffic arrives" does not say from which port, and the credits are not mentioned at all.
For example: "full is high in a cycle if and only if the FIFO holds 8 entries; while full is high, in_rdy is low." It defines full by occupancy and states the consequence.
So checks, coverage points, test plans and bug reports can each refer to exactly one rule, and gaps are visible.
A checkable rule states trigger, definitions in signals, obligation, timing and exceptions.
Each gap in the prose becomes a question, and each answer a numbered rule.
Each rule maps to one check (an assertion or a model prediction) and to coverage.