luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support detailed failure info for constraint violations (#6617) (#6883) 

* logging for the unsatisfied constraints

* Apply 'make format'

* fix teh quote error in the array indexing

* Apply 'make format'

* Len change for the hash for randomity when named assertion is used

* seperate name assertion and satisfied case

* Apply 'make format'

* simply comments and display info

* refine code and fix protect case

* format

* update display in test and .out file

* add an enable flag and warning type, add a protect_id version test and update out files

* Apply 'make format'

* simplify some comments

* update out file, ready to be merged.

* update .py file to set the hash key solid

* rename and reformate the warning message to follow the verilator style

* add a nowarn test

* Apply 'make format'

* ordering

---------

Co-authored-by: Udaya Raj Subedi <075bei047.udaya@pcampus.edu.np>
Co-authored-by: github action <action@example.com>
This commit is contained in:
Yilou Wang 2026-01-12 15:53:49 +01:00 committed by GitHub
parent 703c82cb3d
commit 31f8be0b85
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
17 changed files with 401 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
bin/verilator
View File

@ -576,6 +576,7 @@ description of these arguments.
+verilator+seed+<value> Set random seed
+verilator+V Show verbose version and config
+verilator+version Show version and exit
+verilator+wno+unsatconstr+<value> Disable constraint warnings
=head1 DISTRIBUTION

8
docs/guide/exe_sim.rst
View File

@ -123,3 +123,11 @@ Options:
.. option:: +verilator+version
Displays program version and exits.
.. option:: +verilator+wno+unsatconstr+<value>
Disable unsatisfied constraint warnings at simulation runtime. When set to
1, warnings about unsatisfied constraints during ``randomize()`` calls will
not be displayed. Defaults to 0 (warnings enabled). This can also be
controlled via the C++ API using
``Verilated::threadContextp()->warnUnsatConstr(false)``.

14
docs/guide/warnings.rst
View File

@ -2273,6 +2273,20 @@ List Of Warnings
unpacked struct/array inside a packed struct/array.
.. option:: UNSATCONSTR
Warns that a ``randomize()`` call failed because one or more constraints
could not be satisfied. This warning is issued at simulation runtime when
the SMT solver determines that the combination of constraints is
unsatisfiable.
Each unsatisfied constraint is reported with its source location to help
identify conflicting constraints.
This warning can be disabled by setting the runtime option
``+verilator+wno+unsatconstr+1`` or by calling
``Verilated::threadContextp()->warnUnsatConstr(false)`` in C++.
.. option:: UNSIGNED
.. TODO better example

2
include/verilated.cpp
View File

@ -3013,6 +3013,8 @@ void VerilatedContextImp::commandArgVl(const std::string& arg) {
quiet(true);
} else if (commandArgVlUint64(arg, "+verilator+rand+reset+", u64, 0, 2)) {
randReset(static_cast<int>(u64));
} else if (commandArgVlUint64(arg, "+verilator+wno+unsatconstr+", u64, 0, 1)) {
warnUnsatConstr(u64 == 0); // wno means disable, so invert
} else if (commandArgVlUint64(arg, "+verilator+seed+", u64, 1,
std::numeric_limits<int>::max())) {
randSeed(static_cast<int>(u64));

4
include/verilated.h
View File

@ -414,6 +414,7 @@ protected:
std::string m_profExecFilename; // +prof+exec+file filename
std::string m_profVltFilename; // +prof+vlt filename
std::string m_solverProgram; // SMT solver program
bool m_warnUnsatConstr = true; // Warn on unsatisfied constraints
VlOs::DeltaCpuTime m_cpuTimeStart{false}; // CPU time, starts when create first model
VlOs::DeltaWallTime m_wallTimeStart{false}; // Wall time, starts when create first model
std::vector<traceBaseModelCb_t> m_traceBaseModelCbs; // Callbacks to traceRegisterModel
@ -653,6 +654,9 @@ public:
// Internal: SMT solver program
std::string solverProgram() const VL_MT_SAFE;
void solverProgram(const std::string& flag) VL_MT_SAFE;
// Internal: Control display of unsatisfied constraints
bool warnUnsatConstr() const VL_MT_SAFE { return m_ns.m_warnUnsatConstr; }
void warnUnsatConstr(bool flag) VL_MT_SAFE { m_ns.m_warnUnsatConstr = flag; }
// Internal: Find scope
const VerilatedScope* scopeFind(const char* namep) const VL_MT_SAFE;

96
include/verilated_random.cpp
View File

@ -389,8 +389,30 @@ bool VlRandomizer::next(VlRNG& rngr) {
}
os << "(check-sat)\n";
bool sat = parseSolution(os);
bool sat = parseSolution(os, true);
if (!sat) {
// If unsat, use named assertions to get unsat-core
os << "(reset)\n";
os << "(set-option :produce-unsat-cores true)\n";
os << "(set-logic QF_ABV)\n";
os << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n";
os << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n";
for (const auto& var : m_vars) {
if (var.second->dimension() > 0) {
auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars);
var.second->setArrayInfo(arrVarsp);
}
os << "(declare-fun " << var.first << " () ";
var.second->emitType(os);
os << ")\n";
}
int j = 0;
for (const std::string& constraint : m_constraints) {
os << "(assert (! (= #b1 " << constraint << ") :named cons" << j << "))\n";
j++;
}
os << "(check-sat)\n";
sat = parseSolution(os, true);
os << "(reset)\n";
return false;
}
@ -399,18 +421,67 @@ bool VlRandomizer::next(VlRNG& rngr) {
randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN);
os << ")\n";
os << "\n(check-sat)\n";
sat = parseSolution(os);
sat = parseSolution(os, false);
}
os << "(reset)\n";
return true;
}
bool VlRandomizer::parseSolution(std::iostream& os) {
bool VlRandomizer::parseSolution(std::iostream& os, bool log) {
std::string sat;
do { std::getline(os, sat); } while (sat == "");
if (sat == "unsat") return false;
if (sat == "unsat") {
if (!log) return false;
os << "(get-unsat-core) \n";
sat.clear();
std::getline(os, sat);
std::vector<int> numbers;
std::string currentNum;
for (char c : sat) {
if (std::isdigit(c)) {
currentNum += c;
numbers.push_back(std::stoi(currentNum));
currentNum.clear();
}
}
if (Verilated::threadContextp()->warnUnsatConstr()) {
for (int n : numbers) {
if (n < m_constraints_line.size()) {
const std::string& constraint_info = m_constraints_line[n];
// Parse "filename:linenum source" format
size_t colon_pos = constraint_info.find(':');
if (colon_pos != std::string::npos) {
std::string filename = constraint_info.substr(0, colon_pos);
size_t space_pos = constraint_info.find(" ", colon_pos);
std::string linenum_str;
std::string source;
if (space_pos != std::string::npos) {
linenum_str
= constraint_info.substr(colon_pos + 1, space_pos - colon_pos - 1);
source = constraint_info.substr(space_pos + 3);
} else {
linenum_str = constraint_info.substr(colon_pos + 1);
}
const int linenum = std::stoi(linenum_str);
std::string msg = "UNSATCONSTR: Unsatisfied constraint";
if (!source.empty()) {
// Trim leading whitespace and add quotes
size_t start = source.find_first_not_of(" \t");
if (start != std::string::npos) {
msg += ": '" + source.substr(start) + "'";
}
}
VL_WARN_MT(filename.c_str(), linenum, "", msg.c_str());
} else {
VL_PRINTF("%%Warning-UNSATCONSTR: Unsatisfied constraint: %s\n",
constraint_info.c_str());
}
}
}
}
return false;
}
if (sat != "sat") {
std::stringstream msg;
msg << "Internal: Solver error: " << sat;
@ -501,12 +572,25 @@ bool VlRandomizer::parseSolution(std::iostream& os) {
return true;
}
void VlRandomizer::hard(std::string&& constraint) {
void VlRandomizer::hard(std::string&& constraint, const char* filename, int linenum,
const char* source) {
m_constraints.emplace_back(std::move(constraint));
// Format constraint location: "filename:linenum source"
if (filename[0] != '\0' || source[0] != '\0') {
std::string line;
if (filename[0] != '\0') {
line = std::string(filename) + ":" + std::to_string(linenum);
if (source[0] != '\0') line += " " + std::string(source);
} else {
line = source;
}
m_constraints_line.emplace_back(std::move(line));
}
}
void VlRandomizer::clearConstraints() {
m_constraints.clear();
m_constraints_line.clear();
// Keep m_vars for class member randomization
}

7
include/verilated_random.h
View File

@ -200,6 +200,8 @@ public:
class VlRandomizer VL_NOT_FINAL {
// MEMBERS
std::vector<std::string> m_constraints; // Solver-dependent constraints
std::vector<std::string>
m_constraints_line; // fileline content of the constraint for unsat constraints
std::map<std::string, std::shared_ptr<const VlRandomVar>> m_vars; // Solver-dependent
// variables
ArrayInfoMap m_arr_vars; // Tracks each element in array structures for iteration
@ -208,7 +210,7 @@ class VlRandomizer VL_NOT_FINAL {
// PRIVATE METHODS
void randomConstraint(std::ostream& os, VlRNG& rngr, int bits);
bool parseSolution(std::iostream& file);
bool parseSolution(std::iostream& file, bool log = false);
public:
// CONSTRUCTORS
@ -569,7 +571,8 @@ public:
+ std::to_string(idx);
}
void hard(std::string&& constraint);
void hard(std::string&& constraint, const char* filename = "", int linenum = 0,
const char* source = "");
void clearConstraints();
void clearAll(); // Clear both constraints and variables
void set_randmode(const VlQueue<CData>& randmode) { m_randmodep = &randmode; }

25
src/V3EmitCFunc.h
View File

@ -720,15 +720,40 @@ public:
putns(nodep, nodep->name());
puts("(");
bool comma = false;
int argNum = 0;
for (AstNode* subnodep = nodep->pinsp(); subnodep; subnodep = subnodep->nextp()) {
if (comma) puts(", ");
// handle wide arguments to the queues
if (VN_IS(nodep->fromp()->dtypep(), QueueDType) && subnodep->dtypep()->isWide()) {
emitCvtWideArray(subnodep, nodep->fromp());
} else if (nodep->method() == VCMethod::RANDOMIZER_HARD && argNum == 1) {
// For RANDOMIZER_HARD's filename argument (2nd arg after constraint),
// apply protect() similar to VL_STOP to handle --protected flag
if (const AstCExpr* const cexprp = VN_CAST(subnodep, CExpr)) {
// Extract filename from the CExpr (which contains "filename")
std::string filename;
for (const AstNode* textnodep = cexprp->nodesp(); textnodep;
textnodep = textnodep->nextp()) {
if (const AstText* const textp = VN_CAST(textnodep, Text)) {
filename = textp->text();
break;
}
}
// Remove surrounding quotes if present
if (filename.size() >= 2 && filename.front() == '"'
&& filename.back() == '"') {
filename = filename.substr(1, filename.size() - 2);
}
// Emit with protect()
putsQuoted(protect(filename));
} else {
iterateConst(subnodep);
}
} else {
iterateConst(subnodep);
}
comma = true;
argNum++;
}
puts(")");
}

9
src/V3Error.h
View File

@ -169,6 +169,7 @@ public:
UNOPTFLAT, // Unoptimizable block after flattening
UNOPTTHREADS, // Thread partitioner unable to fill all requested threads
UNPACKED, // Unsupported unpacked
UNSATCONSTR, // Unsatisfied constraint
UNSIGNED, // Comparison is constant due to unsigned arithmetic
UNUSED, // Unused genvar, parameter or signal message (Backward Compatibility)
UNUSEDGENVAR, // No receivers for genvar
@ -231,10 +232,10 @@ public:
"REDEFMACRO", "RISEFALLDLY", "SELRANGE", "SHORTREAL", "SIDEEFFECT", "SPECIFYIGN",
"SPLITVAR", "STATICVAR", "STMTDLY", "SUPERNFIRST", "SYMRSVDWORD", "SYNCASYNCNET",
"TICKCOUNT", "TIMESCALEMOD", "UNDRIVEN", "UNOPT", "UNOPTFLAT", "UNOPTTHREADS",
"UNPACKED", "UNSIGNED", "UNUSED", "UNUSEDGENVAR", "UNUSEDLOOP", "UNUSEDPARAM",
"UNUSEDSIGNAL", "USERERROR", "USERFATAL", "USERINFO", "USERWARN", "VARHIDDEN",
"WAITCONST", "WIDTH", "WIDTHCONCAT", "WIDTHEXPAND", "WIDTHTRUNC", "WIDTHXZEXPAND",
"ZERODLY", "ZEROREPL", " MAX"};
"UNPACKED", "UNSATCONSTR", "UNSIGNED", "UNUSED", "UNUSEDGENVAR", "UNUSEDLOOP",
"UNUSEDPARAM", "UNUSEDSIGNAL", "USERERROR", "USERFATAL", "USERINFO", "USERWARN",
"VARHIDDEN", "WAITCONST", "WIDTH", "WIDTHCONCAT", "WIDTHEXPAND", "WIDTHTRUNC",
"WIDTHXZEXPAND", "ZERODLY", "ZEROREPL", " MAX"};
return names[m_e];
}
// Warnings that default to off

18
src/V3Randomize.cpp
View File

@ -1353,6 +1353,24 @@ class ConstraintExprVisitor final : public VNVisitor {
VAccess::READWRITE},
VCMethod::RANDOMIZER_HARD, nodep->exprp()->unlinkFrBack()};
callp->dtypeSetVoid();
// Pass filename, lineno, and source as separate arguments
// This allows EmitC to call protect() on filename, similar to VL_STOP
// Add filename parameter
callp->addPinsp(
new AstCExpr{nodep->fileline(), "\"" + nodep->fileline()->filename() + "\""});
// Add line number parameter
callp->addPinsp(new AstCExpr{nodep->fileline(), cvtToStr(nodep->fileline()->lineno())});
// Add source text parameter (empty if --protect-ids to avoid source leakage)
std::string prettyText;
if (!v3Global.opt.protectIds()) {
prettyText = nodep->fileline()->prettySource();
size_t pos = 0;
while ((pos = prettyText.find('"', pos)) != std::string::npos) {
prettyText.insert(pos, "\\");
pos += std::strlen("\\\"");
}
}
callp->addPinsp(new AstCExpr{nodep->fileline(), "\"" + prettyText + "\""});
nodep->replaceWith(callp->makeStmt());
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}

