How the Constraint Solver Works

Overview

Everything confusing about SystemVerilog randomization — implication "working backwards", solve...before changing distributions without changing legality, randomize calls that suddenly take seconds — becomes predictable once you hold the right mental model: constraints define a set of legal value assignments, and the solver picks one member of that set . Constraints are declarative equations, not procedural assignments. There is no "first this variable, then that one" unless you explicitly impose ordering.

This topic is the differentiator in senior interviews . Anyone can write inside {[1:10]}; the questions that separate candidates are "what is the probability of y==1 given (x==0) -> (y==0)?", "why does solve-before change distribution but not the solution set?", and "what does the LRM actually guarantee about reproducibility?". Every sub-lesson here targets one of those question families.

Sub-topics

1. The Solution-Space Mental Model — constraints as a set of legal tuples, uniform choice, diagrams for 2-variable examples.

2. Bidirectional Solving — implications constrain both sides; the classic (x==0)->(y==0) joint-distribution table.

3. randc Internals & Limits — permutation cycling, per-variable independence, width limits, ordering vs rand.

4. Distribution Control & Variable Ordering — how solve-before stages the solve and re-weights probability.

5. Solver Performance — what makes constraints expensive and how to restructure slow randomize calls.

6. Solver FAQ: Determinism & Vendor Differences — seed stability rules, LRM guarantees vs implementation freedom.

SOLVER DEEP-DIVE TOPIC MAP

  constraint blocks (declarative equations)
        |
        v
  +------------------------------------------+
  |          SOLUTION SPACE                  |
  |  set of all (var1, var2, ...) tuples     |
  |  satisfying EVERY active constraint      |
  +------------------------------------------+
        |                |               |
        v                v               v
  uniform pick     solve-before     randc cycling
  (default LRM     partitions the   (permutation per
   intent)         space into       variable, solved
        |          stages, re-      BEFORE rand vars)
        |          weights probs
        v
  one assignment written to variables
        |
        v
  same seed + same tool = same sequence (stability)
  different vendors may legally differ

Key takeaways

• Constraints define a solution set; randomize() picks one member — never think in assignment order.

• Every constraint is bidirectional: an implication constrains its antecedent too.

• solve-before and randc change HOW the space is sampled (distribution), never WHICH tuples are legal.

• The LRM guarantees same-seed reproducibility within one tool, not identical values across vendors.