Difficulty: Easy · Puzzle 3 of 6 · Topic: solve...before Bias Puzzles
What is P(a==1) by tuple counting, and what exact value does solve b before a give?
class sb_reverse;
rand bit a;
rand bit [1:0] b;
constraint c_rel { (a == 0) -> (b == 0); }
// Variant: solve b before a;
endclassWith b first, b is uniform over 4 values; only b==0 leaves a free.
1) Legal tuples are (a=0,b=0) plus (a=1,b=0..3) -> total 5 tuples.
2) Tuple baseline gives P(a==1)=4/5.
3) With solve b before a, b is chosen first, uniformly over its 4 feasible values (all have a legal completion).
4) For b!=0 (probability 3/4), a must be 1; for b=0 (probability 1/4) both a values are legal, 1/2 each.
5) P(a==1) = 3/4 + (1/4)*(1/2) = 7/8. The 5 legal tuples are unchanged.Answer: Baseline P(a==1)=4/5; with `solve b before a` it is exactly 7/8 (the legal set stays at 5 tuples).
Checked by running a model of the rule in a Python model. Exact enumeration of the constraint set per the LRM (the LRM defines the distribution; simulator solvers need not be uniform). Same 5 tuples; the three orderings give 4/5, 7/8 and 1/2.
Reversing the order matters: the same legal set gives 4/5 with no ordering, 7/8 with b first, and 1/2 with `solve a before b`. Verilator 5.048 ignores solve-before and returned P(a==1)=1.0 for this class in a 300-sample run, so the exact fraction comes from the LRM rule, not from a simulation.
Which explicit dist on a would neutralize this order-induced skew? Model answer: `a dist {0 := 1, 1 := 1};`. Only if you also remove `solve b before a`: with it still in the class, b is chosen uniformly first and a is forced to 1 whenever b!=0, so P(a==1) stays 7/8 whatever weights a has (dist can only weight values that remain feasible). Without the solve-before, `a dist {0:=1, 1:=1}` gives 1/2 under the marginal reading (tool-dependent). The LRM-defined way is to swap the order to `solve a before b;`, which gives 1/2 exactly.
There are five legal tuples, a zero with b zero and a one with b zero to three, so by counting the probability that a is one is four fifths. With solve b before a, b is chosen first, uniformly over its four feasible values: for b not zero, a must be one, and for b zero it is half each, so the answer is three quarters plus one eighth, seven eighths. The trap is that the order matters: the same legal set gives four fifths, seven eighths, or one half with solve a before b. Next I would put the solve-before on the variable whose balance I actually want.