diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index b26f920fd..169a3247b 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -1600,6 +1600,25 @@ class ConstraintExprVisitor final : public VNVisitor { void visit(AstPowSS* nodep) override { handlePow(nodep); } void visit(AstPowSU* nodep) override { handlePow(nodep); } void visit(AstPowUS* nodep) override { handlePow(nodep); } + // SMT-LIB2 shift operations (bvshl/bvlshr/bvashr) require both operands + // to have the same bitvector width. Zero-extend the RHS if narrower. + void handleShift(AstNodeBiop* nodep) { + if (editFormat(nodep)) return; + const int lhsWidth = nodep->lhsp()->width(); + const int rhsWidth = nodep->rhsp()->width(); + if (rhsWidth < lhsWidth) { + FileLine* const fl = nodep->fileline(); + AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack(); + const bool rhsDependent = rhsp->user1(); + AstExtend* const extendp = new AstExtend{fl, rhsp, lhsWidth}; + extendp->user1(rhsDependent); + nodep->rhsp(extendp); + } + editSMT(nodep, nodep->lhsp(), nodep->rhsp()); + } + void visit(AstShiftL* nodep) override { handleShift(nodep); } + void visit(AstShiftR* nodep) override { handleShift(nodep); } + void visit(AstShiftRS* nodep) override { handleShift(nodep); } void visit(AstNodeBiop* nodep) override { if (editFormat(nodep)) return; editSMT(nodep, nodep->lhsp(), nodep->rhsp()); diff --git a/test_regress/t/t_constraint_shift_width.py b/test_regress/t/t_constraint_shift_width.py new file mode 100755 index 000000000..0b0c140af --- /dev/null +++ b/test_regress/t/t_constraint_shift_width.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(verilator_flags2=["--timing"], ) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_constraint_shift_width.v b/test_regress/t/t_constraint_shift_width.v new file mode 100644 index 000000000..142acf818 --- /dev/null +++ b/test_regress/t/t_constraint_shift_width.v @@ -0,0 +1,122 @@ +// 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 AlignedPacket; + localparam int ADDRW = 37; + localparam int SIZEW = 4; + + typedef logic [ADDRW-1:0] address_t; + typedef logic [SIZEW-1:0] size_t; + + rand address_t address; + rand size_t size; + + // Constraint with mixed-width shift: address is 37-bit, size is 4-bit + // The expression (1 << size) involves a width mismatch that must be + // handled by zero-extending the shift RHS to match LHS width. + constraint c_aligned { + address % (1 << size) == 0; + } +endclass + +class ConstShiftPacket; + localparam int ADDRW = 37; + + typedef logic [ADDRW-1:0] address_t; + + rand address_t address; + + // Constraint with constant shift amount (different width from address) + constraint c_aligned { + address % (1 << 10) == 0; + } +endclass + +class ImplicationShift; + localparam int ADDRW = 37; + localparam int SIZEW = 4; + + typedef logic [ADDRW-1:0] address_t; + typedef logic [SIZEW-1:0] size_t; + typedef enum { + TXN_READ, TXN_WRITE, TXN_IDLE + } txn_type_t; + + rand txn_type_t txn_type; + rand size_t size; + rand address_t address; + + // Implication with mixed-width shift in consequent + constraint c_addr { + txn_type inside {TXN_READ, TXN_WRITE} -> address % (1 << size) == 0; + } +endclass + +module t; + AlignedPacket pkt1; + ConstShiftPacket pkt2; + ImplicationShift pkt3; + int ok; + + initial begin + // Test 1: Variable shift amount with mixed widths + pkt1 = new; + pkt1.size = 6; + ok = pkt1.randomize() with { size == 6; }; + if (ok != 1) begin + $display("ERROR: Test 1 randomize failed"); + $stop; + end + // address must be aligned to 1<<6 = 64 + if (pkt1.address % 64 != 0) begin + $display("ERROR: Test 1 alignment check failed: address=0x%0h", pkt1.address); + $stop; + end + + // Test 2: Unconstrained randomize (variable shift) + pkt1 = new; + ok = pkt1.randomize(); + if (ok != 1) begin + $display("ERROR: Test 2 randomize failed"); + $stop; + end + // address must be aligned to 1<