A contradiction is a property of a set of constraints, not of one constraint. Somewhere inside the full active set sits a minimal subset that cannot be satisfied together, and the job is to shrink the full set down to that core.
The fastest manual technique is binary search by disabling named constraint blocks. Each experiment halves the suspect set, so twenty blocks take about five tries.
class axi_txn;
rand bit [31:0] addr;
rand bit [3:0] len;
rand bit [2:0] size;
rand bit is_wrap;
constraint align_c { addr % (1 << size) == 0; }
constraint size_c { size inside {[3'd2:3'd3]}; } // planted: 4- or 8-byte beats
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'h1001:32'h1003]}; } // no multiple of 4
endclass
module top;
initial begin
axi_txn t;
bit saved_align, saved_size, saved_wrap, saved_page, saved_hot;
t = new();
if (!t.randomize()) begin
// Binary search: disable half, test, then narrow the guilty half.
saved_align = t.align_c.constraint_mode();
saved_size = t.size_c.constraint_mode();
t.align_c.constraint_mode(0);
t.size_c.constraint_mode(0);
if (t.randomize()) $display("conflict involves the align/size half");
// Restore each block to its own saved state, never to a blanket 1.
t.align_c.constraint_mode(saved_align);
t.size_c.constraint_mode(saved_size);
// Step 2: disable the other half and test again.
saved_wrap = t.wrap_c.constraint_mode();
saved_page = t.page_c.constraint_mode();
saved_hot = t.hot_c.constraint_mode();
t.wrap_c.constraint_mode(0);
t.page_c.constraint_mode(0);
t.hot_c.constraint_mode(0);
if (t.randomize()) $display("the other half also takes part: the core spans both");
t.wrap_c.constraint_mode(saved_wrap);
t.page_c.constraint_mode(saved_page);
t.hot_c.constraint_mode(saved_hot);
// Next: split each half again. The core is align_c, size_c, hot_c.
end
else $fatal(1, "FAIL: the planted conflict solved");
$display("PASS: the planted conflict failed and both halves took part");
$finish;
end
endmodule%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t43.sv:7: Unsatisfied constraint: 'constraint align_c { addr % (1 << size) == 0; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t43.sv:8: Unsatisfied constraint: 'constraint size_c { size inside {[3'd2:3'd3]}; } '
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t43.sv:11: Unsatisfied constraint: 'constraint hot_c { addr inside {[32'h1001:32'h1003]}; } '
conflict involves the align/size half
the other half also takes part: the core spans both
PASS: the planted conflict failed and both halves took partTwo rules make this efficient. Every constraint needs a name, because anonymous blocks cannot be toggled. And each experiment must restore per-block saved state, since a blanket re-enable would turn on blocks the test had deliberately left off.
Halving by hand works, but a short loop does it better. The deletion filter switches each named block off in turn: if the rest still fails, that block is not needed for the conflict and stays off; if the rest now solves, the block is part of the core and goes back on. One pass leaves the smallest set that still fails.
hot_c (addresses 1001 to 1003) against align_c with size_c (4- or 8-byte alignment). Which blocks will the deletion filter keep?align_c, size_c and hot_c. Switching off wrap_c or page_c still fails, so they are not needed; switching off any of the other three lets the call solve.
class axi_txn;
rand bit [31:0] addr;
rand bit [3:0] len;
rand bit [2:0] size;
rand bit is_wrap;
constraint align_c { addr % (32'd1 << size) == 0; }
constraint size_c { size inside {[3'd2:3'd3]}; } // 4- or 8-byte beats
constraint wrap_c { is_wrap -> len inside {1, 3, 7, 15}; }
constraint page_c { 32'(addr[11:0]) + ((32'(len) + 1) << size) <= 4096; }
constraint hot_c { addr inside {[32'h1001:32'h1003]}; } // planted: no multiple of 4
// Switch one named block on or off by index.
function void set_block(int i, bit on);
case (i)
0: align_c.constraint_mode(on);
1: size_c.constraint_mode(on);
2: wrap_c.constraint_mode(on);
3: page_c.constraint_mode(on);
4: hot_c.constraint_mode(on);
endcase
endfunction
endclass
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:6: Unsatisfied constraint: 'constraint align_c { addr % (32'd1 << size) == 0; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:7: Unsatisfied constraint: 'constraint size_c { size inside {[3'd2:3'd3]}; } '
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:10: Unsatisfied constraint: 'constraint hot_c { addr inside {[32'h1001:32'h1003]}; } '
all five blocks on: randomize() returned 0
align_c off: randomize() returned 1 -> in the core
size_c off: randomize() returned 1 -> in the core
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:6: Unsatisfied constraint: 'constraint align_c { addr % (32'd1 << size) == 0; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:7: Unsatisfied constraint: 'constraint size_c { size inside {[3'd2:3'd3]}; } '
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:10: Unsatisfied constraint: 'constraint hot_c { addr inside {[32'h1001:32'h1003]}; } '
wrap_c off: randomize() returned 0 -> not needed
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:6: Unsatisfied constraint: 'constraint align_c { addr % (32'd1 << size) == 0; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:7: Unsatisfied constraint: 'constraint size_c { size inside {[3'd2:3'd3]}; } '
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t44.sv:10: Unsatisfied constraint: 'constraint hot_c { addr inside {[32'h1001:32'h1003]}; } '
page_c off: randomize() returned 0 -> not needed
hot_c off: randomize() returned 1 -> in the core
minimal core: align_c size_c hot_c
PASS: five solves named the minimal core align_c, size_c and hot_cRead the warnings above the result. Verilator 5.048 printed an UNSATCONSTR warning for exactly the three blocks in the core, on every failing call, and the deletion filter agreed. On this tool the warning is the solver dump: read it first, and use the filter to confirm it or when the tool says less.
The standard's check-only call is obj.randomize(null): it treats every field as fixed and only asks whether the current values satisfy the constraints. Verilator 5.048 rejects it as unsupported.
// snippet
t.addr = 32'h1003; t.size = 3'd2; // plant the suspect values
if (!t.randomize(null)) $display("0x1003 with size 2 breaks a constraint");The same question works on every tool if each field is pinned with an inline with. The call can only succeed if those exact values satisfy every active block, so its return value is the verdict.
class axi_txn;
rand bit [31:0] addr;
rand bit [2:0] size;
constraint align_c { addr % (32'd1 << size) == 0; }
constraint size_c { size inside {[3'd2:3'd3]}; }
endclass
module tb_pin_check;
axi_txn t = new();
// Check-only: pin every rand field to the suspect values. The call can only
// succeed if those exact values satisfy every active constraint.
function automatic bit legal(bit [31:0] a, bit [2:0] s);
axi_txn probe = new();
return probe.randomize() with { addr == a; size == s; };
endfunction
initial begin
bit r1, r2, r3;
r1 = legal(32'h1004, 3'd2); // 4-byte aligned, 4-byte beats
r2 = legal(32'h1003, 3'd2); // not 4-byte aligned
r3 = legal(32'h1004, 3'd3); // 8-byte beats need an 8-byte boundary
$display("addr 1004 size 2: %0d addr 1003 size 2: %0d addr 1004 size 3: %0d", r1, r2, r3);
if (!(r1 && !r2 && !r3)) $fatal(1, "FAIL: a pinned check gave the wrong verdict");
$display("PASS: pinning every field with an inline with gave the three verdicts by hand");
$finish;
end
endmodule%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t45.sv:4: Unsatisfied constraint: 'constraint align_c { addr % (32'd1 << size) == 0; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t45.sv:14: Unsatisfied constraint: 'return probe.randomize() with { addr == a; size == s; };'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t45.sv:14: Unsatisfied constraint: 'return probe.randomize() with { addr == a; size == s; };'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t45.sv:4: Unsatisfied constraint: 'constraint align_c { addr % (32'd1 << size) == 0; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t45.sv:14: Unsatisfied constraint: 'return probe.randomize() with { addr == a; size == s; };'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t45.sv:14: Unsatisfied constraint: 'return probe.randomize() with { addr == a; size == s; };'
addr 1004 size 2: 1 addr 1003 size 2: 0 addr 1004 size 3: 0
PASS: pinning every field with an inline with gave the three verdicts by handThe same trick validates a transaction read back from a log against today's constraints: build a fresh object, pin every field to the logged values, and check the return value.
The most common real-world contradiction is a test-level inline constraint silently conflicting with a forgotten base-class range. The solver gives both sources equal authority.
Fixes layer in order of preference: soften the class default where policy allows, disable the block for one call, or subclass with test intent. Never delete the legality constraint.
class eth_frame;
rand bit [13:0] length;
constraint legal_c { length inside {[64:1518]}; }
endclass
module top;
initial begin
eth_frame f = new();
// Wants a jumbo frame. Inline ANDs with legal_c, so this is empty.
if (!f.randomize() with { length == 9000; })
$display("inline length 9000 vs class range: no solution");
else $fatal(1, "FAIL: length 9000 should contradict legal_c");
$display("PASS: the inline jumbo request failed as expected");
$finish;
// Fix 1: soften the class default, then the hard inline wins.
// Fix 2: f.legal_c.constraint_mode(0) around this one call.
// Fix 3: subclass eth_frame with a jumbo constraint.
end
endmodule%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t46.sv:3: Unsatisfied constraint: 'constraint legal_c { length inside {[64:1518]}; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t46.sv:10: Unsatisfied constraint: 'if (!f.randomize() with { length == 9000; })'
inline length 9000 vs class range: no solution
PASS: the inline jumbo request failed as expectedVerilator 5.048 needs no switch: every failed call prints an UNSATCONSTR warning naming the blocks behind it, as the core-finder bench showed. Every major simulator can report the constraint subset behind an UNSAT result with file and line references. Treat the exact switches as capability pointers and look them up in the tool version at hand, since flags move between releases.
Run the dump on a minimal repro, never on the full environment. Reducing the class to its failing core usually reveals the bug before the dump finishes.
// minimal_repro: 3 constraints, 1 state value, no methodology code.
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 divisible by 4, but the hot window
// holds no multiple of 4. Three constraints, zero solutions.
if (!r.randomize()) $display("PASS: repro shows UNSAT as analyzed");
else $fatal(1, "FAIL: solved: addr=%h size=%0d", r.addr, r.size);
$finish;
end
endmodule%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t47.sv:5: Unsatisfied constraint: 'constraint align_c { addr % (1 << size) == 0; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t47.sv:6: Unsatisfied constraint: 'constraint hot_c { addr inside {[32'h1001:32'h1003]}; }'
%Warning-UNSATCONSTR: /var/folders/41/dgs80y1569b4x8pwflv_w9jr0000gn/T/rtbtb-K1WcxI/t47.sv:7: Unsatisfied constraint: 'constraint size_c { size >= 3'd2; }'
PASS: repro shows UNSAT as analyzedIt involves the disabled half. Re-enable and split that half again until the smallest failing set remains.
The full object drags in dozens of inherited and nested blocks that bury the core. The dump is most readable on the smallest failing set.
Run with Verilator 5.048 (--binary --timing) on 2026-10-18; every bench printed the PASS line shown. Verilator prints a harmless WIDTHTRUNC warning for if (!obj.randomize()), because randomize() returns an int, and an UNSATCONSTR warning when a solve fails on purpose. Icarus 13 does not support constraints.
On every failed call Verilator 5.048 printed an UNSATCONSTR warning for exactly the three core blocks, and the deletion filter agreed. randomize(null) is rejected as unsupported.