diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 90904b61c..a8d45dd2e 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -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>=0 ? 1< 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<=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, diff --git a/test_regress/t/t_constraint_non_base2_pow_unsup.out b/test_regress/t/t_constraint_non_base2_pow_unsup.out new file mode 100644 index 000000000..4308d57fc --- /dev/null +++ b/test_regress/t/t_constraint_non_base2_pow_unsup.out @@ -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 diff --git a/test_regress/t/t_constraint_non_base2_pow_unsup.py b/test_regress/t/t_constraint_non_base2_pow_unsup.py new file mode 100755 index 000000000..344a4e20a --- /dev/null +++ b/test_regress/t/t_constraint_non_base2_pow_unsup.py @@ -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() diff --git a/test_regress/t/t_constraint_non_base2_pow_unsup.v b/test_regress/t/t_constraint_non_base2_pow_unsup.v new file mode 100644 index 000000000..118365def --- /dev/null +++ b/test_regress/t/t_constraint_non_base2_pow_unsup.v @@ -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 diff --git a/test_regress/t/t_randomize_pow2.py b/test_regress/t/t_randomize_pow2.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_randomize_pow2.py @@ -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() diff --git a/test_regress/t/t_randomize_pow2.v b/test_regress/t/t_randomize_pow2.v new file mode 100644 index 000000000..73be88d2b --- /dev/null +++ b/test_regress/t/t_randomize_pow2.v @@ -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>=0 ? 1<= 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