mirror of
https://github.com/verilator/verilator.git
synced 2026-09-06 08:57:23 +02:00
Support dynamic containers in unique constraints (#7947)
Signed-off-by: Adam Kostrzewski <[email protected]>
This commit is contained in:
+69
-43
@@ -2358,65 +2358,91 @@ class ConstraintExprVisitor final : public VNVisitor {
|
||||
for (AstNode* itemp = nodep->rangesp(); itemp; itemp = itemp->nextp()) {
|
||||
if (AstVarRef* const varRefp = VN_CAST(itemp, VarRef)) {
|
||||
AstVar* const varp = varRefp->varp();
|
||||
|
||||
AstNodeDType* const dtypep = varp->dtypep()->skipRefp();
|
||||
if (AstUnpackArrayDType* const up = VN_CAST(dtypep, UnpackArrayDType)) {
|
||||
AstRange* const rangep = up->rangep();
|
||||
if (!rangep || !VN_IS(rangep->leftp(), Const)
|
||||
|| !VN_IS(rangep->rightp(), Const)) {
|
||||
nodep->v3warn(
|
||||
CONSTRAINTIGN,
|
||||
"Unsupported: Unique constraint on other than static arrays");
|
||||
continue;
|
||||
}
|
||||
AstConst* dtypeWidthp = nullptr;
|
||||
|
||||
// Ensure it is ONLY 1-D by checking that the sub-type is NOT an array/queue
|
||||
// We skip refs (typedefs) to see the actual underlying type
|
||||
AstNodeDType* const subp = up->subDTypep()->skipRefp();
|
||||
if (VN_IS(subp, NodeArrayDType) || VN_IS(subp, QueueDType)
|
||||
|| VN_IS(subp, DynArrayDType)) {
|
||||
nodep->v3warn(
|
||||
CONSTRAINTIGN,
|
||||
"Unsupported: Unique constraint on other than static arrays");
|
||||
continue;
|
||||
}
|
||||
} else {
|
||||
// Ensure it is ONLY 1-D by checking that the sub-type is NOT an array/queue
|
||||
AstNodeDType* const subp = dtypep->subDTypep()->skipRefp();
|
||||
if (VN_IS(subp, NodeArrayDType) || VN_IS(subp, QueueDType)
|
||||
|| VN_IS(subp, DynArrayDType) || VN_IS(subp, AssocArrayDType)
|
||||
|| VN_IS(subp, WildcardArrayDType)) {
|
||||
nodep->v3warn(CONSTRAINTIGN,
|
||||
"Unsupported: Unique constraint on other than static arrays");
|
||||
"Unsupported: Unique constraint on multidimensional arrays");
|
||||
continue;
|
||||
}
|
||||
|
||||
AstCMethodHard* const wCallp
|
||||
const static auto dynDTypeSupported
|
||||
= [](const AstNodeDType* const dtypep) -> bool {
|
||||
return VN_IS(dtypep, DynArrayDType) || VN_IS(dtypep, QueueDType)
|
||||
|| VN_IS(dtypep, AssocArrayDType);
|
||||
};
|
||||
|
||||
if (AstUnpackArrayDType* const up = VN_CAST(dtypep, UnpackArrayDType)) {
|
||||
const AstRange* const rangep = up->rangep();
|
||||
UASSERT_OBJ(rangep && VN_IS(rangep->leftp(), Const)
|
||||
&& VN_IS(rangep->rightp(), Const),
|
||||
nodep, "Unpack array does not have a constant range");
|
||||
dtypeWidthp = new AstConst{fl, AstConst::Unsized64{},
|
||||
static_cast<uint64_t>(varp->dtypep()->width())};
|
||||
} else if (dynDTypeSupported(dtypep)) {
|
||||
dtypeWidthp
|
||||
= new AstConst{fl, AstConst::Unsized64{},
|
||||
static_cast<uint64_t>(dtypep->subDTypep()->width())};
|
||||
} else {
|
||||
nodep->v3warn(CONSTRAINTIGN, "Unsupported: Unique constraint on "
|
||||
<< dtypep->prettyDTypeName(false));
|
||||
continue;
|
||||
}
|
||||
|
||||
// convert to c string
|
||||
AstNodeExpr* const varnamep = new AstCExpr{
|
||||
fl, AstCExpr::Pure{}, "\"" + varp->name() + "\"", varp->width()};
|
||||
|
||||
AstCMethodHard* const writeVarCallp
|
||||
= new AstCMethodHard{fl, new AstVarRef{fl, modp, genVarp, VAccess::READ},
|
||||
VCMethod::RANDOMIZER_WRITE_VAR};
|
||||
wCallp->addPinsp(new AstVarRef{fl, varp, VAccess::READ});
|
||||
wCallp->addPinsp(new AstConst{fl, AstConst::Unsized64{},
|
||||
static_cast<uint64_t>(varp->dtypep()->width())});
|
||||
wCallp->addPinsp(new AstConst{fl, AstConst::String{}, varp->name()});
|
||||
wCallp->addPinsp(new AstConst{fl, 1}); // Dimension
|
||||
writeVarCallp->addPinsp(new AstVarRef{fl, varp, VAccess::READ});
|
||||
writeVarCallp->addPinsp(dtypeWidthp);
|
||||
writeVarCallp->addPinsp(varnamep);
|
||||
writeVarCallp->addPinsp(new AstConst{fl, 1}); // Dimension
|
||||
|
||||
wCallp->dtypeSetVoid();
|
||||
initTaskp->addStmtsp(new AstStmtExpr{fl, wCallp});
|
||||
writeVarCallp->dtypeSetVoid();
|
||||
initTaskp->addStmtsp(new AstStmtExpr{fl, writeVarCallp});
|
||||
|
||||
AstNodeExpr* const randUniquePinsp
|
||||
= new AstConst{fl, AstConst::String{}, varp->name()};
|
||||
|
||||
uint32_t arraySize = 0;
|
||||
if (AstUnpackArrayDType* const adtypep
|
||||
= VN_CAST(varp->dtypep(), UnpackArrayDType)) {
|
||||
arraySize = adtypep->elementsConst();
|
||||
}
|
||||
if (arraySize > 100) {
|
||||
nodep->v3warn(CONSTRAINTIGN,
|
||||
"Unsupported: Unique constraint on static arrays of size > 100");
|
||||
uint32_t arraySize = adtypep->elementsConst();
|
||||
if (arraySize > 100) {
|
||||
nodep->v3warn(
|
||||
CONSTRAINTIGN,
|
||||
"Unsupported: Unique constraint on static arrays of size > 100");
|
||||
VL_DO_DANGLING(randUniquePinsp->deleteTree(), randUniquePinsp);
|
||||
continue;
|
||||
}
|
||||
randUniquePinsp->addNext(new AstConst{fl, arraySize});
|
||||
} else if (dynDTypeSupported(dtypep)) { // LCOV_EXCL_BR_LINE
|
||||
const VCMethod sizeMethod = VN_IS(dtypep, AssocArrayDType)
|
||||
? VCMethod::ASSOC_SIZE
|
||||
: VCMethod::DYN_SIZE;
|
||||
AstCMethodHard* const dynSizep = new AstCMethodHard{
|
||||
fl, new AstVarRef{fl, modp, varp, VAccess::READ}, sizeMethod};
|
||||
dynSizep->dtypeSetUInt32();
|
||||
// unable to check dynamic array size during verilation
|
||||
randUniquePinsp->addNext(dynSizep);
|
||||
} else {
|
||||
varp->v3fatalSrc("Unexpected variable type "
|
||||
<< varp->dtypep()->prettyDTypeNameQ());
|
||||
continue;
|
||||
}
|
||||
|
||||
AstNodeExpr* const uPins = new AstConst{fl, AstConst::String{}, varp->name()};
|
||||
uPins->addNext(new AstConst{fl, arraySize});
|
||||
|
||||
AstCMethodHard* const uCallp
|
||||
AstCMethodHard* const randUniqueCallp
|
||||
= new AstCMethodHard{fl, new AstVarRef{fl, modp, genVarp, VAccess::READ},
|
||||
VCMethod::RANDOMIZER_UNIQUE, uPins};
|
||||
uCallp->dtypep(nodep->findVoidDType());
|
||||
initTaskp->addStmtsp(new AstStmtExpr{fl, uCallp});
|
||||
VCMethod::RANDOMIZER_UNIQUE, randUniquePinsp};
|
||||
randUniqueCallp->dtypep(nodep->findVoidDType());
|
||||
initTaskp->addStmtsp(new AstStmtExpr{fl, randUniqueCallp});
|
||||
}
|
||||
}
|
||||
nodep->unlinkFrBack();
|
||||
|
||||
Executable
+21
@@ -0,0 +1,21 @@
|
||||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||
#
|
||||
# This program is free software; you can redistribute it and/or modify it
|
||||
# under the terms of either the GNU Lesser General Public License Version 3
|
||||
# or the Perl Artistic License Version 2.0.
|
||||
# SPDX-FileCopyrightText: 2026 Wilson Snyder
|
||||
# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
||||
|
||||
import vltest_bootstrap
|
||||
|
||||
test.scenarios('simulator')
|
||||
|
||||
if not test.have_solver:
|
||||
test.skip("No constraint solver installed")
|
||||
|
||||
test.compile()
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
@@ -0,0 +1,100 @@
|
||||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain
|
||||
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
// Based on t_constraint_unsup_unq_arr.v
|
||||
// We only check uniqueness for small # of elements on a large range
|
||||
// as Z3 does not actually give unique elements (bug?) as of Jul 2026.
|
||||
|
||||
module t;
|
||||
class UniqueMultipleArray;
|
||||
rand bit [15:0] arr[4];
|
||||
rand bit [15:0] darr[];
|
||||
rand bit [15:0] queue[$];
|
||||
rand bit [15:0] queue_c[$:3];
|
||||
rand bit [15:0] assoc[int];
|
||||
|
||||
constraint c {
|
||||
unique {arr};
|
||||
unique {darr};
|
||||
unique {queue};
|
||||
unique {queue_c};
|
||||
unique {assoc};
|
||||
}
|
||||
|
||||
function new;
|
||||
darr = new[4];
|
||||
queue = {0, 0, 0, 0};
|
||||
queue_c = {0, 0, 0, 0};
|
||||
assoc = '{0: 0, 1: 0, 3: 0, 5: 0};
|
||||
endfunction
|
||||
|
||||
function bit check_unique();
|
||||
// static array
|
||||
for (int i = 0; i < $size(arr); i++) begin
|
||||
for (int j = i + 1; j < $size(arr); j++) begin
|
||||
if (arr[i] == arr[j]) begin
|
||||
$error("UNIQUENESS VIOLATION: arr[%0d] == arr[%0d] == 0x%h", i, j, arr[i]);
|
||||
return 0;
|
||||
end
|
||||
end
|
||||
end
|
||||
// dynamic array
|
||||
for (int i = 0; i < darr.size(); i++) begin
|
||||
for (int j = i + 1; j < darr.size(); j++) begin
|
||||
if (darr[i] == darr[j]) begin
|
||||
$error("UNIQUENESS VIOLATION: darr[%0d] == darr[%0d] == 0x%h", i, j,
|
||||
darr[i]);
|
||||
return 0;
|
||||
end
|
||||
end
|
||||
end
|
||||
// queue
|
||||
for (int i = 0; i < queue.size(); i++) begin
|
||||
for (int j = i + 1; j < queue.size(); j++) begin
|
||||
if (queue[i] == queue[j]) begin
|
||||
$error("UNIQUENESS VIOLATION: queue[%0d] == queue[%0d] == 0x%h", i, j,
|
||||
queue[i]);
|
||||
return 0;
|
||||
end
|
||||
end
|
||||
end
|
||||
// queue_c
|
||||
for (int i = 0; i < queue_c.size(); i++) begin
|
||||
for (int j = i + 1; j < queue_c.size(); j++) begin
|
||||
if (queue_c[i] == queue_c[j]) begin
|
||||
$error("UNIQUENESS VIOLATION: queue_c[%0d] == queue_c[%0d] == 0x%h", i, j,
|
||||
queue_c[i]);
|
||||
return 0;
|
||||
end
|
||||
end
|
||||
end
|
||||
// assoc array
|
||||
foreach (assoc[i]) begin
|
||||
foreach (assoc[j]) begin
|
||||
if (i == j) begin
|
||||
continue;
|
||||
end
|
||||
if (assoc[i] == assoc[j]) begin
|
||||
$error("UNIQUENESS VIOLATION: assoc[%0d] == assoc[%0d] == 0x%h", i, j,
|
||||
assoc[i]);
|
||||
return 0;
|
||||
end
|
||||
end
|
||||
end
|
||||
return 1;
|
||||
endfunction
|
||||
|
||||
endclass : UniqueMultipleArray
|
||||
|
||||
initial begin
|
||||
automatic UniqueMultipleArray a = new();
|
||||
a.randomize();
|
||||
assert(a.check_unique());
|
||||
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
endmodule : t
|
||||
@@ -1,23 +1,31 @@
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:19:5: Unsupported: Unique constraint on static arrays of size > 100
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:20:5: Unsupported: Unique constraint on static arrays of size > 100
|
||||
: ... note: In instance 't'
|
||||
19 | unique {uniq_val_arr_400};
|
||||
20 | unique {uniq_val_arr_400};
|
||||
| ^~~~~~
|
||||
... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest
|
||||
... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message.
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:22:5: Unsupported: Unique constraint on other than static arrays
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:21:5: Unsupported: Unique constraint on multidimensional arrays
|
||||
: ... note: In instance 't'
|
||||
22 | unique {uniq_val_darr};
|
||||
21 | unique {uniq_val_arr_multidim_arr};
|
||||
| ^~~~~~
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:23:5: Unsupported: Unique constraint on other than static arrays
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:22:5: Unsupported: Unique constraint on multidimensional arrays
|
||||
: ... note: In instance 't'
|
||||
23 | unique {uniq_val_hash};
|
||||
22 | unique {uniq_val_arr_multidim_dynarr};
|
||||
| ^~~~~~
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:24:5: Unsupported: Unique constraint on other than static arrays
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:23:5: Unsupported: Unique constraint on multidimensional arrays
|
||||
: ... note: In instance 't'
|
||||
24 | unique {uniq_val_queue};
|
||||
23 | unique {uniq_val_arr_multidim_queue};
|
||||
| ^~~~~~
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:25:5: Unsupported: Unique constraint on other than static arrays
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:24:5: Unsupported: Unique constraint on multidimensional arrays
|
||||
: ... note: In instance 't'
|
||||
25 | unique {uniq_val_arr_mda};
|
||||
24 | unique {uniq_val_arr_multidim_assoc};
|
||||
| ^~~~~~
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:25:5: Unsupported: Unique constraint on multidimensional arrays
|
||||
: ... note: In instance 't'
|
||||
25 | unique {uniq_val_arr_multidim_wild};
|
||||
| ^~~~~~
|
||||
%Warning-CONSTRAINTIGN: t/t_constraint_unsup_unq_arr.v:26:5: Unsupported: Unique constraint on WILDCARDARRAYDTYPE
|
||||
: ... note: In instance 't'
|
||||
26 | unique {uniq_val_wild};
|
||||
| ^~~~~~
|
||||
%Error: Exiting due to
|
||||
|
||||
@@ -3,54 +3,28 @@
|
||||
// This file ONLY is placed under the Creative Commons Public Domain
|
||||
// SPDX-FileCopyrightText: 2025 AsFigo
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
// uniqueness check moved to t_constrained_unq_arr.v
|
||||
|
||||
class UniqueMultipleArray;
|
||||
rand bit [15:0] uniq_val_arr[4];
|
||||
rand bit [15:0] uniq_val_arr_400[400];
|
||||
rand bit [15:0] uniq_val_arr_mda[4][];
|
||||
rand bit [15:0] uniq_val_darr[];
|
||||
rand bit [15:0] uniq_val_hash[int];
|
||||
rand bit [15:0] uniq_val_queue[$];
|
||||
rand bit b1;
|
||||
rand int array[2]; // 2,4,6 // TODO: add rand when supported
|
||||
rand bit [15:0] uniq_val_arr_400[400]; // unsupported (size > 100)
|
||||
rand bit [15:0] uniq_val_arr_multidim_arr[4][4]; // unsupported (dim > 1)
|
||||
rand bit [15:0] uniq_val_arr_multidim_dynarr[4][]; // unsupported (dim > 1)
|
||||
rand bit [15:0] uniq_val_arr_multidim_queue[4][$]; // unsupported (dim > 1)
|
||||
rand bit [15:0] uniq_val_arr_multidim_assoc[4][int]; // unsupported (dim > 1)
|
||||
rand bit [15:0] uniq_val_arr_multidim_wild[4][*]; // unsupported (dim > 1)
|
||||
rand bit [15:0] uniq_val_wild[*]; // unsupported
|
||||
|
||||
// Constraint to ensure the elements in the array are unique
|
||||
constraint unique_c {
|
||||
unique {uniq_val_arr}; // Ensure unique values in the array
|
||||
unique {uniq_val_arr_400}; // Ensure unique values in the array
|
||||
unique {uniq_val_arr_400};
|
||||
unique {uniq_val_arr_multidim_arr};
|
||||
unique {uniq_val_arr_multidim_dynarr};
|
||||
unique {uniq_val_arr_multidim_queue};
|
||||
unique {uniq_val_arr_multidim_assoc};
|
||||
unique {uniq_val_arr_multidim_wild};
|
||||
unique {uniq_val_wild};
|
||||
}
|
||||
constraint unique_c1 {
|
||||
unique {uniq_val_darr}; // Ensure unique values in the array
|
||||
unique {uniq_val_hash}; // Ensure unique values in the array
|
||||
unique {uniq_val_queue}; // Ensure unique values in the array
|
||||
unique {uniq_val_arr_mda}; // Ensure unique values in the array
|
||||
unique {array[0], array[1]};
|
||||
}
|
||||
// --------------------------------------------------
|
||||
// Explicit uniqueness checker (post-solve validation)
|
||||
// --------------------------------------------------
|
||||
function bit check_unique();
|
||||
for (int i = 0; i < $size(uniq_val_arr); i++) begin
|
||||
for (int j = i + 1; j < $size(uniq_val_arr); j++) begin
|
||||
if (uniq_val_arr[i] == uniq_val_arr[j]) begin
|
||||
$error("UNIQUENESS VIOLATION: uniq_val_arr[%0d] == uniq_val_arr[%0d] == 0x%h", i, j,
|
||||
uniq_val_arr[i]);
|
||||
return 0;
|
||||
end
|
||||
end
|
||||
end
|
||||
return 1;
|
||||
endfunction
|
||||
|
||||
function void post_randomize();
|
||||
$display("Randomized values in uniq_val_arr: %p", uniq_val_arr);
|
||||
|
||||
if (!check_unique()) begin
|
||||
$fatal(1, "Post-randomize uniqueness check FAILED");
|
||||
end
|
||||
foreach (uniq_val_arr[i]) begin
|
||||
$display("uniq_val_arr[%0d] = 0x%h", i, uniq_val_arr[i]);
|
||||
end
|
||||
endfunction
|
||||
|
||||
endclass : UniqueMultipleArray
|
||||
|
||||
@@ -58,10 +32,6 @@ module t;
|
||||
initial begin
|
||||
// Create an instance of the UniqueMultipleArray class
|
||||
automatic UniqueMultipleArray array_instance = new();
|
||||
|
||||
// Attempt to randomize and verify the constraints
|
||||
/* verilator lint_off WIDTHTRUNC */
|
||||
assert (array_instance.randomize())
|
||||
else $error("Randomization failed!");
|
||||
array_instance.randomize();
|
||||
end
|
||||
endmodule : t
|
||||
|
||||
Reference in New Issue
Block a user