Support implication operator with constraint_set (#7300) (#7448)

* Support implication operator with constraint_set

* improve coverage, achieve 100 line cov

* Address review: simplify addNext; tighten disable soft grammar to constraint_primary

* Apply 'make format'

* re-run

---------

Co-authored-by: github action <action@example.com>
This commit is contained in:
Yilou Wang 2026-04-23 10:50:23 +02:00 committed by GitHub
parent 46a6884df6
commit cfebe805c9
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
10 changed files with 505 additions and 29 deletions

View File

@ -2007,6 +2007,10 @@ class ConstraintExprVisitor final : public VNVisitor {
void visit(AstSFormatF* nodep) override {}
void visit(AstStmtExpr* nodep) override {}
void visit(AstCStmt* nodep) override {}
void visit(AstIf* nodep) override {
// Hoisted runtime-conditional disable_soft statements parked in the
// constraint-items list by the pre-pass; already fully lowered.
}
void visit(AstConstraintIf* nodep) override {
AstNodeExpr* newp = nullptr;
FileLine* const fl = nodep->fileline();
@ -2192,28 +2196,13 @@ class ConstraintExprVisitor final : public VNVisitor {
}
void visit(AstConstraintExpr* nodep) override {
// IEEE 1800-2023 18.5.13: "disable soft" removes all soft constraints
// referencing the specified variable. Pass the variable name directly
// instead of going through SMT lowering.
// IEEE 1800-2023 18.5.13: 'disable soft' is a meta-level directive on
// the constraint graph, lowered to a void RANDOMIZER_DISABLE_SOFT
// call. Conditional occurrences (if / foreach / implication body)
// are rewritten by extractConditionalDisableSofts() before this
// visitor runs, so anything we see here is unconditional.
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->v3fatalSrc("Unexpected expression type 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());
nodep->replaceWith(buildDisableSoftCallStmt(nodep));
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
@ -2603,6 +2592,93 @@ class ConstraintExprVisitor final : public VNVisitor {
"Visit function missing? Constraint function missing for node: " << nodep);
}
// Build the runtime statement that calls RANDOMIZER_DISABLE_SOFT on the
// variable referenced by the given AstConstraintExpr. Parser enforces
// constraint_primary operand (verilog.y, IEEE 1800-2023 18.5.13).
AstNode* buildDisableSoftCallStmt(AstConstraintExpr* nodep) {
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->v3fatalSrc("Unexpected expression type in disable soft");
}
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();
return callp->makeStmt();
}
// Pre-pass: for every AstConstraintExpr(isDisableSoft) nested inside an
// AstConstraintIf subtree (any depth), return a list of runtime AstIf
// statements `if (accumulated_cond) randomizer.disable_soft(var);` where
// accumulated_cond AND-folds the enclosing then/else branch conditions.
// The original ConstraintExpr is replaced with `1'b1` so editSingle()
// folds the surrounding boolean cleanly. Caller appends the returned
// list to the constraint-items chain; that chain becomes the setup task
// body, which runs before the solver on every randomize() call -- giving
// disable-soft real conditional semantics per IEEE 1800-2023 18.5.13.
AstNode* extractConditionalDisableSofts(AstNode* itemsp, AstNodeExpr* outerCondp) {
AstNode* hoistListp = nullptr;
for (AstNode *stmtp = itemsp, *nextp; stmtp; stmtp = nextp) {
nextp = stmtp->nextp();
if (AstConstraintIf* const ifp = VN_CAST(stmtp, ConstraintIf)) {
FileLine* const fl = ifp->fileline();
// then branch: accumulated = outer && this.cond
AstNodeExpr* const thenCondp
= outerCondp ? static_cast<AstNodeExpr*>(
new AstLogAnd{fl, outerCondp->cloneTreePure(false),
ifp->condp()->cloneTreePure(false)})
: ifp->condp()->cloneTreePure(false);
if (AstNode* const thenHoistp
= extractConditionalDisableSofts(ifp->thensp(), thenCondp)) {
hoistListp
= hoistListp ? AstNode::addNext(hoistListp, thenHoistp) : thenHoistp;
}
VL_DO_DANGLING(thenCondp->deleteTree(), thenCondp);
if (ifp->elsesp()) {
// else branch: accumulated = outer && !this.cond
AstNodeExpr* const notInnerp
= new AstLogNot{fl, ifp->condp()->cloneTreePure(false)};
AstNodeExpr* const elseCondp
= outerCondp ? static_cast<AstNodeExpr*>(new AstLogAnd{
fl, outerCondp->cloneTreePure(false), notInnerp})
: notInnerp;
if (AstNode* const elseHoistp
= extractConditionalDisableSofts(ifp->elsesp(), elseCondp)) {
hoistListp
= hoistListp ? AstNode::addNext(hoistListp, elseHoistp) : elseHoistp;
}
VL_DO_DANGLING(elseCondp->deleteTree(), elseCondp);
}
} else if (AstConstraintExpr* const exprp = VN_CAST(stmtp, ConstraintExpr)) {
if (exprp->isDisableSoft() && outerCondp) {
FileLine* const fl = exprp->fileline();
AstIf* const hoistIfp = new AstIf{fl, outerCondp->cloneTreePure(false),
buildDisableSoftCallStmt(exprp), nullptr};
hoistListp = hoistListp ? AstNode::addNext(hoistListp,
static_cast<AstNode*>(hoistIfp))
: static_cast<AstNode*>(hoistIfp);
// Replace in-tree disable-soft with a no-op boolean
// constraint so editSingle() folds cleanly.
AstConstraintExpr* const truep
= new AstConstraintExpr{fl, new AstConst{fl, AstConst::BitTrue{}}};
exprp->replaceWith(truep);
VL_DO_DANGLING(exprp->deleteTree(), exprp);
}
}
// foreach/unique bodies are left untouched: disable-soft inside
// a foreach would need per-iteration condition support, and
// unique cannot legally contain disable-soft.
}
return hoistListp;
}
public:
// CONSTRUCTORS
explicit ConstraintExprVisitor(AstClass* classp, VMemberMap& memberMap, AstNode* nodep,
@ -2618,6 +2694,14 @@ public:
, m_memberMap{memberMap}
, m_writtenVars{writtenVars}
, m_sizeConstrainedArraysp{sizeConstrainedArraysp} {
// Pre-pass before SMT lowering: extract conditional disable-soft
// directives as runtime AstIf statements and append them to the
// constraint-items chain so they reach the setup task body. The SMT
// visitor skips these via visit(AstIf) above.
if (AstNode* const hoistListp
= nodep ? extractConditionalDisableSofts(nodep, nullptr) : nullptr) {
nodep->addNext(hoistListp);
}
iterateAndNextNull(nodep);
}
};

View File

@ -5085,11 +5085,11 @@ expr<nodeExprp>: // IEEE: part of expression/constant_expression/
| type_referenceEq yP_EQUAL type_referenceBoth { $$ = new AstEqT{$2, $1, $3}; }
| type_referenceEq yP_NOTEQUAL type_referenceBoth { $$ = new AstNeqT{$2, $1, $3}; }
// // IEEE: expr yP_MINUSGT expr (1800-2009)
// // Conflicts with constraint_expression:"expr yP_MINUSGT constraint_set"
// // To duplicating expr for constraints, just allow the more general form
// // Later Ast processing must ignore constraint terms where inappropriate
//UNSUP ~l~expr yP_MINUSGT constraint_set { $<fl>$ = $<fl>1; $$ = $1 + $2 + $3; }
//UNSUP remove line below
// // Full IEEE 1800-2023 18.7.2 "expr ->
// // constraint_set" is split: this rule handles
// // the bare-expression RHS as a boolean
// // (AstLogIf), constraint_expression has one
// // production per non-expression RHS shape.
| ~l~expr yP_MINUSGT ~r~expr { $$ = new AstLogIf{$2, $1, $3}; }
//
// // <= is special, as we need to disambiguate it with <= assignment
@ -7910,8 +7910,37 @@ constraint_expression<nodep>: // ==IEEE: constraint_expression
| yUNIQUE '{' range_list '}' ';'
{ $$ = new AstConstraintUnique{$1, $3}; }
// // IEEE: expr yP_MINUSGT constraint_set
// // Conflicts with expr:"expr yP_MINUSGT expr"; rule moved there
//
// // The bare-expression case "expr -> expr ;"
// // arrives via the general expr rule above
// // (AstLogIf) and matches "expr ';'". Each
// // production below covers one constraint_set
// // shape that is not a plain expression and
// // builds an outer AstConstraintIf wrapping the
// // statement V3Randomize already knows how to
// // lower (with disable-soft hoisted by the
// // ConstraintExprVisitor pre-pass).
| expr yP_MINUSGT '{' constraint_expressionList '}'
{ $$ = new AstConstraintIf{$2, $1, $4, nullptr}; }
| expr yP_MINUSGT yIF '(' expr ')' constraint_set %prec prLOWER_THAN_ELSE
{ $$ = new AstConstraintIf{$2, $1,
new AstConstraintIf{$3, $5, $7, nullptr}, nullptr}; }
| expr yP_MINUSGT yIF '(' expr ')' constraint_set yELSE constraint_set
{ $$ = new AstConstraintIf{$2, $1,
new AstConstraintIf{$3, $5, $7, $9}, nullptr}; }
| expr yP_MINUSGT yFOREACH '(' idClassSelForeach ')' constraint_set
{ $$ = new AstConstraintIf{$2, $1,
new AstConstraintForeach{$3, $5, $7}, nullptr}; }
| expr yP_MINUSGT yUNIQUE '{' range_list '}' ';'
{ $$ = new AstConstraintIf{$2, $1,
new AstConstraintUnique{$3, $5}, nullptr}; }
| expr yP_MINUSGT ySOFT expr ';'
{ AstConstraintExpr* const innerp = new AstConstraintExpr{$3, $4};
innerp->isSoft(true);
$$ = new AstConstraintIf{$2, $1, innerp, nullptr}; }
| expr yP_MINUSGT yDISABLE ySOFT constraint_primary ';'
{ AstConstraintExpr* const innerp = new AstConstraintExpr{$3, $5};
innerp->isDisableSoft(true);
$$ = new AstConstraintIf{$2, $1, innerp, nullptr}; }
| yIF '(' expr ')' constraint_set %prec prLOWER_THAN_ELSE
{ $$ = new AstConstraintIf{$1, $3, $5, nullptr}; }
| yIF '(' expr ')' constraint_set yELSE constraint_set
@ -7920,7 +7949,7 @@ constraint_expression<nodep>: // ==IEEE: constraint_expression
| yFOREACH '(' idClassSelForeach ')' constraint_set
{ $$ = new AstConstraintForeach{$1, $3, $5}; }
// // soft is 1800-2012
| yDISABLE ySOFT expr/*constraint_primary*/ ';'
| yDISABLE ySOFT constraint_primary ';'
{ AstConstraintExpr* const newp = new AstConstraintExpr{$1, $3};
newp->isDisableSoft(true);
$$ = newp; }

View File

@ -0,0 +1,5 @@
%Error: t/t_constraint_disable_soft_bad.v:15:25: syntax error, unexpected ';'
15 | disable soft (a + 1);
| ^
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: Exiting due to

View File

@ -0,0 +1,16 @@
#!/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('vlt')
test.lint(fails=True, expect_filename=test.golden_filename)
test.passes()

View File

@ -0,0 +1,23 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 PlanV GmbH
// SPDX-License-Identifier: CC0-1.0
class C;
rand bit [3:0] a;
rand bit [3:0] b;
// IEEE 1800-2023 18.5.13: the operand of 'disable soft' must be a
// constraint_primary (hierarchical identifier with optional select),
// not a bare expression such as (a + 1).
constraint c_bad {
disable soft (a + 1);
}
endclass
module t;
initial begin
$stop;
end
endmodule

View File

@ -0,0 +1,5 @@
%Error: t/t_constraint_implication_else_bad.v:15:32: syntax error, unexpected else
15 | (a == 0) -> { b == 4'h1; } else { b == 4'h2; }
| ^~~~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: Exiting due to

View File

@ -0,0 +1,16 @@
#!/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('linter')
test.lint(fails=True, expect_filename=test.golden_filename)
test.passes()

View File

@ -0,0 +1,23 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 PlanV GmbH
// SPDX-License-Identifier: CC0-1.0
class C;
rand bit [3:0] a;
rand bit [3:0] b;
// IEEE 1800-2023 18.7.2: implication operator -> takes one constraint_set
// on the RHS; it is single-armed (no else clause). Only the if (...) form
// accepts an optional else branch.
constraint c_bad {
(a == 0) -> { b == 4'h1; } else { b == 4'h2; }
}
endclass
module t;
initial begin
$stop;
end
endmodule

View File

@ -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()

View File

@ -0,0 +1,254 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 PlanV GmbH
// SPDX-License-Identifier: CC0-1.0
// verilog_format: off
`define stop $stop
`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
// verilog_format: on
typedef enum bit [1:0] { TXN_READ, TXN_WRITE } txn_e;
// Each constraint exercises one RHS shape allowed by IEEE 1800-2023 18.7.2
// (constraint_set on the right of the implication operator -> ). `mode`
// selects which constraint contributes; the others are vacuous.
class Forms;
rand bit [3:0] mode;
rand bit [3:0] a;
rand bit [3:0] b;
rand bit [3:0] c;
rand bit [31:0] address;
rand txn_e txn_type;
rand bit [7:0] arr [4];
rand bit [3:0] uarr [3];
// Bare expression (legacy form, supported pre-PR via expr->expr).
constraint c_expr {
(mode == 4'd0) -> b == 4'h9;
}
// Brace-block: the exact shape from issue #7300.
constraint c_brace_repro {
(mode == 4'd1) -> {
if (txn_type inside {TXN_READ}) address % (1 << 4) == 0;
}
}
// Brace-block with multiple statements.
constraint c_brace_multi {
(mode == 4'd2) -> {
address[0] == 1'b0;
address[31] == 1'b0;
}
}
// Bare if (without surrounding braces).
constraint c_if {
(mode == 4'd3) -> if (a == 4'h1) b == 4'h7;
}
// Bare if/else.
constraint c_if_else {
(mode == 4'd4) -> if (a == 4'h1) b == 4'ha;
else b == 4'hb;
}
// Bare foreach.
constraint c_foreach {
(mode == 4'd5) -> foreach (arr[i]) arr[i] < 8'h40;
}
// Bare unique (uses the static-array form V3Randomize supports today).
constraint c_unique {
(mode == 4'd6) -> unique { uarr };
}
// Bare soft.
constraint c_soft {
(mode == 4'd7) -> soft b == 4'hd;
}
// Nested implication inside a brace block.
constraint c_nested {
(mode == 4'd8) -> {
(a == 4'h0) -> { b == 4'h5; }
}
}
endclass
// Conditional `disable soft` is meta-level: V3Randomize hoists it into a
// runtime AstIf attached to the setup task so the directive only fires
// when its outer condition is true. When override_flag==0, the soft
// `x == 4'h5` wins; when override_flag==1, the implication fires the
// disable AND the override `x == 4'hc`, so x must be 4'hc.
class DisSoft;
bit override_flag;
rand bit [3:0] x;
constraint c_soft_x { soft x == 4'h5; }
constraint c_override {
(override_flag == 1'b1) -> disable soft x ;
(override_flag == 1'b1) -> x == 4'hc ;
}
endclass
// MemberSel target for `disable soft`. Cross-object reference (inner.y)
// parses as AstMemberSel; disable-soft must extract the variable name from
// that node shape too.
class Inner;
rand bit [3:0] y;
endclass
class DisSoftMember;
bit override_flag;
rand Inner inner;
constraint c_soft_y { soft inner.y == 4'h5; }
constraint c_override {
(override_flag == 1'b1) -> disable soft inner.y ;
(override_flag == 1'b1) -> inner.y == 4'hc ;
}
function new(); inner = new(); endfunction
endclass
// `disable soft` in BOTH then and else arms of a single if. Exercises the
// hoist-list concat path in the else branch (a then-arm hoist already
// exists when the else-arm hoist is appended). We only check that the
// hard constraint in each arm fires correctly under its `pick` condition;
// soft enforcement priority is not asserted (Verilator's soft solver is
// best-effort). The condition variable `pick` is non-rand so the setup
// task sees its current value before the solver runs.
class DisSoftBothArms;
bit [1:0] pick;
rand bit [3:0] a;
rand bit [3:0] b;
constraint c_soft_a { soft a == 4'h7; }
constraint c_soft_b { soft b == 4'h8; }
constraint c_split {
if (pick == 2'd0) { disable soft a; a == 4'h1; }
else { disable soft b; b == 4'h2; }
}
endclass
module t;
Forms obj;
DisSoft ds;
int ok;
initial begin
obj = new();
repeat (10) begin
ok = obj.randomize() with { mode == 4'd0; };
`checkd(ok, 1);
`checkh(obj.b, 4'h9);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd1; txn_type == TXN_READ; };
`checkd(ok, 1);
`checkh(obj.address[3:0], 4'h0);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd2; };
`checkd(ok, 1);
`checkh(obj.address[0], 1'b0);
`checkh(obj.address[31], 1'b0);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd3; a == 4'h1; };
`checkd(ok, 1);
`checkh(obj.b, 4'h7);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd4; a == 4'h1; };
`checkd(ok, 1);
`checkh(obj.b, 4'ha);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd4; a == 4'h2; };
`checkd(ok, 1);
`checkh(obj.b, 4'hb);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd5; };
`checkd(ok, 1);
foreach (obj.arr[i]) `checkh(obj.arr[i] < 8'h40, 1'b1);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd6; };
`checkd(ok, 1);
`checkh(obj.uarr[0] == obj.uarr[1], 1'b0);
`checkh(obj.uarr[0] == obj.uarr[2], 1'b0);
`checkh(obj.uarr[1] == obj.uarr[2], 1'b0);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd7; };
`checkd(ok, 1);
`checkh(obj.b, 4'hd);
end
repeat (10) begin
ok = obj.randomize() with { mode == 4'd8; a == 4'h0; };
`checkd(ok, 1);
`checkh(obj.b, 4'h5);
end
ds = new();
ds.override_flag = 1'b0;
repeat (10) begin
ok = ds.randomize();
`checkd(ok, 1);
`checkh(ds.x, 4'h5);
end
ds.override_flag = 1'b1;
repeat (10) begin
ok = ds.randomize();
`checkd(ok, 1);
`checkh(ds.x, 4'hc);
end
begin
automatic DisSoftMember dsm = new();
dsm.override_flag = 1'b0;
repeat (10) begin
ok = dsm.randomize();
`checkd(ok, 1);
`checkh(dsm.inner.y, 4'h5);
end
dsm.override_flag = 1'b1;
repeat (10) begin
ok = dsm.randomize();
`checkd(ok, 1);
`checkh(dsm.inner.y, 4'hc);
end
end
begin
automatic DisSoftBothArms dba = new();
// pick==0: hard a==1 fires (then arm); hoisted disable_soft(a) runs
dba.pick = 2'd0;
repeat (10) begin
ok = dba.randomize();
`checkd(ok, 1);
`checkh(dba.a, 4'h1);
end
// pick==1: hard b==2 fires (else arm); hoisted disable_soft(b) runs
dba.pick = 2'd1;
repeat (10) begin
ok = dba.randomize();
`checkd(ok, 1);
`checkh(dba.b, 4'h2);
end
end
$write("*-* All Finished *-*\n");
$finish;
end
endmodule