Difficulty: Hard · Puzzle 5 of 6 · Topic: Constraint Solving Order Puzzles
Enable exactly one of c_v1 / c_v2 at a time, with c_ord always on. How many (a,b) solutions does each variant have, and why do the counts differ so much?
class wrap_sum;
rand bit [7:0] a, b;
// Variant 1: sum compared with an 8-bit literal
constraint c_v1 { a + b > 8'd200; }
// Variant 2: sum compared with an unsized (32-bit) literal
constraint c_v2 { a + b > 200; }
constraint c_ord { a < b; }
endclassThe operands of a relational operator are sized to the widest operand on either side, and the addition happens at that width.
1) In c_v1 every operand is 8 bits wide (a, b and 8'd200), so a + b is evaluated in 8 bits and wraps modulo 256. The constraint means ((a+b) mod 256) in 201..255.
2) In c_v2 the literal 200 is a 32-bit int, so a and b are extended to 32 bits first and the sum does not wrap: a + b >= 201 (a+b can reach 510).
3) Without c_ord: c_v1 has 55 sums * 256 pairs each = 14080 solutions; c_v2 has 65536 - 20301 (pairs with a+b<=200) = 45235.
4) c_ord (a<b) keeps the pairs with a!=b and a<b. c_v2: (45235 - 155 diagonal pairs)/2 = 22540. c_v1: the diagonal has 54 pairs, (14080 - 54)/2 = 7013.
5) Concrete pairs: (a=250,b=10) has true sum 260 but wrapped sum 4, so it is illegal in c_v1 and legal in c_v2; (a=100,b=101) has sum 201 and is legal in both.Answer: With c_ord: c_v1 has 7013 solutions, c_v2 has 22540 (without c_ord: 14080 vs 45235). The 8-bit literal makes the sum wrap modulo 256; the unsized literal widens the operands to 32 bits.
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). Evaluates both expressions over all 65536 (a,b) pairs, with the 8-bit wrap for the 8'd200 literal and no wrap for the unsized literal. Verilator 5.048: the same width rule executed on the exact expressions (exhaustive loops), plus 300 real randomize() calls with c_v1 on all satisfy the wrapped sum and a<b.
Reading `a + b > 8'd200` as 'the real sum exceeds 200' is the bug: with an 8-bit literal the whole expression is 8 bits and the sum wraps, so a=250, b=10 (true sum 260, wrapped 4) is illegal, while a=100, b=101 (201) is legal. Counts verified by executing both expressions over all 65536 pairs in Verilator 5.048 (14080 and 45235).
How do you keep bit [7:0] a, b but make the check use the true (unwrapped) sum? Model answer: widen an operand: `{1'b0, a} + b > 8'd200` or `int'(a) + b > 200`. Then the expression is evaluated in 9 or 32 bits and the count is 45235 without c_ord (22540 with a<b). The same context-width rule applies to any constraint with +, - or * on narrow rand variables.
In c_v1 every operand is eight bits wide, so a plus b is evaluated in eight bits and wraps modulo 256, and with a less than b that leaves 7013 solutions. In c_v2 the literal 200 is a 32-bit int, so the operands widen first, the sum does not wrap, and there are 22540 solutions. The trap is reading it as the true sum exceeding 200: a 250 and b 10 has a true sum of 260 but a wrapped sum of 4, so it is illegal in c_v1. Next I would widen an operand, for example int cast of a plus b, if I want the true sum.