Support 2**n expressions in constraint randomization (#7422)

This commit is contained in:
Yilou Wang 2026-04-14 13:17:53 +02:00 committed by GitHub
parent 2770e649ba
commit 9eb2ba4c54
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
6 changed files with 162 additions and 0 deletions

View File

@ -1629,6 +1629,42 @@ class ConstraintExprVisitor final : public VNVisitor {
nodep->replaceWith(powerp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
iterate(powerp);
} else if (const AstConst* const basep = VN_CAST(nodep->lhsp(), Const)) {
if (basep->num().toUInt() == 2) {
// Non-constant exponent, base == 2: transform to shift-based SMT expression.
// AstPow/AstPowSU (unsigned exponent): 2**n -> 1<<n
// AstPowSS/AstPowUS (signed exponent): 2**n -> n>=0 ? 1<<n : 0
// IEEE 1800-2023 ss11.4.3: integer base with negative exponent gives 0,
// which ShiftL cannot represent; use SMT ite (AstCond -> bvsge + bvshl).
FileLine* const fl = nodep->fileline();
AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack();
const int width = nodep->width();
const bool rhsDependent = rhsp->user1();
AstConst* const onep = new AstConst{fl, AstConst::WidthedValue{}, width, 1};
AstShiftL* const shiftp = new AstShiftL{fl, onep, rhsp, width};
shiftp->dtypeFrom(nodep);
shiftp->user1(rhsDependent);
AstNodeExpr* resultp = shiftp;
if (VN_IS(nodep, PowSS) || VN_IS(nodep, PowUS)) {
// Signed exponent: guard 1<<n with n>=0 check
AstNodeExpr* const nClonep = rhsp->cloneTreePure(false);
nClonep->user1(rhsDependent);
AstConst* const zeroNp
= new AstConst{fl, AstConst::WidthedValue{}, rhsp->width(), 0};
AstGteS* const condp = new AstGteS{fl, nClonep, zeroNp};
condp->user1(rhsDependent);
AstConst* const zeroRp = new AstConst{fl, AstConst::WidthedValue{}, width, 0};
resultp = new AstCond{fl, condp, shiftp, zeroRp};
resultp->dtypeFrom(nodep);
resultp->user1(nodep->user1());
}
nodep->replaceWith(resultp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
iterate(resultp);
} else {
nodep->v3warn(CONSTRAINTIGN,
"Unsupported: Power (**) expression with non-2 base in constraint");
}
} else {
nodep->v3warn(
CONSTRAINTIGN,

View File

@ -0,0 +1,6 @@
%Warning-CONSTRAINTIGN: t/t_constraint_non_base2_pow_unsup.v:12:25: Unsupported: Power (**) expression with non-2 base in constraint
12 | constraint c { x == 3 ** n; }
| ^~
... 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.
%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,22 @@
// 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
// Power (**) with constant non-2 base and non-constant exponent is unsupported.
// Only base 2 can be lowered to SMT via left-shift; other bases have no SMT encoding.
class C;
rand int unsigned n;
rand int unsigned x;
constraint c { x == 3 ** n; }
endclass
module t;
C obj;
initial begin
obj = new;
void'(obj.randomize());
$finish;
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,61 @@
// 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
// AstPow (unsigned**unsigned): 2**n -> 1<<n directly
class UnsignedPow2;
rand bit [3:0] n;
rand bit [15:0] result;
constraint c { n inside {[0:7]}; result == 16'(2**n); }
function void check();
if (result !== (16'h1 << n)) begin
$display("FAIL UnsignedPow2: result=%0d expected 2**%0d=%0d", result, n, 16'h1 << n);
$stop;
end
endfunction
endclass
// AstPowUS (unsigned**signed): 2**n -> n>=0 ? 1<<n : 0
class SignedExpPow2;
rand int signed n;
rand bit [15:0] result;
constraint c { n inside {[-2:7]}; result == 16'(2**n); }
function void check();
bit [15:0] expected;
expected = (n >= 0) ? (16'h1 << n) : 16'h0;
if (result !== expected) begin
$display("FAIL SignedExpPow2: n=%0d result=%0d expected=%0d", n, result, expected);
$stop;
end
endfunction
endclass
module t;
UnsignedPow2 u;
SignedExpPow2 s;
initial begin
u = new;
repeat (20) begin
if (u.randomize() == 0) begin
$display("FAIL: UnsignedPow2.randomize() returned 0");
$stop;
end
u.check();
end
s = new;
repeat (30) begin
if (s.randomize() == 0) begin
$display("FAIL: SignedExpPow2.randomize() returned 0");
$stop;
end
s.check();
end
$write("*-* All Finished *-*\n");
$finish;
end
endmodule