Support constraints on associative array user-defined keys (#5671) (#5729)

This commit is contained in:
Yilou Wang
2025-01-11 12:07:52 -05:00
committed by GitHub
parent dfe28f7ed0
commit d3e205f201
7 changed files with 253 additions and 25 deletions
+26 -16
View File
@@ -709,7 +709,7 @@ class ConstraintExprVisitor final : public VNVisitor {
void visit(AstAssocSel* nodep) override {
if (editFormat(nodep)) return;
FileLine* const fl = nodep->fileline();
if (VN_IS(nodep->bitp(), CvtPackString)) {
if (VN_IS(nodep->bitp(), CvtPackString) && VN_IS(nodep->bitp()->dtypep(), BasicDType)) {
AstCvtPackString* const stringp = VN_AS(nodep->bitp(), CvtPackString);
const size_t stringSize = VN_AS(stringp->lhsp(), Const)->width();
if (stringSize > 128) {
@@ -724,22 +724,32 @@ class ConstraintExprVisitor final : public VNVisitor {
handle.relink(idxp);
editSMT(nodep, nodep->fromp(), idxp);
} else {
VNRelinker handle;
const int actual_width = nodep->bitp()->width();
std::string fmt;
// Normalize to standard bit width
if (actual_width <= 8) {
fmt = "#x%2x";
} else if (actual_width <= 16) {
fmt = "#x%4x";
} else {
fmt = "#x%" + std::to_string(VL_WORDS_I(actual_width) * 8) + "x";
}
if (VN_IS(nodep->bitp()->dtypep(), BasicDType)
|| (VN_IS(nodep->bitp()->dtypep(), StructDType)
&& VN_AS(nodep->bitp()->dtypep(), StructDType)->packed())
|| VN_IS(nodep->bitp()->dtypep(), EnumDType)
|| VN_IS(nodep->bitp()->dtypep(), PackArrayDType)) {
VNRelinker handle;
const int actual_width = nodep->bitp()->width();
std::string fmt;
// Normalize to standard bit width
if (actual_width <= 8) {
fmt = "#x%2x";
} else if (actual_width <= 16) {
fmt = "#x%4x";
} else {
fmt = "#x%" + std::to_string(VL_WORDS_I(actual_width) * 8) + "x";
}
AstNodeExpr* const idxp
= new AstSFormatF{fl, fmt, false, nodep->bitp()->unlinkFrBack(&handle)};
handle.relink(idxp);
editSMT(nodep, nodep->fromp(), idxp);
AstNodeExpr* const idxp
= new AstSFormatF{fl, fmt, false, nodep->bitp()->unlinkFrBack(&handle)};
handle.relink(idxp);
editSMT(nodep, nodep->fromp(), idxp);
} else {
nodep->bitp()->v3error(
"Illegal non-integral expression or subexpression in random constraint."
" (IEEE 1800-2023 18.3)");
}
}
}
void visit(AstArraySel* nodep) override {