Implication, if/else and solve...before taught that a -> b means !a || b and that solve...before moves probability, never legality. This lesson uses those rules to explain three effects that surprise people in real benches.

Every rule pushes both ways

A constraint is an equation, not an assignment, so it limits every field it names. Force the result and the inputs move; make a consequent impossible and the antecedent can never be true.

1
2
3
4
5
6
7

// snippet
constraint c { total == a + b; a inside {[10:20]}; }
// randomize() with { total == 250; }  ->  b is pushed into 230..240

constraint c2 { (a == 5) -> (b == 100); }   // b is 4 bits
// b == 100 cannot hold, so every tuple with a == 5 is removed:
// a is never 5, and nothing warns you

A function call stops the push-back

A constraint may call a function, such as total_len >= min_len(n_bursts). The standard cannot invert a function, so it solves the function's arguments first, evaluates the call to a constant, and then solves the rest. Later rules cannot push back through the call.

Verilator 5.048 pushed back through the call anyway and solved every call, which is kinder than the standard. Code that leans on that breaks on the next simulator. When the bound is simple arithmetic, write it as an expression, total_len >= n_bursts * 8, and both tools agree.

Division and modulo by a rand field need their own guard. This short fragment is an illustration, so the course checks skip it.

1
2
3
4
5

// snippet
constraint a_c {
  len > 0;                 // always pair a rand divisor with this guard
  addr % len == 0;         // divisor is rand
}

Verilator never picked len == 0 in 400 unguarded calls, but the standard gives no promise, and a zero divisor makes the expression undefined. The guard costs one line.

Starvation, and three fixes

A control field starves when one of its values admits few completions. An enable bit beside a wide length is the classic case: en == 0 forces len == 0, one tuple, while en == 1 allows 1024 tuples. A uniform pick gives en == 0 once in 1025 calls.

The standard's fix is solve en before len, which picks en from its own two values first. Verilator gave 26% instead of 50%: better than starving, but not what the standard says. A dist on en states the share outright, and Verilator honoured it. When a share matters, write it down.

The bench runs the three classes 1000 times each and checks that en and len always agree. It asserts the starvation and the dist share, and prints the solve...before share.

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
31
32
33
34
35
36
37

class dma_plain;
  rand bit        en;
  rand bit [15:0] len;
  constraint c_len { (en == 0) -> (len == 0); (en == 1) -> (len inside {[1:1024]}); }
endclass

class dma_order extends dma_plain;
  constraint c_ord { solve en before len; }   // the standard's fix: stage en first
endclass

class dma_dist extends dma_plain;
  constraint c_en { en dist {0 := 1, 1 := 1}; }   // say the share outright
endclass

module tb_starve;
  dma_plain p = new();
  dma_order o = new();
  dma_dist  d = new();
  int off_p = 0, off_o = 0, off_d = 0;
  initial begin
    repeat (1000) begin
      if (!p.randomize() || !o.randomize() || !d.randomize()) $fatal(1, "FAIL: a solve failed");
      if ((p.en == 0) != (p.len == 0) || (o.en == 0) != (o.len == 0) || (d.en == 0) != (d.len == 0))
        $fatal(1, "FAIL: en and len disagree");
      off_p += !p.en;
      off_o += !o.en;
      off_d += !d.en;
    end
    $display("en == 0 out of 1000: plain %0d (uniform over tuples: about 1)", off_p);
    $display("en == 0 out of 1000: solve en before len %0d (standard: about 500)", off_o);
    $display("en == 0 out of 1000: en dist 1:1 %0d (about 500)", off_d);
    if (off_p > 30) $fatal(1, "FAIL: the plain class should starve en == 0");
    if (off_d < 440 || off_d > 560) $fatal(1, "FAIL: dist share outside 45 to 55 percent");
    $display("PASS: plain starves the disabled case, and the dist fix gives it half the calls");
    $finish;
  end
endmodule

en == 0 out of 1000: plain 7 (uniform over tuples: about 1)
en == 0 out of 1000: solve en before len 263 (standard: about 500)
en == 0 out of 1000: en dist 1:1 498 (about 500)
PASS: plain starves the disabled case, and the dist fix gives it half the calls

The second bench checks the push-back claims: the impossible consequent, the forced total, and the function call beside its expression form.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

class backward;
  rand bit [3:0] a, b;
  constraint c { (a == 5) -> (b == 100); }  // b is 4 bits: b == 100 is impossible
endclass

class pair_sum;
  rand bit [7:0] a, b;
  rand bit [8:0] total;
  constraint c { total == a + b; a inside {[10:20]}; }
endclass

class frame_fn;                               // the bound comes from a function
  rand bit [3:0] n_bursts;
  rand bit [9:0] total_len;
  function int min_len(bit [3:0] n); return n * 8; endfunction
  constraint c { n_bursts inside {[1:8]}; total_len >= min_len(n_bursts); total_len <= 512; }
endclass

class frame_expr;                             // the same bound as an expression
  rand bit [3:0] n_bursts;
  rand bit [9:0] total_len;
  constraint c { n_bursts inside {[1:8]}; total_len >= n_bursts * 8; total_len <= 512; }
endclass

a == 5 in 0 of 2000 results (the impossible consequent bans it)
total forced to 250: a 17, b 233 (b pushed into 230..240)
total_len < 16: function form solved 400 of 400, expression form 400 of 400
PASS: the impossible consequent bans a == 5, a forced total pushes b, and the expression form always solves

Ordering chains must form a tree or a line, never a loop: solve a before b; solve b before a; is rejected at compile time. Order only the control fields; ordering everything skews shares nobody meant to touch.

Related topics

• randc Internals & Limits