31
test_regress/t/t_constraint_unsat.out Normal file
View File

@ -0,0 +1,31 @@
=== Test 1: Valid constraints ===
=== Test 2: addr out of range ===
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:12: Unsatisfied constraint: 'constraint data_range { data > 10 && data < 200; }'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:12: Unsatisfied constraint: 'constraint data_range { data > 10 && data < 200; }'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:11: Unsatisfied constraint: 'constraint addr_range { addr < 127; }'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin'
Randomization failed.
=== Test 3: data out of range (too small) ===
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:12: Unsatisfied constraint: 'constraint data_range { data > 10 && data < 200; }'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin'
Randomization failed.
=== Test 4: data out of range (too large) ===
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:12: Unsatisfied constraint: 'constraint data_range { data > 10 && data < 200; }'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin'
Randomization failed.
=== Test 5: Both constraints violated ===
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:11: Unsatisfied constraint: 'constraint addr_range { addr < 127; }'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin'
Randomization failed.
=== Test 6: Conflicting constraints (x > 100 && x < 50) ===
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:26: Unsatisfied constraint: 'constraint c1 { x > 100; }'
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:27: Unsatisfied constraint: 'constraint c2 { x < 50; }'
Expected failure: conflicting constraints detected
*-* All Finished *-*

23
test_regress/t/t_constraint_unsat.py Executable file
View File

