Finding Contradictions

The core idea: shrink the UNSAT set

A contradiction is a property of a set of constraints, not of one constraint. Somewhere inside the full active set there is a minimal subset — often just two or three constraints plus a state value — that cannot be satisfied together. Your job is to shrink the full set down to that core. The fastest manual technique is binary search by disabling constraint blocks with constraint_mode(0), which turns named constraint blocks off without recompiling. Disable half the blocks; if randomize now succeeds, the contradiction involves the disabled half; re-enable and recurse. Each iteration halves the suspect set, so even a class with 20 constraint blocks takes about five experiments.

class axi_txn;
  rand bit [31:0] addr;
  rand bit [3:0]  len;      // beats - 1
  rand bit [2:0]  size;     // bytes per beat = 2**size
  rand bit        is_wrap;

  constraint align_c { addr % (1 << size) == 0; }
  constraint size_c  { size <= 3'd2; }                  // up to 4 bytes/beat
  constraint wrap_c  { is_wrap -> len inside {1,3,7,15}; }
  constraint page_c  { addr[11:0] + ((len+1) << size) <= 4096; }
  constraint hot_c   { addr inside {[32'h1000:32'h1010]}; }
endclass

module dbg;
  initial begin
    axi_txn t = new();
    if (!t.randomize()) begin
      // ---- binary search session ----
      t.align_c.constraint_mode(0);
      t.size_c.constraint_mode(0);
      if (t.randomize()) $display("conflict involves align_c/size_c half");
      // restore, then split the guilty half further
      t.align_c.constraint_mode(1);
      t.size_c.constraint_mode(1);
      t.hot_c.constraint_mode(0);
      if (t.randomize()) $display("hot_c participates in the conflict");
    end
  end
endmodule

Two rules make this efficient. First, give every constraint a name — anonymous constraints cannot be toggled. Second, after each experiment restore everything with constraint_mode(1) before the next, so you are always testing exactly one hypothesis. The end state is the smallest set of enabled blocks that still fails: that is your contradiction core.

randomize(null): the consistency check

Calling obj.randomize(null) treats every rand variable as a state variable — nothing is randomized; the solver merely checks whether the constraints are satisfied by the object's current values . It returns 1 if the current state is consistent, 0 if not. This is a precision instrument with two main uses: verifying that a hand-loaded or replayed object satisfies the constraint set, and testing whether a specific suspect value combination is legal without letting the solver wander.

axi_txn t = new();

// Hypothesis: is addr=0x1003 with size=2 legal? Plant values, then check.
t.addr    = 32'h1003;
t.size    = 3'd2;
t.len     = 4'd0;
t.is_wrap = 1'b0;
if (!t.randomize(null))
  $display("0x1003/size=2 violates a constraint (align_c: 0x1003 %% 4 != 0)");

// Also useful after replaying a logged transaction:
// load fields from the log, then prove the repro object is constraint-legal.
if (!logged_txn.randomize(null))
  $display("logged txn does not satisfy current constraints - class changed?");

The second use case catches a subtle regression bug: the transaction class evolved since the log was written, so a replayed object that used to be legal now violates a new constraint. randomize(null) flags it immediately instead of letting the replay produce confusing downstream behavior. A related tool is randomize() with specific variables listed as arguments — e.g. t.randomize(len) randomizes only len, holding all other rand fields at their current values as constants, which is another way to corner a suspect variable.

Vendor solver-debug switches

Every major simulator can report which constraints participate in an UNSAT core, and you should name this capability in interviews even though exact switches vary by tool and version. Conceptually they all do the same thing: on a randomize failure, dump the set of constraint expressions and state-variable values that the solver proved mutually inconsistent, with file/line references.

• VCS — constraint-solver debug runtime options produce a failure analysis listing the conflicting constraint expressions and the state values involved (look for the solver diagnostics section in the simulation log).

• Questa — solveflow/debug analysis modes report the inconsistent constraint subset and can generate a standalone testcase that reproduces just the failing solver call.

• Xcelium — randomization debug options identify the UNSAT core and print participating constraints with their source locations.

• All tools: the dump is most readable on a minimal repro — on a full UVM environment the constraint set includes dozens of inherited and nested blocks, so shrink first, then dump.

Treat tool output as a hint, not gospel: an UNSAT core is not unique, and the tool may report a different minimal subset than the one that is conceptually wrong. The binary-search result plus the tool dump together usually triangulate the true culprit in minutes.

Building a minimal repro

When a contradiction resists quick isolation — or you need to file a tool bug or ask a colleague — build a minimal repro: a standalone module with a copy of the class stripped to the failing constraint core, state variables hard-coded to the failing values, and a single checked randomize call. The discipline of constructing it usually reveals the bug before you finish.

// minimal_repro.sv - 20 lines, no UVM, runs in any simulator
class repro;
  rand bit [31:0] addr;
  rand bit [2:0]  size;
  constraint align_c { addr % (1 << size) == 0; }
  constraint hot_c   { addr inside {[32'h1001:32'h1003]}; }
  constraint size_c  { size >= 3'd2; }
endclass

module top;
  initial begin
    repro r = new();
    // UNSAT: size>=2 needs addr % 4 == 0, but [0x1001:0x1003]
    // contains no multiple of 4. Three constraints, zero solutions.
    if (!r.randomize()) $display("REPRO: UNSAT as expected");
    else                $display("solved: addr=%h size=%0d", r.addr, r.size);
  end
endmodule

The classic walked-through example: inline vs class constraint

class eth_frame;
  rand bit [13:0] length;
  constraint legal_c { length inside {[64:1518]}; }
endclass

eth_frame f = new();

// Test writer wants a jumbo frame and writes:
if (!f.randomize() with { length == 9000; })
  $display("FAILS every time");

// WHY: inline 'with' is ANDed with legal_c:
//   (length inside [64:1518]) && (length == 9000)  -> empty set
// FIX options, in order of preference:
//   1. Make the class constraint soft where policy allows:
//        constraint legal_c { soft length inside {[64:1518]}; }
//      now the hard inline length==9000 wins, soft is discarded.
//   2. Disable for this call:
//        f.legal_c.constraint_mode(0);
//        assert(f.randomize() with { length == 9000; });
//        f.legal_c.constraint_mode(1);
//   3. Subclass eth_frame with a jumbo constraint (test-intent layering).

This exact scenario — inline constraint silently conflicting with a base-class constraint the test writer forgot about — is the single most common real-world contradiction, and the most common interview probe. The deep point: the solver gives both constraint sources equal authority ; there is no precedence between class and inline constraints. Only soft constraints create a priority relationship, and a soft constraint is dropped entirely (not relaxed gradually) when it conflicts with any hard constraint.

Interview angle

The expected answer to “randomize returns 0 — how do you find the conflict?” is a crisp sequence: check the return value is actually being looked at; reproduce with a fixed seed; binary-search with constraint_mode(0) over named blocks; use randomize(null) to test suspect value combinations; turn on the vendor solver-debug dump for the UNSAT core; and reduce to a 20-line standalone repro. Bonus points for stating that inline with constraints are ANDed (not overriding), that state variables can make an otherwise-fine constraint set UNSAT, and that soft constraints are discarded wholesale on conflict.

Key takeaways

• Binary search with constraint_mode(0) halves the suspect set each iteration — name every constraint block.

• randomize(null) checks current values against constraints without randomizing — perfect for hypothesis testing and replay validation.

• Vendor solver-debug dumps identify the UNSAT core, but run them on a minimal repro, not the full env.

• Inline with constraints AND with class constraints — the classic contradiction is forgetting a base-class range.

• A 20-line minimal repro is both a debugging tool and the artifact you hand to colleagues or vendors.

Common pitfalls

• Anonymous constraint blocks — cannot be disabled individually, so binary search is impossible.

• Forgetting to re-enable blocks after an experiment — later tests run under-constrained and results lie.

• Expecting inline with to override class constraints — it conjoins; only soft creates priority.

• Reading the solver dump on a full UVM object — dozens of inherited constraints bury the core.

• Fixing a contradiction by deleting the legality constraint instead of layering test intent properly.