All different in one keyword

The unique constraint makes every listed value pairwise distinct. unique { arr } means arr[i] != arr[j] for every pair of different indexes, in a form solvers can treat as one all-different rule.

The braces can mix scalars and arrays: unique { master_id, id } keeps the scalar different from every element too. Verilator 5.048 honoured unique only on a fixed-size array, and only when another rule also named the elements: unique { v } alone on bit [3:0] v[8] repeated a value in 85 of 100 results. On a dynamic array or a mixed list it printed a CONSTRAINTIGN warning and ignored the rule. The written-out pairwise form works everywhere.

1
2
3
4
5
6

// snippet
unique { id };                 // array elements all distinct
unique { master_id, id };      // a scalar and an array together
unique { a, b, c };            // three scalars pairwise distinct
foreach (p[i]) foreach (p[j])  // the written-out form, for any array
  if (i < j) p[i] != p[j];

Check the pigeonhole first. The value type must offer at least as many values as the set has entries, counted after range rules shrink the space.

The permutation recipe

Fix the size to N, keep every element in [0:N-1], and require uniqueness. With N values squeezed into N distinct slots, only permutations remain, and extra rules such as p[0] != 0 compose with it.

The bench runs that recipe on a fixed array with unique, checks the pigeonhole case, and then compares unique and the written-out form on a dynamic array.

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

class perm8;
  rand bit [3:0] p[8];
  constraint c_range { foreach (p[i]) p[i] inside {[0:7]}; }
  constraint c_diff  { unique { p }; }             // all eight distinct
  constraint c_first { p[0] != 0; }
endclass

class pigeon;
  rand bit [1:0] id[5];                            // 4 values, 5 slots
  constraint c_diff { unique { id }; }
endclass

class dyn_unique;                                  // unique on a dynamic array
  rand bit [3:0] p[];
  constraint c { p.size() == 8; foreach (p[i]) p[i] inside {[0:7]}; unique { p }; }
endclass

class dyn_pairwise;                                // the same rule written out
  rand bit [3:0] p[];
  constraint c { p.size() == 8; foreach (p[i]) p[i] inside {[0:7]};
                 foreach (p[i]) foreach (p[j]) if (i < j) p[i] != p[j]; }
endclass

permutation: '{'h6, 'h5, 'h0, 'h2, 'h3, 'h4, 'h1, 'h7}
pigeonhole, 5 distinct 2-bit ids: randomize() returned 0
dynamic array, unique keyword: 50 of 50 results repeat a value
dynamic array, pairwise !=:    0 of 50 results repeat a value
PASS: unique on a fixed array and pairwise != on a dynamic one give true permutations; 5 into 4 is unsatisfiable

The dynamic unique line is the lesson about tools: it compiled, warned once, and gave wrong answers every time. A bench that checks its own results catches that; one that only prints values does not.

The procedural shuffle() method is the cheap alternative when no extra rules apply. It cannot express rules like p[0] != 0, so reach for the solver only for constrained permutations.

A rand index names the special position when later rules need it. This short fragment is an illustration, so the course checks skip it.

1
2
3
4
5
6
7
8

// snippet
rand int unsigned hot;
constraint c_hot {
  hot < 8;
  foreach (a[i]) (i == hot) ? (a[i] != 0) : (a[i] == 0);
}
// The index form wins when later rules name the position,
// e.g. hot >= 4 keeps the nonzero element in the upper half.

Unique is spatial, randc is temporal

unique enforces distinctness within one call, across the listed elements. randc enforces no repeats across successive calls of one variable, cycling its whole value space before any value comes back.

The two do not combine freely. randc cannot take part in solve...before, so weighted non-repeating values need rand, constraints, and history kept in the class.

Related topics

• sum(), Aggregate Constraints