Add support for `$countones` in constraints (#6144) (#6235)

This commit is contained in:
Ryszard Rozak 2025-07-28 16:14:03 +02:00 committed by GitHub
parent 0bd291e6cd
commit a5b0a0d9dd
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
7 changed files with 151 additions and 3 deletions

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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