Describe a bus operation’s legal lengths and addresses with inside and implication, so randomize() can only produce legal operations.
Hardware context: Weighted traffic profiles for hardware coverage and stress. Generate request values from allowed hardware ranges while excluding reserved holes.
A bus carries three kinds of operation. A read moves 1, 2, 4 or 8 bytes from any address. A write moves 1 to 4 bytes and must start on a 4-byte boundary. A fence moves nothing: its length and address are both 0. Opcode 3 is reserved and must never be sent.
Write the constraint block legal in class bus_op. Use inside for the value sets and implication (->) for the rules that depend on the opcode, so each rule applies only to its own kind of operation.
For a write, lengths 1 to 4 are reachable and only addresses 0 and 4 (in this 3-bit address space). Asking for a reserved operation must fail.
Signals in the timeline
| Signal | Width | Role |
|---|---|---|
op | 2 | input of each check |
Full specification
class bus_op;
rand bit [1:0] op; // 0 read, 1 write, 2 fence, 3 reserved
rand bit [3:0] length;
rand bit [2:0] addr;
constraint legal {
}
endclass
| op | Operation | Legal length | Legal addr |
|---|---|---|---|
| 0 | read | 1, 2, 4 or 8 | any |
| 1 | write | 1 to 4 | a multiple of 4 |
| 2 | fence | 0 | 0 |
| 3 | reserved | never legal | never legal |
Each case forces op and asks for every length (address free). Then it forces op and one length together and asks for every address, so a rule that ties the address to the length is caught. It makes 3 free calls with op forced, and reports the reachable lengths, the addresses reachable with that length, and how many free calls gave a legal operation or failed.
Examples
Example 1
A write- Input
op = 1 (write), addresses tried with length 1
- Output
reachable_lengths = {1, 2, 3, 4}, addrs_for_length = {0, 4}, free_calls_legal = 3, free_calls_failed = 0
Lengths 1 to 4; a 1-byte write may start at either 4-byte-aligned address, 0 or 4.
Example 2
A fence- Input
op = 2 (fence), addresses tried with length 0
- Output
reachable_lengths = {0}, addrs_for_length = {0}, free_calls_legal = 3, free_calls_failed = 0
Only length 0 and address 0 can be solved.
Example 3
The reserved opcode- Input
op = 3 (reserved), addresses tried with length 1
- Output
reachable_lengths = {}, addrs_for_length = {}, free_calls_legal = 0, free_calls_failed = 3
Nothing is reachable and all 3 free calls fail.
Constraints and contract
- Only the class’s constraint block changes.
- A rule for one opcode must not restrict the others.
- Keep the class, field and constraint names.
Hints
Hint 1
Start with the rule that holds for every operation: which opcodes may appear at all?
Hint 2
A -> B constrains B only when A is true. When A is false, the rule says nothing.
Hint 3
Write one implication per opcode. A write needs two conditions on its right-hand side, joined with &&.
What this judge verifies: For every opcode every length is forced, and for eight (opcode, length) pairs every address, and free calls are judged by a second copy of the rules. Passing shows the constraint allows the legal operations probed here and refuses the illegal ones.
8 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 6 steps and the final capstone