From 8f8baccfde62d238025024eb1060ae0aba4c77e3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Jun 2017 12:30:24 +0200 Subject: [PATCH] Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg" --- backends/smt2/smt2.cc | 6 ++++-- backends/smt2/smtbmc.py | 20 ++++++++++++++++++- backends/smt2/smtio.py | 31 +++++++++++++++++++++++++++++- frontends/ast/genrtlil.cc | 7 +++++++ frontends/verilog/verilog_parser.y | 1 + 5 files changed, 61 insertions(+), 4 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index df189fc3f..cccf3dbb3 100644 --- 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 5b5ade103..ceca5b3f8 100644 --- 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 a51986065..abf8e812d 100644 --- 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 78e83e038..6c2eafacd 100644 --- 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 154b59ebc..c5ff3d402 100644 --- 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)); } } |