Difficulty: Medium · Puzzle 2 of 6 · Topic: solve...before Bias Puzzles
Compute tuple-count P(kind==2) without solve-before, then the exact P(kind==2) with solve kind before len.
class sb_kind_len;
rand bit [1:0] kind;
rand bit [2:0] len;
constraint c_dom { kind inside {0,1,2}; }
constraint c_link {
if (kind == 0) len == 0;
else if (kind == 1) len inside {[0:1]};
else len inside {[0:7]};
}
// compare with and without: solve kind before len;
endclassBranch cardinalities are 1, 2, and 8. kind=3 has no legal completion.
1) Legal tuples by kind: kind0->1 tuple, kind1->2 tuples, kind2->8 tuples, total=11.
2) Without solve-before: P(kind==2)=8/11.
3) With solve kind before len: kind is chosen first, uniformly over values that have a legal completion. kind=3 is excluded by c_dom, so the feasible values are {0,1,2} and P(kind==2)=1/3 exactly.
4) The legal set (11 tuples) is the same in both variants.Answer: Without solve-before, P(kind==2)=8/11 (~72.73%); with `solve kind before len`, P(kind==2)=exactly 1/3 (kind uniform over {0,1,2}); legality is unchanged.
Checked by running a model of the rule in a Python model and Verilator 5. Exact enumeration of the constraint set per the LRM (the LRM defines the distribution; simulator solvers need not be uniform). kind=3 has no legal completion, so with solve kind before len the draw is uniform over {0,1,2}. Verilator 5.048 legality only: every result is one of the 11 legal tuples (the ordering is ignored, so no probability is asserted).
The 2-bit kind has four values but the uniform draw is over three, not four: kind==3 has no legal completion, so it never gets probability mass. The answer is 1/3, not 1/4. Solve-before also never creates or removes len values: kind==0 still forces len==0.
How would you make kind exactly 1/3 each without solve-before? Model answer: choose kind outside the solver (`kind = $urandom_range(0,2); kind.rand_mode(0);`) and let randomize() pick len under the same if/else. Equalizing the branch cardinalities (1, 2, 8 tuples) is not possible without changing the legal set; `kind dist {0:=1,1:=1,2:=1}` works under the marginal reading but is tool-dependent.
By tuple counting there are eleven legal tuples: one for kind zero, two for kind one and eight for kind two, so without solve-before the probability that kind is two is eight elevenths. With solve kind before len, kind is chosen uniformly over the values that have a legal completion, which are zero, one and two, so it is exactly one third. The trap is answering one quarter because kind has two bits; kind three has no legal completion. Next I would confirm the legal set is still eleven tuples, since solve-before never changes it.