Assertion to check array contents for duplicate values

Question

I have an array logic [254:0][7:0] array. By design, this array must consist all values from 0 to 254 exactly once.

I want to write a SystemVerilog assertion to test it.

So far, I came up with something like this:

    logic update_array_d;
    bit [254:0] a_array_dup_mask;

    always_ff @(posedge clock, negedge arstn)
        if(!arstn) update_array_d <= 1'b0;
        else update_array_d <= update_array;

    always_comb begin
        a_array_dup_mask= '0;
        if(update_array_d) begin
            a_array_dup_mask= '1;
            for(int i=0; i<254; i++)
                a_array_dup_mask[array[i]] = 1'b0;
        end
    end
    UNIQUE_ARRAY: assert property (
        @(posedge clock) disable iff (!arstn)
        update_array_d |-> a_array_dup_mask == '0
    );

Is there a more elegant way to implement it?

Answer 1

The code looks fine as long as it works for you and you find it easy to understand.

---

You could also consider this approach.

You declared array as a packed array. Had you declared it as an unpacked array, such as:

logic [7:0] array [255];

then you would have been able to use the unique array method. Refer to IEEE Std 1800-2017, section 7.12.1 Array locator methods. But you would have also needed to declare an intermediate queue variable as well. Whether this is more elegant is debatable. Something along the lines of:

logic [7:0] array [255];
logic [7:0] q [$];
q = array.unique();
if (q.size() == $size(array)) // there are no duplicates in the array