rand, inside, ranges, %, implication

Runs: every solve was legal

Runs the real solver many times and checks every result

randc

Runs: every block of N calls was a full permutation

Runs it

dist with := and :/

Runs: measured shares within about 1.5 points of the predicted weights

Shows measured shares beside the predicted ones

dist after another constraint removes a listed value

Differs a little: about 90% where renormalising the weights gives 93.1%

Shows both numbers

dist written with enum names (DATA := 85)

Differs: the weights were ignored and every name came out about equally often. Numeric values (0 := 85) worked, even on an enum variable

Writes the numeric values, with the names in a comment

Uniform choice over the legal solutions

Differs: err -> addr == 0 gave err about 8.5% of the time, where a uniform pick over the 17 solutions gives 5.9%. With len deciding which payload bytes are zero, lengths 7 and 8 came out 91% of the time. x inside {[0:1000]} with a hole at 100 to 200 gave values below 100 in under 4% of calls, against 11% uniform; $countones(a ^ b) == 1 flipped bit 6 in 272 of 300 calls. With blen inside {[1:16]} beside a 32-bit addr, length 16 came up about a third as often as uniform, and odd lengths more often than even

Teaches the standard's numbers and shows Verilator's measured numbers next to them

solve ... before

Differs, and not consistently: in one test the flag came out about 30% where the standard gives 50%; in another it was never set at all; on a starved enable bit it gave 26% where the standard gives 50%. Every solve stayed legal. A dist on the bit gave the full 50%

Teaches the standard's numbers; the benches check legality and print the measured rates

soft, including two softs in conflict

Runs: a hard rule discards the soft one, and the later of two softs wins, as the standard says

Runs it

soft on a dist

Differs: the weights applied, but a hard inline rule that contradicted the soft dist made randomize() fail instead of discarding it

Says so; the bench checks only the weights

constraint_mode(), rand_mode()

Runs. Reading constraint_mode() directly inside if (...) is rejected; read it into a variable first

Uses the variable form

pre_randomize, post_randomize

Runs, but post_randomize also runs after a failed randomize(), which the standard forbids

Says so where hooks are taught

A contradiction: randomize() returns 0, fields unchanged

Runs, with an UNSATCONSTR warning

Runs it

std::randomize() with, $urandom_range, srandom

Runs

Runs them

Object random stability: an object seeded at new(), unaffected by later draws or other objects

Runs, as the standard says; an extra new() before it shifted its values

Runs it

std::process get_randstate and set_randstate

Runs: restoring the state repeated the next draw

Runs it

$urandom(seed) to reseed a thread before building objects

Runs on its own. Once the design names std::process anywhere, $urandom(seed) stopped reseeding what new() draws from; process::self().srandom(seed) still worked

Reseeds with process::self().srandom(seed)

A function call in a constraint (total_len >= min_len(n))

Differs, in the helpful direction: the argument was not solved first, so a later bound pushed back through the call. 400 of 400 calls solved where the standard's order makes most of them fail

Teaches the standard's order and shows Verilator's result

randc constrained together with a rand field (data > slot)

Differs: the randc field was solved together with the rand one. slot == 15, which leaves no legal data, was never dealt, so the standard's failure never happened

Teaches the standard's order and shows Verilator's result

randomize(null) (check only)

Rejected: "Unsupported"

Shown as a fragment

randomize(field) (randomize one field)

Differs: other rand fields changed too

Uses rand_mode(0) on the fields that must stay

Dynamic array size() with foreach

Runs

Runs it

sum() on a fixed-size array

Runs

Runs it

sum() with no widening with

Differs: the total was computed wide, so b.sum() == 600 on four bytes solved, with bytes totalling 600. The standard sums in the element width, where 600 cannot fit

Teaches the widened form, which is right on every tool, and shows Verilator's result

item.index inside a reduction's with

Differs: the solver stopped with an internal error, and later solves in the same run went wrong

Zeroes unused bytes, so the reduction runs over the whole array

A size whose elements are infeasible (data[i] == data.size() * 2 on 4-bit elements)

Better than the standard promises: 300 of 300 calls solved, using only the feasible sizes 1 to 7

Teaches the standard's size-first risk and shows Verilator's result

size() together with sum() on a dynamic array

Differs: every solve failed as unsatisfiable

Uses a fixed-size array plus a length field

unique { arr }

Runs on a fixed-size array when another rule also names its elements (such as a range); with unique alone, 85 of 100 results repeated a value. On a dynamic array, or a list mixing scalars and an array, it was ignored with a CONSTRAINTIGN warning: 50 of 50 results repeated a value

Uses unique on fixed-size arrays and the written-out form, arr[i] != arr[j] for every pair, elsewhere

dist on an element that another rule also pins (a counting sum(), or gap[k] == 0)

Differs: about a third of the calls failed as unsatisfiable, though legal answers existed

Keeps the dist off the pinned element with a guard

One rand class handle inside another

Runs, including constraints across the two objects

Runs it

A null rand class handle, never built

