Difficulty: Medium · Puzzle 1 of 6 · Topic: Distribution Puzzles (`dist`, `:=` vs `:/`)
Activate one constraint at a time. Compute per-value probabilities for Case A, Case B, and c_trap.
class dist_puzzle;
rand int unsigned x;
// Case A
constraint c_a {
x dist { [0:3] := 8, [4:7] := 8 };
}
// Case B
constraint c_b {
x dist { [0:3] :/ 8, [4:7] :/ 8 };
}
// Trap variant
constraint c_trap {
x dist { [0:1] := 10, [2:7] :/ 10 };
}
endclassConvert ranges to per-value weights before normalizing.
1) Case A (:=): each value in 0..3 gets weight 8, each value in 4..7 gets weight 8 -> uniform 0..7.
2) Case B (:/): each range gets total weight 8 split over 4 values -> each value weight 2 -> again uniform 0..7.
3) Trap: values 0 and 1 each weight 10; values 2..7 each weight 10/6.
4) Trap total weight = 10+10+6*(10/6)=30.
5) Trap probabilities: P(0)=P(1)=10/30=1/3, and P(any of 2..7)= (10/6)/30 = 1/18.Answer: Case A and B are both uniform (each value 1/8), while in c_trap values 0 and 1 are each 1/3 and each of 2..7 is 1/18.
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). Expands every dist clause into per-value weights (:= per value, :/ split over the range) and normalizes. Verilator 5.048 legality only: all three dist constraints solve and stay in 0..7. No frequency is asserted, because Verilator only approximates dist.
A and B look different (weights 8 vs 2 per value) but are identical because both ranges have the same size (4). The operators only differ when range sizes differ; c_trap is where that bites: 2 values at weight 10 each vs one 10-weight shared by 6 values. (Verilator only approximates dist: its c_trap run gave P(0)~0.46 against the exact 1/3, so never use a simulator run to check this arithmetic.)
What single operator swap makes c_trap uniform? Model answer: change `[2:7] :/ 10` to `[2:7] := 10`. Then all eight values carry weight 10 (total 80) and each has probability exactly 1/8. The swap that goes the other way, `[0:1] :/ 10`, would give 0 and 1 weight 5 each and is not uniform either (5,5 and six values at 10/6).
Case A gives every value in zero to seven a weight of eight, and case B gives each range a total of eight split over four values, so both are uniform at one eighth each. In the trap variant, values zero and one carry weight ten each, while the ten for two to seven is shared by six values, so zero and one are a third each and each of two to seven is one eighteenth. The trap is thinking := and :/ differ even when the ranges are the same size; they only differ when range sizes differ. Next I would make the trap uniform by switching to := for the second range.