Difficulty: Easy · Puzzle 1 of 6 · Topic: solve...before Bias Puzzles
For this class, compare no-solve-before vs solve a before b. What is the legal set, and what are the exact values of P(a==0) in each variant?
class sb_puzzle;
rand bit a;
rand bit [3:0] b;
constraint c_rel { (a == 0) -> (b == 0); }
// Variant 1: no solve-before
// Variant 2: solve a before b;
endclassCount legal tuples first. Then apply the LRM rule: the early variable is uniform over the values that admit a legal completion.
1) Legal tuples: (a=0,b=0) is 1 tuple; (a=1,b=0..15) is 16 tuples; total=17.
2) Legal set is identical with or without solve-before.
3) Variant 1 (no ordering): every tuple is equally likely, so P(a=0)=1/17.
4) Variant 2: per IEEE 1800 18.5.10, a is chosen first, uniformly over the values that have a legal completion. Both a=0 and a=1 do, so P(a=0)=1/2; then b is chosen within the branch (b=0 forced after a=0, uniform over 16 values after a=1).Answer: 17 legal tuples either way. P(a==0)=1/17 without solve-before and exactly 1/2 with `solve a before b`.
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). Same 17 tuples either way; solve a before b applies the 18.5.10 rule (a uniform over {0,1}). Verilator 5.048 legality only: the solve-before form compiles and never produces a tuple outside the 17 legal ones (it ignores the ordering, so no probability is asserted).
Not solver luck and not 'near' 50/50: the LRM defines the result, so it is exactly 1/2. But solve-before is only a distribution rule, never a legality constraint: the 17 tuples are the same in both variants. Simulators may not implement it faithfully (Verilator 5.048 ignores the ordering), so you cannot 'run it and see' on every tool.
How can you force exact 50/50 on a without relying on solve-before? Model answer: take the choice out of the solver. Pick a procedurally with `a = $urandom_range(0,1); a.rand_mode(0);` (for example in pre_randomize) and randomize b with the same implication; a is then exactly 50/50 and b still obeys (a==0)->(b==0). `a dist {0:=1, 1:=1}` also works under the marginal reading but is tool-dependent.
There are seventeen legal tuples either way: a zero with b zero, and a one with any of sixteen b values. Without solve-before, every tuple is equally likely, so the probability that a is zero is one in seventeen. With solve a before b, a is chosen first, uniformly over values that have a legal completion, so it is exactly one half. The trap is thinking solve-before changes legality or is only approximate; it only changes the distribution, and some simulators ignore it. Next I would check my tool, or pick a procedurally and freeze it with rand_mode if I need a guarantee.