Distribution Control & Variable Ordering

What solve-before actually does

solve a before b; splits one joint solve into stages . Stage 1 solves a considering only whether each candidate value of a admits at least one legal completion of the remaining variables — every viable value of a is equally likely regardless of how many completions it has . Stage 2 then solves b (and the rest) with a frozen. Two facts to internalize: the solution set never changes (a value of a with zero completions is still excluded), and only the probability weighting moves — from per-tuple uniform to per-stage uniform.

SOLVE-BEFORE = STAGED SOLVING

  constraint:  x inside {[0:3]};  (x != 0) -> (y == 0);
               y inside {[0:7]};

  legal tuples: x=0: (0,0)(0,1)...(0,7)   = 8 tuples
                x=1: (1,0)                = 1 tuple
                x=2: (2,0)                = 1 tuple
                x=3: (3,0)                = 1 tuple   total 11

  DEFAULT (uniform tuples)         solve x before y
  -------------------------        ---------------------------
  P(x=0) = 8/11  <- dominates      stage1: x in {0,1,2,3} all
  P(x=1) = 1/11                            viable -> 1/4 each
  P(x=2) = 1/11                    stage2: x=0 -> y uniform 0..7
  P(x=3) = 1/11                            x!=0 -> y=0
                                   P(x=0) = 1/4   <- flattened

  +--------------------------------------------------+
  | Ordering rescues variables whose values admit    |
  | FEW completions from being starved by uniform-   |
  | tuple weighting. Legality is untouched.          |
  +--------------------------------------------------+

This is the practical reason verification code uses solve...before: a control field (mode, opcode, enable) whose "interesting" values admit few data completions would otherwise almost never be chosen.

Worked example: enable bit starvation

class dma_cfg;
  rand bit        en;
  rand bit [15:0] len;
  constraint c_len {
    (en == 0) -> (len == 0);        // disabled => len forced to 0
    (en == 1) -> (len inside {[1:1024]});
  }
  // tuple counts: en=0 -> 1 tuple; en=1 -> 1024 tuples
  // DEFAULT:            P(en=0) = 1/1025  ~ 0.1%  (starved!)
  constraint c_ord { solve en before len; }
  // WITH ordering:      P(en=0) = 1/2  — both en values viable
endclass

Without ordering, the disabled case appears roughly once per thousand randomizations — a coverage hole that looks like bad luck. With solve en before len, en is a fair coin and len follows. The alternative fix is dist on en — and the two compose: dist weights apply within the stage that variable is solved in, so solve en before len; plus en dist {0 := 1, 1 := 9}; gives a 10%/90% split with len still conditioned correctly.

Multi-stage chains

class layered;
  rand bit [1:0]  mode;
  rand bit [7:0]  burst;
  rand bit [31:0] addr;
  constraint c_rel {
    (mode == 0) -> (burst == 1);
    (mode != 0) -> (burst inside {[2:64]});
    addr % burst == 0;             // alignment follows burst
  }
  // chain: mode staged first, then burst, then addr
  constraint c_ord {
    solve mode  before burst;
    solve burst before addr;
  }
endclass
// Stages:  pick mode (viable values uniform)
//      ->  pick burst given mode
//      ->  pick addr given burst (alignment)
// Ordering forms a DAG: cycles like "solve a before b" plus
// "solve b before a" are illegal and rejected at compile time.

When ordering goes wrong

Three failure patterns recur. First, circular ordering — the solve-before graph must be acyclic; a cycle is a compile-time error. Second, ordering as a bug-hider : solve-before never repairs an unsatisfiable set, but by changing which values get picked it can make failures intermittent instead of constant — the worst kind of bug. Third, over-ordering : chaining solve-before through many variables collapses the joint solve into near-sequential picking, which both slows some solvers and quietly skews distributions you never meant to touch.

class subtle;
  rand bit [3:0] a, b;
  constraint c   { a + b == 20; }       // satisfiable: a,b in [5:15]
  constraint ord { solve a before b; }
endclass
// Stage 1 must pick a ONLY among values with a completion:
// a in [5:15] (since b <= 15 forces a >= 5). A CONFORMING solver
// gets this right — but it must effectively peek at b's range.
// Lesson: stage-1 "viability" still requires global reasoning;
// ordering does not make stage 1 cheap, just differently weighted.

That example also explains a performance subtlety: solve-before does not necessarily make solving faster — stage 1 still has to prove each candidate value viable against everything downstream. Use ordering to fix distributions , not as a performance lever.

Interview angle

What interviewers probe

• "What does solve a before b change?" — expected: probability weighting only; the legal set is identical; a's viable values become equally likely regardless of completion counts.

• "Why would you use it?" — expected: rescue control fields (enable/mode) starved by uniform-tuple weighting when one value admits few completions. Quote the 1/1025 vs 1/2 enable example.

• "Can solve-before fix a randomize() failure?" — expected: never; empty set stays empty. If ordering 'fixed' it, the set was never empty — distribution changed, not legality.

• "dist vs solve-before?" — expected: dist sets explicit weights on one variable's values; solve-before changes staging so viable values weight equally; they compose.

• "Is circular solve-before legal?" — expected: no — ordering must form a DAG, tools reject cycles.

The crispest interview formulation: "solve-before moves probability mass, never solution-set membership." Then back it with the staged 1/2-1/4-1/4 table from the bidirectional-solving lesson.

Key takeaways

• solve-before stages the solve: ordered variable picked uniformly among VIABLE values, rest solved given it.

• It re-weights probability only — the solution set is bit-for-bit unchanged, and contradictions stay contradictions.

• Use it to rescue control fields starved by uniform-tuple weighting (enable bits, modes, opcodes).

• dist composes with ordering: weights apply within the variable's stage.

• Ordering must be acyclic, and stage-1 viability still requires global reasoning — it is not a speed knob.

Common pitfalls

• Expecting solve-before to change WHICH values are legal — it cannot; it only re-weights.

• Leaving control fields unordered next to large dependent data fields — interesting modes starve at ~1/N rates.

• Building solve-before cycles across constraint blocks — compile error, sometimes discovered late in integration.

• Chaining ordering through every variable 'for determinism' — skews distributions and may slow solving.

• Using ordering to mask an over-constrained set — failures turn intermittent and much harder to root-cause.