Skip to content

Commit 8f8bacc

Browse files
cliffordwolfcliffordwolf
committedJun 7, 2017
Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg"
1 parent 129984e commit 8f8bacc

File tree

5 files changed

+61
-4
lines changed

5 files changed

+61
-4
lines changed
 

Diff for: ‎backends/smt2/smt2.cc

+4-2
Original file line numberDiff line numberDiff line change
@@ -458,8 +458,10 @@ struct Smt2Worker
458458
if (cell->type.in("$anyconst", "$anyseq"))
459459
{
460460
registers.insert(cell);
461-
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
462-
cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
461+
string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
462+
if (cell->attributes.count("\\reg"))
463+
infostr += " " + cell->attributes.at("\\reg").decode_string();
464+
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, infostr.c_str()));
463465
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
464466
register_bv(cell->getPort("\\Y"), idcounter++);
465467
recursive_cells.erase(cell);

Diff for: ‎backends/smt2/smtbmc.py

+19-1
Original file line numberDiff line numberDiff line change
@@ -709,6 +709,13 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
709709
hidden_net = True
710710
print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
711711

712+
anyconsts = sorted(smt.hieranyconsts(topmod))
713+
for info in anyconsts:
714+
if info[3] is not None:
715+
modstate = smt.net_expr(topmod, "s%d" % steps_start, info[0])
716+
value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
717+
print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
718+
712719
mems = sorted(smt.hiermems(topmod))
713720
for mempath in mems:
714721
abits, width, rports, wports = smt.mem_info(topmod, mempath)
@@ -733,6 +740,8 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
733740
for addr, data in addr_data.items():
734741
print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
735742

743+
anyseqs = sorted(smt.hieranyseqs(topmod))
744+
736745
for i in range(steps_start, steps_stop):
737746
pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
738747
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):
744753
for name, val in zip(pi_names, pi_values):
745754
print(" PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
746755

756+
for info in anyseqs:
757+
if info[3] is not None:
758+
modstate = smt.net_expr(topmod, "s%d" % steps_start, info[0])
759+
value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
760+
print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
761+
747762
print(" genclock = 0;", file=f)
748763
print(" end", file=f)
749764

@@ -859,7 +874,10 @@ def print_anyconsts_worker(mod, state, path):
859874
print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
860875

861876
for fun, info in smt.modinfo[mod].anyconsts.items():
862-
print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
877+
if info[1] is None:
878+
print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
879+
else:
880+
print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
863881

864882

865883
def print_anyconsts(state):

Diff for: ‎backends/smt2/smtio.py

+30-1
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ def __init__(self):
4444
self.asserts = dict()
4545
self.covers = dict()
4646
self.anyconsts = dict()
47+
self.anyseqs = dict()
4748

4849

4950
class SmtIo:
@@ -349,7 +350,10 @@ def info(self, stmt):
349350
self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
350351

351352
if fields[1] == "yosys-smt2-anyconst":
352-
self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3]
353+
self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
354+
355+
if fields[1] == "yosys-smt2-anyseq":
356+
self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
353357

354358
def hiernets(self, top, regs_only=False):
355359
def hiernets_worker(nets, mod, cursor):
@@ -363,6 +367,28 @@ def hiernets_worker(nets, mod, cursor):
363367
hiernets_worker(nets, top, [])
364368
return nets
365369

370+
def hieranyconsts(self, top):
371+
def worker(results, mod, cursor):
372+
for name, value in sorted(self.modinfo[mod].anyconsts.items()):
373+
results.append((cursor, name, value[0], value[1]))
374+
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
375+
worker(results, celltype, cursor + [cellname])
376+
377+
results = list()
378+
worker(results, top, [])
379+
return results
380+
381+
def hieranyseqs(self, top):
382+
def worker(results, mod, cursor):
383+
for name, value in sorted(self.modinfo[mod].anyseqs.items()):
384+
results.append((cursor, name, value[0], value[1]))
385+
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
386+
worker(results, celltype, cursor + [cellname])
387+
388+
results = list()
389+
worker(results, top, [])
390+
return results
391+
366392
def hiermems(self, top):
367393
def hiermems_worker(mems, mod, cursor):
368394
for memname in sorted(self.modinfo[mod].memories.keys()):
@@ -555,6 +581,9 @@ def get_path(self, mod, path):
555581
return [".".join(path)]
556582

557583
def net_expr(self, mod, base, path):
584+
if len(path) == 0:
585+
return base
586+
558587
if len(path) == 1:
559588
assert mod in self.modinfo
560589
if path[0] == "":

Diff for: ‎frontends/ast/genrtlil.cc

+7
Original file line numberDiff line numberDiff line change
@@ -1497,6 +1497,13 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
14971497
cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
14981498
cell->parameters["\\WIDTH"] = width;
14991499

1500+
if (attributes.count("\\reg")) {
1501+
auto &attr = attributes.at("\\reg");
1502+
if (attr->type != AST_CONSTANT)
1503+
log_error("Attribute `reg' with non-constant value at %s:%d!\n", filename.c_str(), linenum);
1504+
cell->attributes["\\reg"] = attr->asAttrConst();
1505+
}
1506+
15001507
Wire *wire = current_module->addWire(myid + "_wire", width);
15011508
wire->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
15021509
cell->setPort("\\Y", wire);

Diff for: ‎frontends/verilog/verilog_parser.y

+1
Original file line numberDiff line numberDiff line change
@@ -764,6 +764,7 @@ wire_name_and_opt_assign:
764764
AstNode *fcall = new AstNode(AST_FCALL);
765765
wire->str = ast_stack.back()->children.back()->str;
766766
fcall->str = current_wire_const ? "\\$anyconst" : "\\$anyseq";
767+
fcall->attributes["\\reg"] = AstNode::mkconst_str(RTLIL::unescape_id(wire->str));
767768
ast_stack.back()->children.push_back(new AstNode(AST_ASSIGN, wire, fcall));
768769
}
769770
} |

0 commit comments

Comments
 (0)
Please sign in to comment.