From 17583b6a2175bf509d6a233e5684a183af54f48c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 20 Feb 2018 17:45:22 +0100 Subject: [PATCH] Add support for mockup clock signals in yosys-smtbmc vcd output Signed-off-by: Clifford Wolf --- backends/smt2/smt2.cc | 60 ++++++++++++++++++++++++++++++++++++++--- backends/smt2/smtbmc.py | 6 ++++- backends/smt2/smtio.py | 51 +++++++++++++++++++++++++++++++++-- 3 files changed, 111 insertions(+), 6 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index dbbf01843..a401cacb7 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -41,6 +41,8 @@ struct Smt2Worker std::set exported_cells, hiercells, hiercells_queue; pool recursive_cells, registers; + pool clock_posedge, clock_negedge; + std::map> fcache; std::map memarrays; std::map bvsizes; @@ -104,18 +106,24 @@ struct Smt2Worker decls.push_back(decl_str + "\n"); } - Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict &mod_stbv_width) : + Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, + dict &mod_stbv_width, dict>> &mod_clk_cache) : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0) { + pool noclock; + makebits(stringf("%s_is", get_id(module))); for (auto cell : module->cells()) - for (auto &conn : cell->connections()) { + for (auto &conn : cell->connections()) + { if (GetSize(conn.second) == 0) continue; + bool is_input = ct.cell_input(cell->type, conn.first); bool is_output = ct.cell_output(cell->type, conn.first); + if (is_output && !is_input) for (auto bit : sigmap(conn.second)) { if (bit_driver.count(bit)) @@ -125,6 +133,48 @@ struct Smt2Worker else if (is_output || !is_input) log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type)); + + if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C")) + { + bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool()); + for (auto bit : sigmap(conn.second)) { + if (posedge) + clock_posedge.insert(bit); + else + clock_negedge.insert(bit); + } + } + else + if (mod_clk_cache.count(cell->type) && mod_clk_cache.at(cell->type).count(conn.first)) + { + for (auto bit : sigmap(conn.second)) { + if (mod_clk_cache.at(cell->type).at(conn.first).first) + clock_posedge.insert(bit); + if (mod_clk_cache.at(cell->type).at(conn.first).second) + clock_negedge.insert(bit); + } + } + else + { + for (auto bit : sigmap(conn.second)) + noclock.insert(bit); + } + } + + for (auto bit : noclock) { + clock_posedge.erase(bit); + clock_negedge.erase(bit); + } + + for (auto wire : module->wires()) + { + if (!wire->port_input || GetSize(wire) != 1) + continue; + SigBit bit = sigmap(wire); + if (clock_posedge.count(bit)) + mod_clk_cache[module->name][wire->name].first = true; + if (clock_negedge.count(bit)) + mod_clk_cache[module->name][wire->name].second = true; } } @@ -731,6 +781,9 @@ struct Smt2Worker decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); + if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) + decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), + clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); if (bvmode && GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str())); @@ -1386,6 +1439,7 @@ struct Smt2Backend : public Backend { } dict mod_stbv_width; + dict>> mod_clk_cache; Module *topmod = design->top_module(); std::string topmod_id; @@ -1396,7 +1450,7 @@ struct Smt2Backend : public Backend { log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); - Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width); + Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width, mod_clk_cache); worker.run(); worker.write(*f); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index c86b520a2..047fb6cde 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -589,7 +589,11 @@ def write_vcd_trace(steps_start, steps_stop, index): if n.startswith("$"): hidden_net = True if not hidden_net: - vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath)) + edge = smt.net_clock(topmod, netpath) + if edge is None: + vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath)) + else: + vcd.add_clock([topmod] + netpath, edge) path_list.append(netpath) mem_trace_data = dict() diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 07bd92265..7af37bca2 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -53,6 +53,7 @@ class SmtModInfo: self.memories = dict() self.wires = set() self.wsize = dict() + self.clocks = dict() self.cells = dict() self.asserts = dict() self.covers = dict() @@ -404,6 +405,13 @@ class SmtIo: self.modinfo[self.curmod].wires.add(fields[2]) self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3]) + if fields[1] == "yosys-smt2-clock": + for edge in fields[3:]: + if fields[2] not in self.modinfo[self.curmod].clocks: + self.modinfo[self.curmod].clocks[fields[2]] = edge + elif self.modinfo[self.curmod].clocks[fields[2]] != edge: + self.modinfo[self.curmod].clocks[fields[2]] = "event" + if fields[1] == "yosys-smt2-assert": self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3] @@ -672,6 +680,17 @@ class SmtIo: assert net_path[-1] in self.modinfo[mod].wsize return self.modinfo[mod].wsize[net_path[-1]] + def net_clock(self, mod, net_path): + for i in range(len(net_path)-1): + assert mod in self.modinfo + assert net_path[i] in self.modinfo[mod].cells + mod = self.modinfo[mod].cells[net_path[i]] + + assert mod in self.modinfo + if net_path[-1] not in self.modinfo[mod].clocks: + return None + return self.modinfo[mod].clocks[net_path[-1]] + def net_exists(self, mod, net_path): for i in range(len(net_path)-1): if mod not in self.modinfo: return False @@ -823,6 +842,7 @@ class MkVcd: self.f = f self.t = -1 self.nets = dict() + self.clocks = dict() def add_net(self, path, width): path = tuple(path) @@ -830,11 +850,19 @@ class MkVcd: key = "n%d" % len(self.nets) self.nets[path] = (key, width) + def add_clock(self, path, edge): + path = tuple(path) + assert self.t == -1 + key = "n%d" % len(self.nets) + self.nets[path] = (key, 1) + self.clocks[path] = (key, edge) + def set_net(self, path, bits): path = tuple(path) assert self.t >= 0 assert path in self.nets - print("b%s %s" % (bits, self.nets[path][0]), file=self.f) + if path not in self.clocks: + print("b%s %s" % (bits, self.nets[path][0]), file=self.f) def set_time(self, t): assert t >= self.t @@ -851,13 +879,32 @@ class MkVcd: print("$scope module %s $end" % path[len(scope)], file=self.f) scope.append(path[len(scope)-1]) key, width = self.nets[path] - print("$var wire %d %s %s $end" % (width, key, path[-1]), file=self.f) + if path in self.clocks and self.clocks[path][1] == "event": + print("$var event 1 %s %s $end" % (key, path[-1]), file=self.f) + else: + print("$var wire %d %s %s $end" % (width, key, path[-1]), file=self.f) for i in range(len(scope)): print("$upscope $end", file=self.f) print("$enddefinitions $end", file=self.f) + self.t = t assert self.t >= 0 + + if self.t > 0: + print("#%d" % (10 * self.t - 5), file=self.f) + for path in sorted(self.clocks.keys()): + if self.clocks[path][1] == "posedge": + print("b0 %s" % self.nets[path][0], file=self.f) + elif self.clocks[path][1] == "negedge": + print("b1 %s" % self.nets[path][0], file=self.f) + print("#%d" % (10 * self.t), file=self.f) print("1!", file=self.f) print("b%s t" % format(self.t, "032b"), file=self.f) + for path in sorted(self.clocks.keys()): + if self.clocks[path][1] == "negedge": + print("b0 %s" % self.nets[path][0], file=self.f) + else: + print("b1 %s" % self.nets[path][0], file=self.f) + -- 2.30.2