From 4a589976041a4157c89b642d4757c3b99f32c5b4 Mon Sep 17 00:00:00 2001 From: Arkadiusz Kozdra Date: Tue, 10 Sep 2024 15:33:14 +0200 Subject: [PATCH] Support basic constrained queue randomization (#5413) Signed-off-by: Arkadiusz Kozdra --- include/verilated_random.cpp | 60 ++++++++++++------- include/verilated_random.h | 56 +++++++++++++++-- src/V3Randomize.cpp | 32 ++++++---- .../t/t_randomize_method_types_unsup.out | 11 +++- .../t/t_randomize_queue_constraints.py | 21 +++++++ .../t/t_randomize_queue_constraints.v | 50 ++++++++++++++++ 6 files changed, 190 insertions(+), 40 deletions(-) create mode 100755 test_regress/t/t_randomize_queue_constraints.py create mode 100644 test_regress/t/t_randomize_queue_constraints.v diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index d0ccefa70..10a22ed9f 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -230,7 +230,7 @@ static Process& getSolver() { const char* const* const cmd = &s_argv[0]; s_solver.open(cmd); - s_solver << "(set-logic QF_BV)\n"; + s_solver << "(set-logic QF_ABV)\n"; s_solver << "(check-sat)\n"; s_solver << "(reset)\n"; std::string s; @@ -253,12 +253,13 @@ static Process& getSolver() { //====================================================================== // VlRandomizer:: Methods -bool VlRandomVar::set(std::string&& val) const { - VlWide qowp; - VL_SET_WQ(qowp, 0ULL); - WDataOutP owp = qowp; - int obits = width(); - if (obits > VL_QUADSIZE) owp = reinterpret_cast(datap()); +void VlRandomVar::emitGetValue(std::ostream& s) const { s << ' ' << m_name; } +void VlRandomVar::emitExtract(std::ostream& s, int i) const { + s << " ((_ extract " << i << ' ' << i << ") " << m_name << ')'; +} +void VlRandomVar::emitType(std::ostream& s) const { s << "(_ BitVec " << width() << ')'; } +int VlRandomVar::totalWidth() const { return m_width; } +static bool parseSMTNum(int obits, WDataOutP owp, const std::string& val) { int i; for (i = 0; val[i] && val[i] != '#'; i++) {} if (val[i++] != '#') return false; @@ -272,17 +273,31 @@ bool VlRandomVar::set(std::string&& val) const { "Internal: Unable to parse solver's randomized number"); return false; } + return true; +} +bool VlRandomVar::set(const std::string& idx, const std::string& val) const { + VlWide qowp; + VL_SET_WQ(qowp, 0ULL); + WDataOutP owp = qowp; + const int obits = width(); + VlWide qiwp; + VL_SET_WQ(qiwp, 0ULL); + if (!idx.empty() && !parseSMTNum(64, qiwp, idx)) return false; + const int nidx = qiwp[0]; + if (obits > VL_QUADSIZE) owp = reinterpret_cast(datap(nidx)); + if (!parseSMTNum(obits, owp, val)) return false; + if (obits <= VL_BYTESIZE) { - CData* const p = static_cast(datap()); + CData* const p = static_cast(datap(nidx)); *p = VL_CLEAN_II(obits, obits, owp[0]); } else if (obits <= VL_SHORTSIZE) { - SData* const p = static_cast(datap()); + SData* const p = static_cast(datap(nidx)); *p = VL_CLEAN_II(obits, obits, owp[0]); } else if (obits <= VL_IDATASIZE) { - IData* const p = static_cast(datap()); + IData* const p = static_cast(datap(nidx)); *p = VL_CLEAN_II(obits, obits, owp[0]); } else if (obits <= VL_QUADSIZE) { - QData* const p = static_cast(datap()); + QData* const p = static_cast(datap(nidx)); *p = VL_CLEAN_QQ(obits, obits, VL_SET_QW(owp)); } else { _vl_clean_inplace_w(obits, owp); @@ -293,7 +308,7 @@ bool VlRandomVar::set(std::string&& val) const { void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) { const IData hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1); int varBits = 0; - for (const auto& var : m_vars) varBits += var.second->width(); + for (const auto& var : m_vars) varBits += var.second->totalWidth(); os << "(= #b"; for (int i = bits - 1; i >= 0; i--) os << (VL_BITISSET_I(hash, i) ? '1' : '0'); if (bits > 1) os << " (concat"; @@ -302,10 +317,10 @@ void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) { IData varBitsWant = (varBits + 1) / 2; if (varBits > 2) os << " (bvxor"; for (const auto& var : m_vars) { - for (int j = 0; j < var.second->width(); j++, varBitsLeft--) { + for (int j = 0; j < var.second->totalWidth(); j++, varBitsLeft--) { const bool doEmit = (VL_RANDOM_RNG_I(rngr) % varBitsLeft) < varBitsWant; if (doEmit) { - os << " ((_ extract " << j << ' ' << j << ") " << var.second->name() << ')'; + var.second->emitExtract(os, j); if (--varBitsWant == 0) break; } } @@ -323,12 +338,13 @@ bool VlRandomizer::next(VlRNG& rngr) { if (!f) return false; f << "(set-option :produce-models true)\n"; - f << "(set-logic QF_BV)\n"; + f << "(set-logic QF_ABV)\n"; f << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n"; f << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n"; for (const auto& var : m_vars) { - f << "(declare-fun " << var.second->name() << " () (_ BitVec " << var.second->width() - << "))\n"; + f << "(declare-fun " << var.second->name() << " () "; + var.second->emitType(f); + f << ")\n"; } for (const std::string& constraint : m_constraints) { f << "(assert (= #b1 " << constraint << "))\n"; @@ -367,7 +383,7 @@ bool VlRandomizer::parseSolution(std::iostream& f) { } f << "(get-value ("; - for (const auto& var : m_vars) f << var.second->name() << ' '; + for (const auto& var : m_vars) var.second->emitGetValue(f); f << "))\n"; // Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE)) @@ -388,8 +404,12 @@ bool VlRandomizer::parseSolution(std::iostream& f) { return false; } - std::string name, value; + std::string name, idx, value; f >> name; + if (name == "(select") { + f >> name; + std::getline(f, idx, ')'); + } std::getline(f, value, ')'); auto it = m_vars.find(name); @@ -399,7 +419,7 @@ bool VlRandomizer::parseSolution(std::iostream& f) { if (!(m_randmode->at(varr.randModeIdx()))) continue; } - varr.set(std::move(value)); + varr.set(idx, value); } return true; diff --git a/include/verilated_random.h b/include/verilated_random.h index bd82d8628..2a0596780 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -27,10 +27,12 @@ #include "verilated.h" +#include + //============================================================================= // VlRandomExpr and subclasses represent expressions for the constraint solver. -class VlRandomVar final { +class VlRandomVar VL_NOT_FINAL { const char* const m_name; // Variable name void* const m_datap; // Reference to variable data const int m_width; // Variable width in bits @@ -42,12 +44,50 @@ public: , m_datap{datap} , m_width{width} , m_randModeIdx{randModeIdx} {} + virtual ~VlRandomVar() = default; const char* name() const { return m_name; } int width() const { return m_width; } - void* datap() const { return m_datap; } + virtual void* datap(int idx) const { return m_datap; } std::uint32_t randModeIdx() const { return m_randModeIdx; } bool randModeIdxNone() const { return randModeIdx() == std::numeric_limits::max(); } - bool set(std::string&&) const; + bool set(const std::string& idx, const std::string& val) const; + virtual void emitGetValue(std::ostream& s) const; + virtual void emitExtract(std::ostream& s, int i) const; + virtual void emitType(std::ostream& s) const; + virtual int totalWidth() const; +}; + +template +class VlRandomQueueVar final : public VlRandomVar { +public: + VlRandomQueueVar(const char* name, int width, void* datap, std::uint32_t randModeIdx) + : VlRandomVar{name, width, datap, randModeIdx} {} + void* datap(int idx) const override { + return &static_cast(VlRandomVar::datap(idx))->atWrite(idx); + } + void emitSelect(std::ostream& s, int i) const { + s << " (select " << name() << " #x"; + for (int j = 28; j >= 0; j -= 4) s << "0123456789abcdef"[(i >> j) & 0xf]; + s << ')'; + } + void emitGetValue(std::ostream& s) const override { + const int length = static_cast(VlRandomVar::datap(0))->size(); + for (int i = 0; i < length; i++) emitSelect(s, i); + } + void emitType(std::ostream& s) const override { + s << "(Array (_ BitVec 32) (_ BitVec " << width() << "))"; + } + int totalWidth() const override { + const int length = static_cast(VlRandomVar::datap(0))->size(); + return width() * length; + } + void emitExtract(std::ostream& s, int i) const override { + const int j = i / width(); + i = i % width(); + s << " ((_ extract " << i << ' ' << i << ')'; + emitSelect(s, j); + s << ')'; + } }; //============================================================================= @@ -75,11 +115,17 @@ public: template void write_var(T& var, int width, const char* name, std::uint32_t randmodeIdx = std::numeric_limits::max()) { - auto it = m_vars.find(name); - if (it != m_vars.end()) return; + if (m_vars.find(name) != m_vars.end()) return; // TODO: make_unique once VlRandomizer is per-instance not per-ref m_vars[name] = std::make_shared(name, width, &var, randmodeIdx); } + template + void write_var(VlQueue& var, int width, const char* name, + std::uint32_t randmodeIdx = std::numeric_limits::max()) { + if (m_vars.find(name) != m_vars.end()) return; + m_vars[name] + = std::make_shared>>(name, width, &var, randmodeIdx); + } void hard(std::string&& constraint); void clear(); void set_randmode(const VlQueue& randmode) { m_randmode = &randmode; } diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 63ce08f58..e10ec5830 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -595,8 +595,11 @@ class ConstraintExprVisitor final : public VNVisitor { = new AstVarRef{varp->fileline(), classp, varp, VAccess::WRITE}; varRefp->classOrPackagep(classOrPackagep); methodp->addPinsp(varRefp); - methodp->addPinsp(new AstConst{varp->dtypep()->fileline(), AstConst::Unsized64{}, - (size_t)varp->width()}); + size_t width = varp->width(); + if (VN_IS(varp->dtypep(), DynArrayDType) || VN_IS(varp->dtypep(), QueueDType)) + width = varp->dtypep()->subDTypep()->width(); + methodp->addPinsp( + new AstConst{varp->dtypep()->fileline(), AstConst::Unsized64{}, width}); AstNodeExpr* const varnamep = new AstCExpr{varp->fileline(), "\"" + smtName + "\"", varp->width()}; varnamep->dtypep(varp->dtypep()); @@ -744,18 +747,23 @@ class ConstraintExprVisitor final : public VNVisitor { void visit(AstCMethodHard* nodep) override { if (editFormat(nodep)) return; - UASSERT_OBJ(nodep->name() == "size", nodep, "Non-size method call in constraints"); + if (nodep->name() == "at" && nodep->fromp()->user1()) { + iterateChildren(nodep); + AstNodeExpr* const argsp + = AstNode::addNext(nodep->fromp()->unlinkFrBack(), nodep->pinsp()->unlinkFrBack()); + AstSFormatF* const newp + = new AstSFormatF{nodep->fileline(), "(select %@ %@)", false, argsp}; + nodep->replaceWith(newp); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + return; + } - AstNode* fromp = nodep->fromp(); - // Warn early while the dtype is still there - fromp->v3warn(E_UNSUPPORTED, "Unsupported: random member variable with type " - << fromp->dtypep()->prettyDTypeNameQ()); + nodep->v3warn(CONSTRAINTIGN, + "Unsupported: randomizing this expression, treating as state"); + nodep->user1(false); - iterateChildren(nodep); // Might change fromp - fromp = nodep->fromp()->unlinkFrBack(); - fromp->dtypep(nodep->dtypep()); - nodep->replaceWith(fromp); - VL_DO_DANGLING(pushDeletep(nodep), nodep); + if (editFormat(nodep)) return; + nodep->v3fatalSrc("Method not handled in constraints? " << nodep); } void visit(AstNodeExpr* nodep) override { if (editFormat(nodep)) return; diff --git a/test_regress/t/t_randomize_method_types_unsup.out b/test_regress/t/t_randomize_method_types_unsup.out index 82369a9c7..d7863c9f1 100644 --- a/test_regress/t/t_randomize_method_types_unsup.out +++ b/test_regress/t/t_randomize_method_types_unsup.out @@ -1,11 +1,16 @@ -%Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:14:25: Unsupported: random member variable with type 'int$[]' +%Warning-CONSTRAINTIGN: t/t_randomize_method_types_unsup.v:14:32: Unsupported: randomizing this expression, treating as state 14 | constraint dynsize { dynarr.size < 20; } - | ^~~~~~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest + | ^~~~ + ... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest + ... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message. %Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:8:13: Unsupported: random member variable with type 'int$[string]' : ... note: In instance 't' 8 | rand int assocarr[string]; | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:9:13: Unsupported: random member variable with type 'int$[]' + : ... note: In instance 't' + 9 | rand int dynarr[]; + | ^~~~~~ %Error-UNSUPPORTED: t/t_randomize_method_types_unsup.v:10:13: Unsupported: random member variable with type 'int$[0:4]' : ... note: In instance 't' 10 | rand int unpackarr[5]; diff --git a/test_regress/t/t_randomize_queue_constraints.py b/test_regress/t/t_randomize_queue_constraints.py new file mode 100755 index 000000000..a2b131082 --- /dev/null +++ b/test_regress/t/t_randomize_queue_constraints.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_randomize_queue_constraints.v b/test_regress/t/t_randomize_queue_constraints.v new file mode 100644 index 000000000..ab8230354 --- /dev/null +++ b/test_regress/t/t_randomize_queue_constraints.v @@ -0,0 +1,50 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2024 by Antmicro Ltd. +// SPDX-License-Identifier: CC0-1.0 + +`define check_rand(cl, field, cond) \ +begin \ + longint prev_result; \ + int ok = 0; \ + for (int i = 0; i < 10; i++) begin \ + longint result; \ + if (!bit'(cl.randomize())) $stop; \ + result = longint'(field); \ + if (!(cond)) $stop; \ + if (i > 0 && result != prev_result) ok = 1; \ + prev_result = result; \ + end \ + if (ok != 1) $stop; \ +end + +class Foo; + rand int m_intQueue[$]; + rand int m_idx; + + function new; + m_intQueue = '{10{0}}; + endfunction + + constraint int_queue_c { + m_idx inside {[0:9]}; + m_intQueue[m_idx] == m_idx + 1; + foreach (m_intQueue[i]) { + m_intQueue[i] inside {[0:127]}; + } + } +endclass + +module t_randomize_queue_constraints; + initial begin + Foo foo = new; + + `check_rand(foo, foo.m_idx, foo.m_idx inside {[0:9]} && foo.m_intQueue[foo.m_idx] == foo.m_idx + 1); + $display("Queue: %p", foo.m_intQueue); + `check_rand(foo, foo.m_intQueue[3], foo.m_intQueue[5] inside {[0:127]}); + $display("Queue: %p", foo.m_intQueue); + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule