From 31f8be0b85c891ee089ecc7b9dd3ddd58323aef9 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Mon, 12 Jan 2026 15:53:49 +0100 Subject: [PATCH] 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 --- bin/verilator | 1 + docs/guide/exe_sim.rst | 8 ++ docs/guide/warnings.rst | 14 +++ include/verilated.cpp | 2 + include/verilated.h | 4 + include/verilated_random.cpp | 96 +++++++++++++++++-- include/verilated_random.h | 7 +- src/V3EmitCFunc.h | 25 +++++ src/V3Error.h | 9 +- src/V3Randomize.cpp | 18 ++++ test_regress/t/t_constraint_unsat.out | 31 ++++++ test_regress/t/t_constraint_unsat.py | 23 +++++ test_regress/t/t_constraint_unsat.v | 76 +++++++++++++++ test_regress/t/t_constraint_unsat_nowarn.out | 18 ++++ test_regress/t/t_constraint_unsat_nowarn.py | 23 +++++ .../t/t_constraint_unsat_protect_ids.out | 31 ++++++ .../t/t_constraint_unsat_protect_ids.py | 27 ++++++ 17 files changed, 401 insertions(+), 12 deletions(-) create mode 100644 test_regress/t/t_constraint_unsat.out create mode 100755 test_regress/t/t_constraint_unsat.py create mode 100755 test_regress/t/t_constraint_unsat.v create mode 100644 test_regress/t/t_constraint_unsat_nowarn.out create mode 100755 test_regress/t/t_constraint_unsat_nowarn.py create mode 100644 test_regress/t/t_constraint_unsat_protect_ids.out create mode 100755 test_regress/t/t_constraint_unsat_protect_ids.py diff --git a/bin/verilator b/bin/verilator index 626d1dda5..ebe3fd3b5 100755 --- a/bin/verilator +++ b/bin/verilator @@ -576,6 +576,7 @@ description of these arguments. +verilator+seed+ Set random seed +verilator+V Show verbose version and config +verilator+version Show version and exit + +verilator+wno+unsatconstr+ Disable constraint warnings =head1 DISTRIBUTION diff --git a/docs/guide/exe_sim.rst b/docs/guide/exe_sim.rst index c8f686646..ed9fb9a99 100644 --- a/docs/guide/exe_sim.rst +++ b/docs/guide/exe_sim.rst @@ -123,3 +123,11 @@ Options: .. option:: +verilator+version Displays program version and exits. + +.. option:: +verilator+wno+unsatconstr+ + + 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)``. diff --git a/docs/guide/warnings.rst b/docs/guide/warnings.rst index fb30d158c..02aa57cb2 100644 --- a/docs/guide/warnings.rst +++ b/docs/guide/warnings.rst @@ -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 diff --git a/include/verilated.cpp b/include/verilated.cpp index f3fce0a10..8cc2d0522 100644 --- a/include/verilated.cpp +++ b/include/verilated.cpp @@ -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(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::max())) { randSeed(static_cast(u64)); diff --git a/include/verilated.h b/include/verilated.h index 7a7b79b8d..5301d9899 100644 --- a/include/verilated.h +++ b/include/verilated.h @@ -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 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; diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 30d13846e..b472d28df 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -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(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 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 } diff --git a/include/verilated_random.h b/include/verilated_random.h index 0b68eadcf..31c5af1f1 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -200,6 +200,8 @@ public: class VlRandomizer VL_NOT_FINAL { // MEMBERS std::vector m_constraints; // Solver-dependent constraints + std::vector + m_constraints_line; // fileline content of the constraint for unsat constraints std::map> 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& randmode) { m_randmodep = &randmode; } diff --git a/src/V3EmitCFunc.h b/src/V3EmitCFunc.h index bb38c80f2..a5fb551ff 100644 --- a/src/V3EmitCFunc.h +++ b/src/V3EmitCFunc.h @@ -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(")"); } diff --git a/src/V3Error.h b/src/V3Error.h index 4be730016..a6284cc52 100644 --- a/src/V3Error.h +++ b/src/V3Error.h @@ -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 diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 313fba115..ed90490c4 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -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); } diff --git a/test_regress/t/t_constraint_unsat.out b/test_regress/t/t_constraint_unsat.out new file mode 100644 index 000000000..67cfc6c0b --- /dev/null +++ b/test_regress/t/t_constraint_unsat.out @@ -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 *-* diff --git a/test_regress/t/t_constraint_unsat.py b/test_regress/t/t_constraint_unsat.py new file mode 100755 index 000000000..52937df98 --- /dev/null +++ b/test_regress/t/t_constraint_unsat.py @@ -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() diff --git a/test_regress/t/t_constraint_unsat.v b/test_regress/t/t_constraint_unsat.v new file mode 100755 index 000000000..f50c8d765 --- /dev/null +++ b/test_regress/t/t_constraint_unsat.v @@ -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 diff --git a/test_regress/t/t_constraint_unsat_nowarn.out b/test_regress/t/t_constraint_unsat_nowarn.out new file mode 100644 index 000000000..7889ade0a --- /dev/null +++ b/test_regress/t/t_constraint_unsat_nowarn.out @@ -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 *-* diff --git a/test_regress/t/t_constraint_unsat_nowarn.py b/test_regress/t/t_constraint_unsat_nowarn.py new file mode 100755 index 000000000..0ef8d3817 --- /dev/null +++ b/test_regress/t/t_constraint_unsat_nowarn.py @@ -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() diff --git a/test_regress/t/t_constraint_unsat_protect_ids.out b/test_regress/t/t_constraint_unsat_protect_ids.out new file mode 100644 index 000000000..6fe852ed4 --- /dev/null +++ b/test_regress/t/t_constraint_unsat_protect_ids.out @@ -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 *-* diff --git a/test_regress/t/t_constraint_unsat_protect_ids.py b/test_regress/t/t_constraint_unsat_protect_ids.py new file mode 100755 index 000000000..6025d7305 --- /dev/null +++ b/test_regress/t/t_constraint_unsat_protect_ids.py @@ -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()