mirror of https://github.com/YosysHQ/yosys.git
Yosys-smtbmc: Support for hierarchical VCD dumping
This commit is contained in:
Clifford Wolf
parent
0153ad85d9
commit
c71785d65e
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
def get_net_bool(self, mod_name, net_name, state_name):
|
||||
v = self.get_net(mod_name, net_name, state_name)
|
||||
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_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
|
||||
|
|
|
|||
Loading…
Reference in New Issue