@ -0,0 +1,23 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2026 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 default behavior (warnings enabled)
# To disable warnings: use +verilator+wno+unsatconstr+1
test.execute(expect_filename=test.golden_filename)
test.passes()

76
test_regress/t/t_constraint_unsat.v Executable file
View File

@ -0,0 +1,76 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2026 by PlanV GmbH.
// SPDX-License-Identifier: CC0-1.0
class Packet;
rand bit [7:0] addr;
rand bit [7:0] data;
constraint addr_range { addr < 127; }
constraint data_range { data > 10 && data < 200; }
function void check(bit [7:0] a, bit [7:0] d);
/* verilator lint_off WIDTHTRUNC */
if (!randomize() with { addr == a; data == d; }) begin
/* verilator lint_on WIDTHTRUNC */
$display("Randomization failed.");
end
endfunction
endclass
class TestConflict;
rand bit [7:0] x;
constraint c1 { x > 100; }
constraint c2 { x < 50; }
function bit try_randomize();
/* verilator lint_off WIDTHTRUNC */
return randomize();
/* verilator lint_on WIDTHTRUNC */
endfunction
endclass
module t_constraint_unsat;
initial begin
Packet pkt;
TestConflict tc;
pkt = new;
// Test 1: Valid randomization
$display("\n=== Test 1: Valid constraints ===");
pkt.check(50, 100);
// Test 2: addr out of range
$display("\n=== Test 2: addr out of range ===");
pkt.check(128, 18);
// Test 3: data out of range (too small)
$display("\n=== Test 3: data out of range (too small) ===");
pkt.check(100, 5);
// Test 4: data out of range (too large)
$display("\n=== Test 4: data out of range (too large) ===");
pkt.check(100, 250);
// Test 5: Both constraints violated
$display("\n=== Test 5: Both constraints violated ===");
pkt.check(200, 5);
// Test 6: Conflicting constraints
$display("\n=== Test 6: Conflicting constraints (x > 100 && x < 50) ===");
tc = new;
if (!tc.try_randomize()) begin
$display("Expected failure: conflicting constraints detected");
end else begin
$display("ERROR: Should have failed with conflicting constraints");
$stop;
end
$write("*-* All Finished *-*\n");
$finish;
end
endmodule

