From a5b0a0d9dd3a19eea4469a74fb17970873901f27 Mon Sep 17 00:00:00 2001 From: Ryszard Rozak Date: Mon, 28 Jul 2025 16:14:03 +0200 Subject: [PATCH] Add support for `$countones` in constraints (#6144) (#6235) --- src/V3AstNodeExpr.h | 2 +- src/V3Randomize.cpp | 38 ++++++++++++++++- test_regress/t/t_constraint_countones.py | 21 ++++++++++ test_regress/t/t_constraint_countones.v | 53 ++++++++++++++++++++++++ test_regress/t/t_constraint_unsup.out | 5 +++ test_regress/t/t_constraint_unsup.py | 16 +++++++ test_regress/t/t_constraint_unsup.v | 19 +++++++++ 7 files changed, 151 insertions(+), 3 deletions(-) create mode 100755 test_regress/t/t_constraint_countones.py create mode 100644 test_regress/t/t_constraint_countones.v create mode 100644 test_regress/t/t_constraint_unsup.out create mode 100755 test_regress/t/t_constraint_unsup.py create mode 100644 test_regress/t/t_constraint_unsup.v diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 0047e2845..851f9e7f4 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -56,7 +56,7 @@ public: virtual string emitVerilog() = 0; /// Format string for verilog writing; see V3EmitV // For documentation on emitC format see EmitCFunc::emitOpName virtual string emitC() = 0; - virtual string emitSMT() const { V3ERROR_NA_RETURN(""); }; + virtual string emitSMT() const { return ""; }; virtual string emitSimpleOperator() { return ""; } // "" means not ok to use virtual bool emitCheckMaxWords() { return false; } // Check VL_MULS_MAX_WORDS virtual bool cleanOut() const = 0; // True if output has extra upper bits zero diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 30581654a..decadd40e 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -532,8 +532,10 @@ class ConstraintExprVisitor final : public VNVisitor { AstNodeExpr* thsp = nullptr) { // Replace incomputable (result-dependent) expression with SMT expression std::string smtExpr = nodep->emitSMT(); // Might need child width (AstExtend) - UASSERT_OBJ(smtExpr != "", nodep, - "Node needs randomization constraint, but no emitSMT: " << nodep); + if (smtExpr == "") { + nodep->v3warn(E_UNSUPPORTED, "Unsupported expression inside constraint"); + return; + } if (lhsp) lhsp = VN_AS(iterateSubtreeReturnEdits(lhsp->backp() ? lhsp->unlinkFrBack() : lhsp), @@ -718,6 +720,38 @@ class ConstraintExprVisitor final : public VNVisitor { initTaskp->addStmtsp(methodp->makeStmt()); } } + void visit(AstCountOnes* nodep) override { + // Convert it to (x & 1) + ((x & 2) >> 1) + ((x & 4) >> 2) + ... + FileLine* const fl = nodep->fileline(); + AstNodeExpr* const argp = nodep->lhsp()->unlinkFrBack(); + V3Number numOne{nodep, argp->width(), 1}; + AstNodeExpr* sump = new AstAnd{fl, argp, new AstConst{fl, numOne}}; + sump->user1(true); + for (int i = 1; i < argp->width(); i++) { + V3Number numBitMask{nodep, argp->width(), 0}; + numBitMask.setBit(i, 1); + AstAnd* const andp + = new AstAnd{fl, argp->cloneTreePure(false), new AstConst{fl, numBitMask}}; + andp->user1(true); + AstShiftR* const shiftp = new AstShiftR{ + fl, andp, new AstConst{fl, AstConst::WidthedValue{}, argp->width(), (uint32_t)i}}; + shiftp->user1(true); + shiftp->dtypeFrom(nodep); + sump = new AstAdd{nodep->fileline(), sump, shiftp}; + sump->user1(true); + } + // Restore the original width + if (nodep->width() > sump->width()) { + sump = new AstExtend{fl, sump, nodep->width()}; + sump->user1(true); + } else if (nodep->width() < sump->width()) { + sump = new AstSel{fl, sump, 0, nodep->width()}; + sump->user1(true); + } + nodep->replaceWith(sump); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + iterate(sump); + } void visit(AstNodeBiop* nodep) override { if (editFormat(nodep)) return; editSMT(nodep, nodep->lhsp(), nodep->rhsp()); diff --git a/test_regress/t/t_constraint_countones.py b/test_regress/t/t_constraint_countones.py new file mode 100755 index 000000000..a2b131082 --- /dev/null +++ b/test_regress/t/t_constraint_countones.py @@ -0,0 +1,21 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2024 by Wilson Snyder. 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-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_constraint_countones.v b/test_regress/t/t_constraint_countones.v new file mode 100644 index 000000000..86bf60772 --- /dev/null +++ b/test_regress/t/t_constraint_countones.v @@ -0,0 +1,53 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2025 by Antmicro. +// SPDX-License-Identifier: CC0-1.0 + +`define check_rand(cl, field, cond) \ +begin \ + longint prev_result; \ + int ok = 0; \ + if (!bit'(cl.randomize())) $stop; \ + prev_result = longint'(field); \ + if (!(cond)) $stop; \ + repeat(9) begin \ + longint result; \ + if (!bit'(cl.randomize())) $stop; \ + result = longint'(field); \ + if (!(cond)) $stop; \ + if (result != prev_result) ok = 1; \ + prev_result = result; \ + end \ + if (ok != 1) $stop; \ +end + +class Rand1; + rand bit [4:0] x; + constraint c {$countones(x) == 1;} +endclass + +class Rand2; + rand bit [5:0] x; + rand bit [2:0] y; + constraint c {10'b1 + 10'($countones(x + 6'(y))) == 3;} +endclass + +class Rand3; + rand bit [32:0] x; + constraint c {$countones(x) == 1;} +endclass + +module t ( /*AUTOARG*/); + Rand1 r1 = new; + Rand2 r2 = new; + Rand3 r3 = new; + initial begin + `check_rand(r1, r1.x, $countones(r1.x) == 1); + `check_rand(r2, r2.x, 10'b1 + 10'($countones(r2.x + 6'(r2.y))) == 3); + `check_rand(r3, r3.x, $countones(r3.x) == 1); + + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule diff --git a/test_regress/t/t_constraint_unsup.out b/test_regress/t/t_constraint_unsup.out new file mode 100644 index 000000000..2708313a4 --- /dev/null +++ b/test_regress/t/t_constraint_unsup.out @@ -0,0 +1,5 @@ +%Error-UNSUPPORTED: t/t_constraint_unsup.v:9:22: Unsupported expression inside constraint + 9 | constraint cons { $onehot(m_one) == 1; } + | ^~~~~~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_constraint_unsup.py b/test_regress/t/t_constraint_unsup.py new file mode 100755 index 000000000..6585af685 --- /dev/null +++ b/test_regress/t/t_constraint_unsup.py @@ -0,0 +1,16 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2024 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('vlt') + +test.lint(fails=test.vlt_all, expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_constraint_unsup.v b/test_regress/t/t_constraint_unsup.v new file mode 100644 index 000000000..8369075bb --- /dev/null +++ b/test_regress/t/t_constraint_unsup.v @@ -0,0 +1,19 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2025 by Antmicro. +// SPDX-License-Identifier: CC0-1.0 + +class Packet; + rand int m_one; + constraint cons { $onehot(m_one) == 1; } +endclass + +module t; + Packet p; + + initial begin + p = new; + void'(p.randomize()); + end +endmodule