Difficulty: Easy · Puzzle 6 of 6 · Topic: Distribution Puzzles (`dist`, `:=` vs `:/`)
Given this dist, what is P(x==0) and P(x==4)?
class zero_weight;
rand int unsigned x;
constraint c {
x dist { 0 := 0, [1:3] := 1, [4:5] :/ 2 };
}
endclassTranslate [4:5] :/ 2 into per-value weights first.
1) x=0 has weight 0, so it is effectively excluded.
2) x=1,2,3 each get weight 1.
3) [4:5] :/ 2 gives each of 4 and 5 weight 1.
4) Total non-zero weight=5.
5) P(x==0)=0 and P(x==4)=1/5.Answer: x==0 is impossible (0%), and P(x==4)=20%.
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). Zero weight removes a value from the pool; [4:5] :/ 2 gives 4 and 5 weight 1 each. Verilator 5.048: in 400 calls x==0 never appears and x stays in 1..5 (legality of the zero weight, not a frequency).
Zero weight is 'never selected', not 'rare', and it does not matter that 0 is listed in the dist. Verified on Verilator 5.048: x==0 never appeared in 400 runs. The [4:5] :/ 2 clause gives 4 and 5 weight 1 each, so five equal-weight values remain.
Would adding x inside {[0:5]} change these probabilities? Model answer: no. All five weighted values already lie in 0..5, so the hard constraint removes nothing, and 0 remains impossible because its dist weight is 0 (P(0)=0, P(4)=1/5). Adding x inside {[1:3]} instead would renormalize to 1/3 each and P(4)=0.
A weight of zero means never chosen, so the probability that x is zero is exactly zero. Values one, two and three get weight one each, and the range four to five with :/ two gives four and five weight one each, so five equal values remain and the probability that x is four is one fifth. The trap is thinking zero is just rare because it is listed in the dist. Next I would check whether a hard constraint clips some of the remaining values, which would renormalize the rest.