如何用更优雅的SystemVerilog断言验证数组值的唯一性与完整性？

针对你需要验证logic [254:0][7:0] array包含0到254所有值且唯一的需求，原实现存在循环范围错误（原循环仅遍历到索引253，漏掉了array[254]），同时可以简化逻辑结构、减少冗余信号。以下是几种更简洁的优化方案：

方案一：简化掩码逻辑，合并完整性与唯一性检查 #

通过掩码记录每个值的出现情况，一次检查同时覆盖无重复和所有值都出现两个要求：

bit [254:0] value_present;

always_comb begin
    value_present = '0;
    foreach (array[i]) begin
        // 若当前值已被标记，说明重复，保留标记位为1
        if (value_present[array[i]]) begin
            value_present[array[i]] = 1'b1;
        end else begin
            value_present[array[i]] = 1'b1;
        end
    end
end

UNIQUE_AND_COMPLETE_ARRAY: assert property (
    @(posedge clock) disable iff (!arstn)
    update_array |-> (value_present == '1)
);

用foreach遍历数组更直观，value_present全1既保证了0-254所有值都被覆盖，也隐含了没有重复值（若有重复，不会影响掩码全1，但如果有值缺失，对应位会是0；若重复+缺失，同样会被检测到）。

方案二：去掉冗余延迟触发器，内联检查逻辑 #

原代码中update_array_d用于延迟一拍检测，可直接在断言中用内联逻辑替代，减少额外信号：

UNIQUE_AND_COMPLETE_ARRAY: assert property (
    @(posedge clock) disable iff (!arstn)
    $rose(update_array) |-> ##0 begin
        bit [254:0] temp_mask = '0;
        foreach (array[i]) begin
            if (temp_mask[array[i]]) $error("重复值%0d出现在索引%0d", array[i], i);
            temp_mask[array[i]] = 1'b1;
        end
        temp_mask == '1;
    end
);

这种方式把检查逻辑直接嵌入断言序列块，无需额外组合逻辑always块，同时能在发现重复时直接打印错误位置，方便调试。

方案三：利用SystemVerilog数组方法（需仿真器支持） #

若你的仿真器支持SystemVerilog 2012及以上标准，可借助数组方法简化代码，适合快速验证小规模数组：

UNIQUE_AND_COMPLETE_ARRAY: assert property (
    @(posedge clock) disable iff (!arstn)
    update_array |-> (array.unique().size() == 255) && (array.find(item) with (item inside {[0:254]}).size() == 255)
);

注：这种方式性能可能不如掩码方法高效，且依赖仿真器对数组方法的完整支持。

原代码的最小修正 #

如果要保留原代码结构，至少需要修正循环范围，避免漏掉最后一个数组元素：

for(int i=0; i<=254; i++) // 原代码为i<254，漏掉了array[254]的检查

内容的提问来源于stack exchange，提问作者Michael