Difficulty: Hard · Puzzle 5 of 6 · Topic: solve...before Bias Puzzles
Find the legal tuples and compute P(mode==1) for three variants: no ordering, solve mode before x,y, and solve y before mode.
class sb_mode_xy;
rand bit mode;
rand bit [1:0] x;
rand bit [1:0] y;
constraint c {
(mode == 0) -> (x == 0);
(mode == 1) -> (y == 3);
x + y <= 3;
}
// Variant 1: no ordering
// Variant 2: solve mode before x, y;
// Variant 3: solve y before mode;
endclassEnumerate mode=0 and mode=1 branches separately. For variant 3 list which mode values are possible for each y.
1) mode=0 forces x=0; y can be 0..3 -> tuples (0,0,0),(0,0,1),(0,0,2),(0,0,3), 4 tuples.
2) mode=1 forces y=3 and x+y<=3, so x must be 0 -> 1 tuple (1,0,3). Total 5 tuples.
3) Variant 1: P(mode==1)=1/5.
4) Variant 2: mode is chosen first among its feasible values {0,1}: P(mode==1)=1/2.
5) Variant 3: y is chosen first, uniformly over feasible values {0,1,2,3} (1/4 each). Only y=3 allows mode=1, and there mode is 50/50 (tuples (0,0,3) and (1,0,3)). P(mode==1)=1/4 * 1/2 = 1/8.Answer: 5 legal tuples. P(mode==1) = 1/5 with no ordering, 1/2 with `solve mode before x,y`, and 1/8 with `solve y before mode`.
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). mode=1 owns a single tuple (1,0,3); the answer depends on which variable is solved first. Verilator 5.048 legality only: all results are among the 5 legal (mode,x,y) tuples; ordering variants are not run because Verilator ignores solve-before.
Which variable you put first decides the answer: ordering by mode inflates mode==1 (1 tuple) to 1/2, but ordering by y pushes it the other way to 1/8, below the tuple-count 1/5, because only one of four y values can be paired with mode==1. The cross-constraint x+y<=3 collapses the mode==1 branch to a single tuple.
What additional constraint would make both mode branches have equal tuple count, without solve-before? Model answer: add `y == 3;`. Then mode=0 has only (0,0,3) and mode=1 has only (1,0,3): 2 tuples, 1 each, so P(mode==1)=1/2 for every ordering. The price is that the legal set shrinks from 5 to 2 tuples; `solve mode before x,y` gets 1/2 without changing legality.
There are five legal tuples: mode zero forces x to zero with y anywhere in zero to three, four tuples, and mode one forces y to three and x to zero, one tuple. With no ordering the probability that mode is one is one fifth. With solve mode before x and y it is one half, and with solve y before mode it is one eighth, because only y equal to three allows mode one, and there mode is half each. The trap is that the variable you name first decides the answer, and it can push the bias below the tuple count. Next I would check the cross-constraint that collapses the branch.