Refactor disable soft to match by variable name per IEEE spec

This commit is contained in:
Yilou Wang 2026-03-03 10:34:42 +01:00
parent 492eddd8b0
commit 472160683f
3 changed files with 51 additions and 27 deletions

View File

@ -746,9 +746,11 @@ void VlRandomizer::soft(std::string&& constraint, const char* /*filename*/, uint
m_softConstraints.emplace_back(std::move(constraint)); m_softConstraints.emplace_back(std::move(constraint));
} }
void VlRandomizer::disable_soft(std::string&& constraint) { void VlRandomizer::disable_soft(const std::string& varName) {
// IEEE 1800-2017 18.5.13: Remove all soft constraints referencing the variable
m_softConstraints.erase( m_softConstraints.erase(
std::remove(m_softConstraints.begin(), m_softConstraints.end(), constraint), std::remove_if(m_softConstraints.begin(), m_softConstraints.end(),
[&](const std::string& c) { return c.find(varName) != std::string::npos; }),
m_softConstraints.end()); m_softConstraints.end());
} }

View File

@ -596,7 +596,7 @@ public:
const char* source = ""); const char* source = "");
void soft(std::string&& constraint, const char* filename = "", uint32_t linenum = 0, void soft(std::string&& constraint, const char* filename = "", uint32_t linenum = 0,
const char* source = ""); const char* source = "");
void disable_soft(std::string&& constraint); void disable_soft(const std::string& varName);
void clearConstraints(); void clearConstraints();
void clearAll(); // Clear both constraints and variables void clearAll(); // Clear both constraints and variables
void markRandc(const char* name); // Mark variable as randc for cyclic tracking void markRandc(const char* name); // Mark variable as randc for cyclic tracking

View File

@ -1900,6 +1900,31 @@ class ConstraintExprVisitor final : public VNVisitor {
} }
void visit(AstConstraintExpr* nodep) override { void visit(AstConstraintExpr* nodep) override {
// IEEE 1800-2017 18.5.13: "disable soft" removes all soft constraints
// referencing the specified variable. Pass the variable name directly
// instead of going through SMT lowering.
if (nodep->isDisableSoft()) {
// Extract variable name from expression (VarRef or MemberSel)
std::string varName;
if (const AstNodeVarRef* const vrefp = VN_CAST(nodep->exprp(), NodeVarRef)) {
varName = vrefp->name();
} else if (const AstMemberSel* const mselp = VN_CAST(nodep->exprp(), MemberSel)) {
varName = mselp->name();
} else {
nodep->v3warn(E_UNSUPPORTED, "Unsupported expression in disable soft");
return;
}
AstCMethodHard* const callp = new AstCMethodHard{
nodep->fileline(),
new AstVarRef{nodep->fileline(), VN_AS(m_genp->user2p(), NodeModule), m_genp,
VAccess::READWRITE},
VCMethod::RANDOMIZER_DISABLE_SOFT,
new AstConst{nodep->fileline(), AstConst::String{}, varName}};
callp->dtypeSetVoid();
nodep->replaceWith(callp->makeStmt());
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
// IEEE 1800-2017 18.5.1: A bare expression used as a constraint is // IEEE 1800-2017 18.5.1: A bare expression used as a constraint is
// implicitly treated as "expr != 0" when wider than 1 bit. // implicitly treated as "expr != 0" when wider than 1 bit.
// Must wrap before iterateChildren, which converts to SMT format. // Must wrap before iterateChildren, which converts to SMT format.
@ -1920,38 +1945,35 @@ class ConstraintExprVisitor final : public VNVisitor {
VL_DO_DANGLING(nodep->deleteTree(), nodep); VL_DO_DANGLING(nodep->deleteTree(), nodep);
return; return;
} }
// Emit as soft, hard, or disable_soft per IEEE 1800-2017 18.5.13 // Emit as soft or hard constraint per IEEE 1800-2017 18.5.13
const VCMethod method = nodep->isDisableSoft() ? VCMethod::RANDOMIZER_DISABLE_SOFT const VCMethod method
: nodep->isSoft() ? VCMethod::RANDOMIZER_SOFT = nodep->isSoft() ? VCMethod::RANDOMIZER_SOFT : VCMethod::RANDOMIZER_HARD;
: VCMethod::RANDOMIZER_HARD;
AstCMethodHard* const callp = new AstCMethodHard{ AstCMethodHard* const callp = new AstCMethodHard{
nodep->fileline(), nodep->fileline(),
new AstVarRef{nodep->fileline(), VN_AS(m_genp->user2p(), NodeModule), m_genp, new AstVarRef{nodep->fileline(), VN_AS(m_genp->user2p(), NodeModule), m_genp,
VAccess::READWRITE}, VAccess::READWRITE},
method, nodep->exprp()->unlinkFrBack()}; method, nodep->exprp()->unlinkFrBack()};
callp->dtypeSetVoid(); callp->dtypeSetVoid();
if (!nodep->isDisableSoft()) { // Pass filename, lineno, and source as separate arguments
// Pass filename, lineno, and source as separate arguments // This allows EmitC to call protect() on filename, similar to VL_STOP
// This allows EmitC to call protect() on filename, similar to VL_STOP // Add filename parameter
// Add filename parameter callp->addPinsp(new AstCExpr{nodep->fileline(), AstCExpr::Pure{},
callp->addPinsp(new AstCExpr{nodep->fileline(), AstCExpr::Pure{}, "\"" + nodep->fileline()->filename() + "\""});
"\"" + nodep->fileline()->filename() + "\""}); // Add line number parameter
// Add line number parameter const uint32_t lineno = static_cast<uint32_t>(nodep->fileline()->lineno());
const uint32_t lineno = static_cast<uint32_t>(nodep->fileline()->lineno()); callp->addPinsp(new AstConst{nodep->fileline(), lineno});
callp->addPinsp(new AstConst{nodep->fileline(), lineno}); // Add source text parameter (empty if --protect-ids to avoid source leakage)
// Add source text parameter (empty if --protect-ids to avoid source leakage) std::string prettyText;
std::string prettyText; if (!v3Global.opt.protectIds()) {
if (!v3Global.opt.protectIds()) { prettyText = nodep->fileline()->prettySource();
prettyText = nodep->fileline()->prettySource(); size_t pos = 0;
size_t pos = 0; while ((pos = prettyText.find('"', pos)) != std::string::npos) {
while ((pos = prettyText.find('"', pos)) != std::string::npos) { prettyText.insert(pos, "\\");
prettyText.insert(pos, "\\"); pos += std::strlen("\\\"");
pos += std::strlen("\\\"");
}
} }
callp->addPinsp(
new AstCExpr{nodep->fileline(), AstCExpr::Pure{}, "\"" + prettyText + "\""});
} }
callp->addPinsp(
new AstCExpr{nodep->fileline(), AstCExpr::Pure{}, "\"" + prettyText + "\""});
nodep->replaceWith(callp->makeStmt()); nodep->replaceWith(callp->makeStmt());
VL_DO_DANGLING(nodep->deleteTree(), nodep); VL_DO_DANGLING(nodep->deleteTree(), nodep);
} }