Difficulty: Hard · Puzzle 6 of 6 · Topic: solve...before Bias Puzzles
Count the legal (a,b,c) tuples and compute P(a==0), P(b==0) and P(c==0) with no ordering. Then compute the same three probabilities with `solve a before b; solve b before c;`. What happens if you also add `solve c before a;`?
class sb_chain;
rand bit a;
rand bit [1:0] b;
rand bit [1:0] c;
constraint c_ab { (a == 0) -> (b == 0); }
constraint c_bc { (b == 0) -> (c == 0); }
// Variant 1: no ordering
// Variant 2: solve a before b; solve b before c;
endclassEnumerate tuples first. For the chain, apply the LRM rule at each step: the next variable is uniform over its values that still have a legal completion given the earlier ones.
1) Legal tuples: (a=0,b=0,c=0) is 1; (a=1,b=0,c=0) is 1; (a=1,b=1..3,c=0..3) is 3*4=12. Total 14.
2) Variant 1 (tuple counting): P(a==0)=1/14, P(b==0)=2/14=1/7, P(c==0)=5/14 (tuples with c=0: 1+1+3).
3) Variant 2: a is chosen first over its feasible values {0,1}: P(a==0)=1/2. For a=0, b=0 is forced; for a=1, b is uniform over {0,1,2,3} (all have a completion).
4) P(b==0)=1/2*1 + 1/2*1/4 = 5/8. Then c: forced to 0 when b==0, uniform over {0..3} otherwise.
5) P(c==0)=5/8*1 + 3/8*1/4 = 23/32.
6) Adding `solve c before a` creates the cycle a->b->c->a. The LRM (18.5.10) requires the ordering to be acyclic, so this is an error, not a different distribution.Answer: 14 legal tuples. No ordering: P(a==0)=1/14, P(b==0)=1/7, P(c==0)=5/14. With the chain `solve a before b; solve b before c;`: P(a==0)=1/2, P(b==0)=5/8, P(c==0)=23/32. Adding `solve c before a;` makes the ordering circular, which is an error.
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). Applies the 18.5.10 rule step by step along the chain and detects the a->b->c->a cycle that the LRM rejects as an error.
Each step renormalizes over the values that still have a legal completion, so the bias does not just flip once: a is uniform (1/2), b stays biased toward 0 (5/8) because a=0 forces it, and c inherits that bias (23/32). The legal set is the same 14 tuples in every variant, and a cyclic solve-before is rejected rather than interpreted. Fractions re-derived by exact enumeration in Python; Verilator 5.048 ignores solve-before, so do not run it to check.
What does the reverse chain `solve c before b; solve b before a;` give for P(a==0)? Model answer: c is uniform over {0,1,2,3} (each has a completion), so P(c==0)=1/4. Given c==0, b is uniform over {0,1,2,3}, so P(b==0)=1/16. Only b==0 leaves a free, then 1/2 each, so P(a==0)=1/32. The order you name decides the bias, while the 14 legal tuples never change.
There are fourteen legal tuples, and they stay the same in every variant. With no ordering the probabilities that a, b and c are zero are one fourteenth, one seventh and five fourteenths. With the chain a before b before c, a is one half, b is five eighths and c is twenty-three thirty-seconds, because the bias carries down the chain. The trap is adding solve c before a: that makes the ordering circular, and the LRM treats it as an error, not a different distribution. Next I would check the order is acyclic.