aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smtbmc.py13
-rw-r--r--backends/smt2/smtio.py69
2 files changed, 59 insertions, 23 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 3d96b07a0..f74908f87 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -98,7 +98,7 @@ smt.setup("QF_AUFBV")
with open(args[0], "r") as f:
for line in f:
smt.write(line)
- smt.getinfo(line)
+ smt.info(line)
if topmod is None:
topmod = smt.topmod
@@ -106,18 +106,19 @@ if topmod is None:
assert topmod is not None
assert topmod in smt.modinfo
+
def write_vcd_model(steps):
print("%s Writing model to VCD file." % smt.timestamp())
vcd = mkvcd(open(vcdfile, "w"))
- for netname in sorted(smt.modinfo[topmod].wsize.keys()):
- width = len(smt.get_net_bin(topmod, netname, "s0"))
- vcd.add_net(netname, width)
+ for netpath in sorted(smt.hiernets(topmod)):
+ width = len(smt.get_net_bin(topmod, netpath, "s0"))
+ vcd.add_net([topmod] + netpath, width)
for i in range(steps):
vcd.set_time(i)
- for netname in smt.modinfo[topmod].wsize.keys():
- vcd.set_net(netname, smt.get_net_bin(topmod, netname, "s%d" % i))
+ for netpath in sorted(smt.hiernets(topmod)):
+ vcd.set_net([topmod] + netpath, smt.get_net_bin(topmod, netpath, "s%d" % i))
vcd.set_time(steps)
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 14ad75e3e..5f93a2fed 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -97,7 +97,7 @@ class smtio:
self.p.stdin.write(bytes(stmt + "\n", "ascii"))
self.p.stdin.flush()
- def getinfo(self, stmt):
+ def info(self, stmt):
if not stmt.startswith("; yosys-smt2-"):
return
@@ -129,6 +129,17 @@ class smtio:
self.modinfo[self.curmod].wires.add(fields[2])
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
+ def hiernets(self, top):
+ def hiernets_worker(nets, mod, cursor):
+ for netname in sorted(self.modinfo[mod].wsize.keys()):
+ nets.append(cursor + [netname])
+ for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+ hiernets_worker(nets, celltype, cursor + [cellname])
+
+ nets = list()
+ hiernets_worker(nets, top, [])
+ return nets
+
def read(self):
stmt = []
count_brackets = 0
@@ -282,19 +293,32 @@ class smtio:
self.write("(get-value (%s))" % (expr))
return self.parse(self.read())[0][1]
- def get_net(self, mod_name, net_name, state_name):
- return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
+ def get_net(self, mod_name, net_path, state_name):
+ def mkexpr(mod, base, path):
+ if len(path) == 1:
+ assert mod in self.modinfo
+ assert path[0] in self.modinfo[mod].wsize
+ return "(|%s_n %s| %s)" % (mod, path[0], base)
+
+ assert mod in self.modinfo
+ assert path[0] in self.modinfo[mod].cells
+
+ nextmod = self.modinfo[mod].cells[path[0]]
+ nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
+ return mkexpr(nextmod, nextbase, path[1:])
+
+ return self.get(mkexpr(mod_name, state_name, net_path))
- def get_net_bool(self, mod_name, net_name, state_name):
- v = self.get_net(mod_name, net_name, state_name)
+ def get_net_bool(self, mod_name, net_path, state_name):
+ v = self.get_net(mod_name, net_path, state_name)
assert v in ["true", "false"]
return 1 if v == "true" else 0
- def get_net_hex(self, mod_name, net_name, state_name):
- return self.bv2hex(self.get_net(mod_name, net_name, state_name))
+ def get_net_hex(self, mod_name, net_path, state_name):
+ return self.bv2hex(self.get_net(mod_name, net_path, state_name))
- def get_net_bin(self, mod_name, net_name, state_name):
- return self.bv2bin(self.get_net(mod_name, net_name, state_name))
+ def get_net_bin(self, mod_name, net_path, state_name):
+ return self.bv2bin(self.get_net(mod_name, net_path, state_name))
def wait(self):
self.p.wait()
@@ -344,24 +368,35 @@ class mkvcd:
self.t = -1
self.nets = dict()
- def add_net(self, name, width):
+ def add_net(self, path, width):
+ path = tuple(path)
assert self.t == -1
key = "n%d" % len(self.nets)
- self.nets[name] = (key, width)
+ self.nets[path] = (key, width)
- def set_net(self, name, bits):
- assert name in self.nets
+ def set_net(self, path, bits):
+ path = tuple(path)
assert self.t >= 0
- print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
+ assert path in self.nets
+ print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
def set_time(self, t):
assert t >= self.t
if t != self.t:
if self.t == -1:
print("$var event 1 ! smt_clock $end", file=self.f)
- for name in sorted(self.nets):
- key, width = self.nets[name]
- print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
+ scope = []
+ for path in sorted(self.nets):
+ while len(scope)+1 > len(path) or (len(scope) > 0 and scope[-1] != path[len(scope)-1]):
+ print("$upscope $end", file=self.f)
+ scope = scope[:-1]
+ while len(scope)+1 < len(path):
+ 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)
+ 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