Runs as the standard says when the handle's class has no constraints: skipped, and randomize() returned 1. When the class has its own constraints, the run stopped with "Null pointer dereferenced"

Builds every rand handle in new(); the lesson says what each tool does

A null-handle guard in a constraint (prev != null -> addr > prev.addr)

Differs: the handle was dereferenced anyway and the run stopped with "Null pointer dereferenced", in both the -> and the if form

Copies the value into a plain field plus a "have previous" bit

A constraint that reads another object's rand field through a plain handle (burst <= cfg.max_burst)

Differs: after that, cfg.randomize() returned 1 but no longer changed max_burst

Copies the configuration value into a plain field of the transaction

Arrays of rand class handles

Differs: each element's own constraints were ignored

Shown as a fragment, with a fixed-size field array as the runnable form

|->, |=>, ##N, ##[m:n] at the end, disable iff

Runs: right verdicts, including the failing cases

Runs real assertions with a planted bug

Multi-step sequences in an assertion: repetition and and in a consequent, a range or goto followed by more (##[1:3] ack ##1 done, in the antecedent or the consequent; ack [->3] ##1 done)

Differs, depending on where the trace breaks: busy [*4] and inline and caught a pattern that broke on its last tick but missed one that broke on its second; the range-then-more and goto-then-more forms missed every planted failure. Covers on the same sequences counted their matches correctly

Teaches the full forms; benches show the compact form's count beside a form that works: fixed delays, written-out repetition, a split into simple implications, or a few lines of modeling code

Goto b [->N] starting on a cycle where b is already 1

Differs: that occurrence was not counted, so $rose(b) ##0 b [->3] never matched b = 1 0 1 1. Started on a cycle where b is 0, the same goto matched correctly

Starts goto counts on a cycle before the first event

first_match(...) followed by more sequence

Differs: matched nothing, as an assert or a cover

Uses a flag set by modeling code for the first event

throughout over a fixed window

Runs: caught a planted abort

Runs it

A named sequence whose body has ## after its first item (sequence s; a ##1 b; endsequence)

Rejected: "Cycle delays not allowed as intra-assignment delays", with or without a default clocking block. A body that starts with the delay (##[1:4] gnt) is accepted

Writes the sequence inline in the property, and says where a named sequence would go

cover sequence

Ignored with a COVERIGN warning; it never counted

Uses cover property, which counts once per attempt that matched

$rose, $fell, $stable, $changed, $past(x), $past(x, N)

Runs

Runs them

$past(x, N, enable) (gated)

Rejected: "Unsupported: $past expr2 and/or clock arguments"

Uses a small flop to hold the gated value

$onehot, $onehot0, $countones

Runs

Runs them

$isunknown and X in checks

Never fires: Verilator is 2-state, so X becomes 0 or 1

Shows X behaviour on Icarus with immediate checks

b[*3] as a consequent

Differs: when b held for the first repetition and dropped on the second, the failure was missed

Writes b ##1 b ##1 b, which failed correctly on the same trace

!x straight after ##1 or after a repetition, even as ##1 (!x)

Rejected: "Unexpected 'not' in sequence expression context"

Writes ##1 ~x or ##1 (x == 0)

$error in an action block, or a failing assertion with no action block

Stops the run at the first failure: the default error limit is 1. The run-time option +verilator+error+limit+N raises it

Counts failures in the action block (else fails++) so a bench can plant bugs and keep going, and says so

if / else inside a property

Rejected: "Unsupported: property case expression"

Writes one implication per arm

nexttime, always [m:n], s_until

Rejected: "Unsupported"

Writes ##1, a fixed repetition, or until

until, until_with, implies, iff

Runs: right verdicts on a known trace

Runs them

Sequence or, between named sequences or inline

Runs: the cover counted the right match with --coverage

Runs it

Ranged goto [->m:n]

Rejected: "Unsupported"

Uses a fixed [->N] or a counter

within with a ranged delay

Rejected: "Unsupported"

Shown as a fragment

intersect, non-consecutive [=N]

Rejected: the tool stopped with an internal error

Shown as fragments, with a counter as the runnable form

first_match

Runs (cover count correct)

Runs it

.triggered on a sequence, s_eventually, strong, expect, checker

Rejected

Shown as fragments

Local variables in a property

Differs: compiled, but the captured value was not held, so the verdict was wrong

Uses a small scoreboard instead; the Expert part has the details

cover property

Counts correctly with --coverage; without it the cover is dropped and its action never runs

Builds covers with --coverage

Immediate assert, assert final, $assertoff, $asserton, bind

Runs

Runs them

covergroup, coverpoint, bins, cross

Verilator 5.048 compiles them with a COVERIGN warning and ignores the bins: get_inst_coverage() reads 0.0 even when every bin was hit. Icarus 13 does not support them

Teaches the real syntax, and gets real numbers from a small bins model written in plain classes, which runs and prints a report shaped like a simulator's

Code coverage (lines, toggles)

Verilator runs it with --coverage; verilator_coverage writes the report

Shows real line coverage where code and functional coverage are compared

cover property counts

Counted with --coverage

Used as the third coverage instrument