Difficulty: Medium · Puzzle 1 of 6 · Topic: Constraint Solving Order Puzzles
Compare req_a vs req_b. Assuming unbiased tuple selection from legal solutions, compute P(kind==1) in each class and explain why they differ.
class req_a;
rand bit [1:0] kind; // 0:READ, 1:WRITE
rand bit [3:0] burst;
constraint c_kind { kind inside {0,1}; }
constraint c_legal { burst inside {[1:8]}; }
constraint c_link { (kind == 1) -> (burst inside {[1:3]}); }
endclass
class req_b;
rand bit [1:0] kind;
rand bit [3:0] burst;
constraint c_kind { kind inside {0,1}; }
constraint c_legal { burst inside {[1:8]}; }
constraint c_link {
if (kind == 1) burst inside {[1:3]};
else burst inside {[4:8]};
}
endclassCount satisfying (kind,burst) tuples per class before discussing solver heuristics.
1) req_a legal tuples: kind=0 allows burst 1..8 (8 tuples), kind=1 allows 1..3 (3 tuples), total=11.
2) req_b legal tuples: kind=1 allows 3 tuples, kind=0 allows 5 tuples (4..8), total=8.
3) Tuple-weighted probabilities are P_a(kind=1)=3/11 and P_b(kind=1)=3/8.
4) Both snippets are declarative; the difference comes from legal-space partitioning, not runtime execution order. The implication leaves kind==0 free over all of 1..8, the if/else cuts it to 4..8.Answer: P(kind==1) is 3/11 (~27.27%) for req_a and 3/8 (37.5%) for req_b under tuple counting.
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). Counts the legal (kind,burst) tuples of both classes and applies the 18.5.10 rule for the follow-up.
The tempting story is 'the implication is checked after burst is picked'. In req_a, kind==0 simply does not restrict burst, so the whole 1..8 range (8 tuples) stays in the legal set; the else branch of req_b removes 1..3 from kind==0 and that is the entire difference (11 vs 8 tuples).
How would you modify req_b so kind is exactly 50/50 without changing legal burst values? Model answer: add `solve kind before burst;`. The legal set stays at 8 tuples, but per LRM 18.5.10 kind (feasible values {0,1}) is then chosen first and uniformly, so P(kind==1)=1/2, with burst uniform inside the chosen branch (3 or 5 values). Under the common 'dist is the marginal' reading, `kind dist {0:=1, 1:=1}` does the same, but that is tool-dependent; solve-before is the LRM-defined way.
I would count the legal kind and burst pairs. In req_a, kind zero leaves burst free over one to eight, so that is eight pairs plus three for kind one, eleven in total, and the chance of kind one is three over eleven. In req_b the else branch cuts kind zero to burst four to eight, so it is five plus three, eight pairs, and the chance is three over eight. The trap is thinking the implication is checked after burst is picked; it is a relation, and kind zero simply does not restrict burst. Next I would add solve kind before burst to make kind exactly fifty-fifty.