Verification #19 · 2026-10-12 · Inline constraints · Medium · about 15 min

The inline constraint that constrains nothing

read_gen::make(addr, id, max_len) builds one random read for a directed test. The caller chooses where the read goes and which ID it carries, and randomization picks the rest:

• The returned read_txn has exactly the addr and id that were passed in.
• Its len is at most max_len (the caller passes 1 to 16), and is random within what's allowed.
• Every constraint in read_txn still holds. In particular the burst never crosses a 16-byte page: addr[3:0] + len <= 16.

Run asks for eight reads. randomize() reports no failure, but the reads that come back aren't the ones asked for. Fix gen.sv.

Write and run your answer in the browser. The hidden tests check it, and it’s free.