Skip to content

Commit 17583b6

Browse files
cliffordwolfcliffordwolf
committed
Add support for mockup clock signals in yosys-smtbmc vcd output
Signed-off-by: Clifford Wolf <[email protected]>
1 parent f2cfe73 commit 17583b6

File tree

3 files changed

+111
-6
lines changed

3 files changed

+111
-6
lines changed

‎backends/smt2/smt2.cc

Lines changed: 57 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,8 @@ struct Smt2Worker
4141
std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
4242
pool<Cell*> recursive_cells, registers;
4343

44+
pool<SigBit> clock_posedge, clock_negedge;
45+
4446
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
4547
std::map<Cell*, int> memarrays;
4648
std::map<int, int> bvsizes;
@@ -104,18 +106,24 @@ struct Smt2Worker
104106
decls.push_back(decl_str + "\n");
105107
}
106108

107-
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict<IdString, int> &mod_stbv_width) :
109+
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt,
110+
dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
108111
ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
109112
verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
110113
{
114+
pool<SigBit> noclock;
115+
111116
makebits(stringf("%s_is", get_id(module)));
112117

113118
for (auto cell : module->cells())
114-
for (auto &conn : cell->connections()) {
119+
for (auto &conn : cell->connections())
120+
{
115121
if (GetSize(conn.second) == 0)
116122
continue;
123+
117124
bool is_input = ct.cell_input(cell->type, conn.first);
118125
bool is_output = ct.cell_output(cell->type, conn.first);
126+
119127
if (is_output && !is_input)
120128
for (auto bit : sigmap(conn.second)) {
121129
if (bit_driver.count(bit))
@@ -125,6 +133,48 @@ struct Smt2Worker
125133
else if (is_output || !is_input)
126134
log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
127135
log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
136+
137+
if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C"))
138+
{
139+
bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool());
140+
for (auto bit : sigmap(conn.second)) {
141+
if (posedge)
142+
clock_posedge.insert(bit);
143+
else
144+
clock_negedge.insert(bit);
145+
}
146+
}
147+
else
148+
if (mod_clk_cache.count(cell->type) && mod_clk_cache.at(cell->type).count(conn.first))
149+
{
150+
for (auto bit : sigmap(conn.second)) {
151+
if (mod_clk_cache.at(cell->type).at(conn.first).first)
152+
clock_posedge.insert(bit);
153+
if (mod_clk_cache.at(cell->type).at(conn.first).second)
154+
clock_negedge.insert(bit);
155+
}
156+
}
157+
else
158+
{
159+
for (auto bit : sigmap(conn.second))
160+
noclock.insert(bit);
161+
}
162+
}
163+
164+
for (auto bit : noclock) {
165+
clock_posedge.erase(bit);
166+
clock_negedge.erase(bit);
167+
}
168+
169+
for (auto wire : module->wires())
170+
{
171+
if (!wire->port_input || GetSize(wire) != 1)
172+
continue;
173+
SigBit bit = sigmap(wire);
174+
if (clock_posedge.count(bit))
175+
mod_clk_cache[module->name][wire->name].first = true;
176+
if (clock_negedge.count(bit))
177+
mod_clk_cache[module->name][wire->name].second = true;
128178
}
129179
}
130180

@@ -731,6 +781,9 @@ struct Smt2Worker
731781
decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
732782
if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
733783
decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
784+
if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
785+
decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
786+
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
734787
if (bvmode && GetSize(sig) > 1) {
735788
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
736789
get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
@@ -1386,6 +1439,7 @@ struct Smt2Backend : public Backend {
13861439
}
13871440

13881441
dict<IdString, int> mod_stbv_width;
1442+
dict<IdString, dict<IdString, pair<bool, bool>>> mod_clk_cache;
13891443
Module *topmod = design->top_module();
13901444
std::string topmod_id;
13911445

@@ -1396,7 +1450,7 @@ struct Smt2Backend : public Backend {
13961450

13971451
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
13981452

1399-
Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width);
1453+
Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width, mod_clk_cache);
14001454
worker.run();
14011455
worker.write(*f);
14021456

‎backends/smt2/smtbmc.py

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -589,7 +589,11 @@ def write_vcd_trace(steps_start, steps_stop, index):
589589
if n.startswith("$"):
590590
hidden_net = True
591591
if not hidden_net:
592-
vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
592+
edge = smt.net_clock(topmod, netpath)
593+
if edge is None:
594+
vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
595+
else:
596+
vcd.add_clock([topmod] + netpath, edge)
593597
path_list.append(netpath)
594598

595599
mem_trace_data = dict()

‎backends/smt2/smtio.py

Lines changed: 49 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@ def __init__(self):
5353
self.memories = dict()
5454
self.wires = set()
5555
self.wsize = dict()
56+
self.clocks = dict()
5657
self.cells = dict()
5758
self.asserts = dict()
5859
self.covers = dict()
@@ -404,6 +405,13 @@ def info(self, stmt):
404405
self.modinfo[self.curmod].wires.add(fields[2])
405406
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
406407

408+
if fields[1] == "yosys-smt2-clock":
409+
for edge in fields[3:]:
410+
if fields[2] not in self.modinfo[self.curmod].clocks:
411+
self.modinfo[self.curmod].clocks[fields[2]] = edge
412+
elif self.modinfo[self.curmod].clocks[fields[2]] != edge:
413+
self.modinfo[self.curmod].clocks[fields[2]] = "event"
414+
407415
if fields[1] == "yosys-smt2-assert":
408416
self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
409417

@@ -672,6 +680,17 @@ def net_width(self, mod, net_path):
672680
assert net_path[-1] in self.modinfo[mod].wsize
673681
return self.modinfo[mod].wsize[net_path[-1]]
674682

683+
def net_clock(self, mod, net_path):
684+
for i in range(len(net_path)-1):
685+
assert mod in self.modinfo
686+
assert net_path[i] in self.modinfo[mod].cells
687+
mod = self.modinfo[mod].cells[net_path[i]]
688+
689+
assert mod in self.modinfo
690+
if net_path[-1] not in self.modinfo[mod].clocks:
691+
return None
692+
return self.modinfo[mod].clocks[net_path[-1]]
693+
675694
def net_exists(self, mod, net_path):
676695
for i in range(len(net_path)-1):
677696
if mod not in self.modinfo: return False
@@ -823,18 +842,27 @@ def __init__(self, f):
823842
self.f = f
824843
self.t = -1
825844
self.nets = dict()
845+
self.clocks = dict()
826846

827847
def add_net(self, path, width):
828848
path = tuple(path)
829849
assert self.t == -1
830850
key = "n%d" % len(self.nets)
831851
self.nets[path] = (key, width)
832852

853+
def add_clock(self, path, edge):
854+
path = tuple(path)
855+
assert self.t == -1
856+
key = "n%d" % len(self.nets)
857+
self.nets[path] = (key, 1)
858+
self.clocks[path] = (key, edge)
859+
833860
def set_net(self, path, bits):
834861
path = tuple(path)
835862
assert self.t >= 0
836863
assert path in self.nets
837-
print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
864+
if path not in self.clocks:
865+
print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
838866

839867
def set_time(self, t):
840868
assert t >= self.t
@@ -851,13 +879,32 @@ def set_time(self, t):
851879
print("$scope module %s $end" % path[len(scope)], file=self.f)
852880
scope.append(path[len(scope)-1])
853881
key, width = self.nets[path]
854-
print("$var wire %d %s %s $end" % (width, key, path[-1]), file=self.f)
882+
if path in self.clocks and self.clocks[path][1] == "event":
883+
print("$var event 1 %s %s $end" % (key, path[-1]), file=self.f)
884+
else:
885+
print("$var wire %d %s %s $end" % (width, key, path[-1]), file=self.f)
855886
for i in range(len(scope)):
856887
print("$upscope $end", file=self.f)
857888
print("$enddefinitions $end", file=self.f)
889+
858890
self.t = t
859891
assert self.t >= 0
892+
893+
if self.t > 0:
894+
print("#%d" % (10 * self.t - 5), file=self.f)
895+
for path in sorted(self.clocks.keys()):
896+
if self.clocks[path][1] == "posedge":
897+
print("b0 %s" % self.nets[path][0], file=self.f)
898+
elif self.clocks[path][1] == "negedge":
899+
print("b1 %s" % self.nets[path][0], file=self.f)
900+
860901
print("#%d" % (10 * self.t), file=self.f)
861902
print("1!", file=self.f)
862903
print("b%s t" % format(self.t, "032b"), file=self.f)
863904

905+
for path in sorted(self.clocks.keys()):
906+
if self.clocks[path][1] == "negedge":
907+
print("b0 %s" % self.nets[path][0], file=self.f)
908+
else:
909+
print("b1 %s" % self.nets[path][0], file=self.f)
910+

0 commit comments

Comments
 (0)