Support basic constrained queue randomization (#5413)

Signed-off-by: Arkadiusz Kozdra <akozdra@antmicro.com>

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<VL_WQ_WORDS_E> qowp;
-    VL_SET_WQ(qowp, 0ULL);
-    WDataOutP owp = qowp;
-    int obits = width();
-    if (obits > VL_QUADSIZE) owp = reinterpret_cast<WDataOutP>(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<VL_WQ_WORDS_E> qowp;
+    VL_SET_WQ(qowp, 0ULL);
+    WDataOutP owp = qowp;
+    const int obits = width();
+    VlWide<VL_WQ_WORDS_E> 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<WDataOutP>(datap(nidx));
+    if (!parseSMTNum(obits, owp, val)) return false;
+
     if (obits <= VL_BYTESIZE) {
-        CData* const p = static_cast<CData*>(datap());
+        CData* const p = static_cast<CData*>(datap(nidx));
         *p = VL_CLEAN_II(obits, obits, owp[0]);
     } else if (obits <= VL_SHORTSIZE) {
-        SData* const p = static_cast<SData*>(datap());
+        SData* const p = static_cast<SData*>(datap(nidx));
         *p = VL_CLEAN_II(obits, obits, owp[0]);
     } else if (obits <= VL_IDATASIZE) {
-        IData* const p = static_cast<IData*>(datap());
+        IData* const p = static_cast<IData*>(datap(nidx));
         *p = VL_CLEAN_II(obits, obits, owp[0]);
     } else if (obits <= VL_QUADSIZE) {
-        QData* const p = static_cast<QData*>(datap());
+        QData* const p = static_cast<QData*>(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;

include/verilated_random.h

@@ -27,10 +27,12 @@
 
 #include "verilated.h"
 
+#include <ostream>
+
 //=============================================================================
 // 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<unsigned>::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 <typename T>
+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<T*>(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<T*>(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<T*>(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 <typename T>
     void write_var(T& var, int width, const char* name,
                    std::uint32_t randmodeIdx = std::numeric_limits<std::uint32_t>::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<const VlRandomVar>(name, width, &var, randmodeIdx);
     }
+    template <typename T>
+    void write_var(VlQueue<T>& var, int width, const char* name,
+                   std::uint32_t randmodeIdx = std::numeric_limits<std::uint32_t>::max()) {
+        if (m_vars.find(name) != m_vars.end()) return;
+        m_vars[name]
+            = std::make_shared<const VlRandomQueueVar<VlQueue<T>>>(name, width, &var, randmodeIdx);
+    }
     void hard(std::string&& constraint);
     void clear();
     void set_randmode(const VlQueue<CData>& randmode) { m_randmode = &randmode; }

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;

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];

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

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