What costs the most

Ordinary verification constraints solve quickly on every engine. Cost rises with a few shapes, and it multiplies: a medium constraint inside a foreach over 1000 elements is 1000 medium constraints in one problem.

A constant multiply is a shift that range reasoning handles directly. A product of two rand fields is factoring, which needs search.

Measure before fixing

A slow solve shows up as wall-clock time growing while simulated time stands still. $realtime around randomize() measures simulated time, so it reads zero and says nothing about solver cost.

Use the simulator's solver profile, which reports time per constraint block and the number of failed attempts. Retries are the most useful signal on any tool: a constraint that fails and re-solves often costs many times its nominal solve. Guessing the hot constraint by eye fails routinely.

Verilator 5.048 hands each solve to an external SMT solver (z3 in this course's setup), so a constraint-heavy bench spends most of its time in that solver. Run the same bench with a few constraint blocks switched off by constraint_mode(0) to see which block costs the time.

Rewrites that keep every result legal

Three rewrites remove most solver cost. Each one must keep the set of legal results, and a bench proves that before the rewrite is trusted.

The bench checks the first two rewrites against the original rule: a pages and stride pair whose product must fit an 8 KiB buffer. The product form, the table form and a precomputed base address all solve 300 times, every result is checked, and three planted bad pairs prove the checker can fail.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

localparam int LIMIT = 8192;                  // buffer bytes: pages * stride must fit

class product_pair;                           // rand times rand: a hard shape for solvers
  rand bit [7:0]  pages, stride;
  rand bit [15:0] total;
  constraint c {
    pages != 0;
    stride inside {1, 2, 4, 8, 16, 32, 64, 128};
    total == 16'(pages) * stride;             // 16-bit multiply: no wrap
    total <= LIMIT;
  }
endclass

class table_pair;                             // pick a row of legal pairs instead
  rand bit [2:0] pick;
  bit [7:0] pages_tbl [8] = '{10, 20, 30, 40, 50, 60, 70, 80};
  bit [7:0] stride_tbl[8] = '{ 1,  2,  4,  8, 16, 32, 64, 64};
  function bit [7:0] pages();  return pages_tbl[pick];  endfunction
  function bit [7:0] stride(); return stride_tbl[pick]; endfunction
endclass

class region_txn;                             // procedural work before the solve
  rand bit [31:0] addr;
  bit [31:0] base;                            // plain field: a constant to the solver
  bit [31:0] region_tbl[4] = '{32'h0000_0000, 32'h1000_0000, 32'h2000_0000, 32'h3000_0000};
  function void pre_randomize();
    base = region_tbl[$urandom_range(3)];     // any procedural choice
  endfunction
  constraint c { addr inside {[base : base + 32'h0FFF]}; }
endclass

product form: last pair 64 x 32 = 2048
table form: 8 of 8 rows used, every pair legal
precomputed base: last addr 20000ce5 in region 20000000
PASS: the product, table and precomputed forms all give only legal results; planted bad pairs are rejected

The table form trades reach for speed: it can only produce the eight pairs it holds, while the product form can produce any legal pair. That is a coverage decision, so record it in the test plan rather than leaving it in a comment.

Related topics

• Solver FAQ: Determinism and Vendor Differences