Add support for mockup clock signals in yosys-smtbmc vcd output

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index dbbf01843f97cea3f08f4c0737268496b614670c..a401cacb7ca643b0efd96d1013df801ddc3a74cb 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -41,6 +41,8 @@ struct Smt2Worker
        std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
        pool<Cell*> recursive_cells, registers;
 
+       pool<SigBit> clock_posedge, clock_negedge;
+
        std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
        std::map<Cell*, int> memarrays;
        std::map<int, int> 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<IdString, int> &mod_stbv_width) :
+       Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt,
+                       dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &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<SigBit> 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<IdString, int> mod_stbv_width;
+               dict<IdString, dict<IdString, pair<bool, bool>>> 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 c86b520a2eb7bef68431105c10147c27bbd65718..047fb6cdeab4dc6e6876a177b00146a8e1353dd3 100644 (file)
--- 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 07bd92265afa64125350c1a758624febc27d7dd8..7af37bca2e97695b16ed46c70bfe80a75aa5c8da 100644 (file)
--- 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)
+