18
test_regress/t/t_constraint_unsat_nowarn.out Normal file
View File

@ -0,0 +1,18 @@
=== Test 1: Valid constraints ===
=== Test 2: addr out of range ===
Randomization failed.
=== Test 3: data out of range (too small) ===
Randomization failed.
=== Test 4: data out of range (too large) ===
Randomization failed.
=== Test 5: Both constraints violated ===
Randomization failed.
=== Test 6: Conflicting constraints (x > 100 && x < 50) ===
Expected failure: conflicting constraints detected
*-* All Finished *-*

23
test_regress/t/t_constraint_unsat_nowarn.py Executable file
View File

@ -0,0 +1,23 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2026 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')
test.top_filename = "t/t_constraint_unsat.v"
if not test.have_solver:
test.skip("No constraint solver installed")
test.compile()
# Test with warnings disabled via +verilator+wno+unsatconstr+1
test.execute(all_run_flags=['+verilator+wno+unsatconstr+1'], expect_filename=test.golden_filename)
test.passes()

31
test_regress/t/t_constraint_unsat_protect_ids.out Normal file
View File

@ -0,0 +1,31 @@
=== Test 1: Valid constraints ===
=== Test 2: addr out of range ===
%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:12: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:12: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:11: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint
Randomization failed.
=== Test 3: data out of range (too small) ===
%Warning-UNSATCONSTR: PSTByA:12: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint
Randomization failed.
=== Test 4: data out of range (too large) ===
%Warning-UNSATCONSTR: PSTByA:12: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint
Randomization failed.
=== Test 5: Both constraints violated ===
%Warning-UNSATCONSTR: PSTByA:11: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint
Randomization failed.
=== Test 6: Conflicting constraints (x > 100 && x < 50) ===
%Warning-UNSATCONSTR: PSTByA:26: Unsatisfied constraint
%Warning-UNSATCONSTR: PSTByA:27: Unsatisfied constraint
Expected failure: conflicting constraints detected
*-* All Finished *-*

27
test_regress/t/t_constraint_unsat_protect_ids.py Executable file
View File

@ -0,0 +1,27 @@
#!/usr/bin/env python3
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2026 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')
test.top_filename = "t/t_constraint_unsat.v"
if not test.have_solver:
test.skip("No constraint solver installed")
# This test makes randomly named .cpp/.h files, which tend to collect, so remove them first
for filename in (glob.glob(test.obj_dir + "/*_PS*.cpp") + glob.glob(test.obj_dir + "/*_PS*.h") +
glob.glob(test.obj_dir + "/*.d")):
test.unlink_ok(filename)
test.compile(verilator_flags2=["--protect-ids", "--protect-key SECRET_KEY"])
test.execute(expect_filename=test.golden_filename)
test.passes()