One equation over every element

Reduction methods such as sum(), product(), and(), or() and xor() are legal inside constraints. Each makes one equation that couples every element at once, which is how budgets, checksums and counts are written.

The optional with clause transforms each element first. Inside it, item names the current element. The standard also offers item.index, but Verilator 5.048 hit an internal solver error on it, so the course zeroes unused elements instead and reduces the whole array.

Aggregate equations work both ways, like every constraint. The solver can pick bytes to hit a forced total, or derive the total from free bytes.

Widen before summing

The standard says arr.sum() returns the element type. Summing bit [7:0] elements gives an 8-bit total that wraps at 256, so b.sum() == 600 on bytes can never hold.

The fix widens each item inside with: int'(item) moves the total to 32 bits. Verilator 5.048 computed the unwidened sum wide too, which the bench below shows, but other simulators follow the standard. Write the widened form and every tool agrees.

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

class budget;
  rand bit [7:0] weight[4];
  constraint c_total {
    weight.sum() with (int'(item)) == 100;        // widened: a 32-bit total
    foreach (weight[i]) weight[i] inside {[5:60]};
  }
endclass

class narrow;
  rand bit [7:0] b[4];
  constraint c { b.sum() == 600; }                // LRM: an 8-bit total, so 600 never fits
endclass

class wide;
  rand bit [7:0] b[4];
  constraint c { b.sum() with (int'(item)) == 600; }
endclass

class counting;
  rand bit [7:0] data[10];
  rand bit [7:0] mask[6];
  constraint c {
    data.sum() with (int'(item == 8'h5A)) == 3;   // exactly 3 bytes equal 5A
    data.sum() with (int'(item > 200)) <= 2;      // at most 2 above 200
    mask.sum() with (int'(item != 0)) == 1;       // one-hot over the slots
  }
endclass

budget: 23 + 31 + 31 + 15 = 100
unwidened b.sum() == 600: randomize() returned 1, bytes total 600
widened sum == 600: 98 + 109 + 163 + 230
counting: exactly 3 bytes of 5A, at most 2 above 200, one nonzero mask slot, 200 times
PASS: widened sums hit 100 and 600 exactly, and all three counting sums hold

Count with sums of comparisons

A comparison inside with gives 1 or 0 per element, so the sum is a count. One line answers exactly-K, at-most-K and at-least-one, and the one-hot form is item != 0 counted to 1. The counting class above runs all three.

Budget targets need a feasibility check first. Four weights in 5 to 60 can total anything from 20 to 240, so 100 is safe; a target of 250 would make every call fail.

PacketFIFO: a check byte the checker can trust

One way to write it:

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

typedef enum bit [1:0] {DATA = 2'd0, CTRL = 2'd1, ERR = 2'd2} kind_e;

class pkt_txn;
  rand kind_e    kind;
  rand bit [1:0] dest;
  rand bit [3:0] len;
  rand bit [7:0] payload[8];
  rand bit [7:0] check;
  constraint legal_c { len inside {[1:8]}; dest inside {[0:2]}; }
  constraint payload_c { foreach (payload[i]) if (i >= len) payload[i] == 8'h00; }
  // Unused bytes are zero, so XOR over all 8 equals XOR over the first len.
  constraint check_c { check == (8'(kind) ^ 8'(len) ^ payload.xor()); }
endclass

module tb_pkt_check;
  pkt_txn p = new();
  initial begin
    bit [7:0] x;
    repeat (1000) begin
      if (!p.randomize()) $fatal(1, "FAIL: randomize failed");
      x = 8'(p.kind) ^ 8'(p.len);         // the checker's own computation
      for (int i = 0; i < p.len; i++) x ^= p.payload[i];
      if (x != p.check) $fatal(1, "FAIL: check %0h, recomputed %0h", p.check, x);
    end
    $display("last packet: kind %s, len %0d, check %0h", p.kind.name(), p.len, p.check);
    $display("PASS: 1000 packets, every check byte matches the XOR the checker recomputes");
    $finish;
  end
endmodule

last packet: kind CTRL, len 8, check f4
PASS: 1000 packets, every check byte matches the XOR the checker recomputes

The constraint and the bench compute the same byte in two different ways: one as an equation the solver satisfies, one as a loop over len bytes. Agreement over 1000 packets is the evidence. The fault phase from Dynamic Constraint Control can now switch check_c off to plant a wrong check byte on purpose.

Related topics

• foreach Constraints