Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg"

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index df189fc3f50948bc9efffaf5a74568f8d8e6d15c..cccf3dbb36b67d069ab2ffca6f667973eb080315 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -458,8 +458,10 @@ struct Smt2Worker
                        if (cell->type.in("$anyconst", "$anyseq"))
                        {
                                registers.insert(cell);
-                               decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
-                                               cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+                               string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
+                               if (cell->attributes.count("\\reg"))
+                                       infostr += " " + cell->attributes.at("\\reg").decode_string();
+                               decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, infostr.c_str()));
                                makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
                                register_bv(cell->getPort("\\Y"), idcounter++);
                                recursive_cells.erase(cell);

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 5b5ade1035ed8866d905593af784202c5bbd061a..ceca5b3f8db610baa0879f95ab19ead4c8c67d34 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -709,6 +709,13 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
                     hidden_net = True
             print("    %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
 
+        anyconsts = sorted(smt.hieranyconsts(topmod))
+        for info in anyconsts:
+            if info[3] is not None:
+                modstate = smt.net_expr(topmod, "s%d" % steps_start, info[0])
+                value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
+                print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
             abits, width, rports, wports = smt.mem_info(topmod, mempath)
@@ -733,6 +740,8 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
             for addr, data in addr_data.items():
                 print("    UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
 
+        anyseqs = sorted(smt.hieranyseqs(topmod))
+
         for i in range(steps_start, steps_stop):
             pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
             pi_values = smt.get_net_bin_list(topmod, pi_names, "s%d" % i)
@@ -744,6 +753,12 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
             for name, val in zip(pi_names, pi_values):
                 print("    PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
 
+            for info in anyseqs:
+                if info[3] is not None:
+                    modstate = smt.net_expr(topmod, "s%d" % steps_start, info[0])
+                    value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
+                    print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+
         print("    genclock = 0;", file=f)
         print("  end", file=f)
 
@@ -859,7 +874,10 @@ def print_anyconsts_worker(mod, state, path):
         print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
 
     for fun, info in smt.modinfo[mod].anyconsts.items():
-        print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+        if info[1] is None:
+            print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+        else:
+            print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
 
 
 def print_anyconsts(state):

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index a51986065cede47c7d7acc658b41987b21c7a9b7..abf8e812d3decebd94a19b2cb68a6f3f09f03b67 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -44,6 +44,7 @@ class SmtModInfo:
         self.asserts = dict()
         self.covers = dict()
         self.anyconsts = dict()
+        self.anyseqs = dict()
 
 
 class SmtIo:
@@ -349,7 +350,10 @@ class SmtIo:
             self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
 
         if fields[1] == "yosys-smt2-anyconst":
-            self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3]
+            self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
+
+        if fields[1] == "yosys-smt2-anyseq":
+            self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
 
     def hiernets(self, top, regs_only=False):
         def hiernets_worker(nets, mod, cursor):
@@ -363,6 +367,28 @@ class SmtIo:
         hiernets_worker(nets, top, [])
         return nets
 
+    def hieranyconsts(self, top):
+        def worker(results, mod, cursor):
+            for name, value in sorted(self.modinfo[mod].anyconsts.items()):
+                results.append((cursor, name, value[0], value[1]))
+            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+                worker(results, celltype, cursor + [cellname])
+
+        results = list()
+        worker(results, top, [])
+        return results
+
+    def hieranyseqs(self, top):
+        def worker(results, mod, cursor):
+            for name, value in sorted(self.modinfo[mod].anyseqs.items()):
+                results.append((cursor, name, value[0], value[1]))
+            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+                worker(results, celltype, cursor + [cellname])
+
+        results = list()
+        worker(results, top, [])
+        return results
+
     def hiermems(self, top):
         def hiermems_worker(mems, mod, cursor):
             for memname in sorted(self.modinfo[mod].memories.keys()):
@@ -555,6 +581,9 @@ class SmtIo:
         return [".".join(path)]
 
     def net_expr(self, mod, base, path):
+        if len(path) == 0:
+            return base
+
         if len(path) == 1:
             assert mod in self.modinfo
             if path[0] == "":

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 78e83e038615466ecdbb5830f023167eb6d3557e..6c2eafacdef4b8ba310437572014a7de45ac86da 100644 (file)
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1497,6 +1497,13 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
                                cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
                                cell->parameters["\\WIDTH"] = width;
 
+                               if (attributes.count("\\reg")) {
+                                       auto &attr = attributes.at("\\reg");
+                                       if (attr->type != AST_CONSTANT)
+                                               log_error("Attribute `reg' with non-constant value at %s:%d!\n", filename.c_str(), linenum);
+                                       cell->attributes["\\reg"] =  attr->asAttrConst();
+                               }
+
                                Wire *wire = current_module->addWire(myid + "_wire", width);
                                wire->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
                                cell->setPort("\\Y", wire);

diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 154b59ebc9c8ff3631b0d5b3cf60cf291d68cbe7..c5ff3d402ecc3b42031fdca966b3249d845df658 100644 (file)
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -764,6 +764,7 @@ wire_name_and_opt_assign:
                        AstNode *fcall = new AstNode(AST_FCALL);
                        wire->str = ast_stack.back()->children.back()->str;
                        fcall->str = current_wire_const ? "\\$anyconst" : "\\$anyseq";
+                       fcall->attributes["\\reg"] = AstNode::mkconst_str(RTLIL::unescape_id(wire->str));
                        ast_stack.back()->children.push_back(new AstNode(AST_ASSIGN, wire, fcall));
                }
        } |