mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Add "yosys-smtbmc --vlogtb-top"

Browse source
This commit is contained in:
Clifford Wolf 2017-07-01 18:19:23 +02:00
parent 0a02cdb93b
commit ea805af6f5
1 changed files with 32 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
backends/smt2/smtbmc.py
View file

@ -33,6 +33,7 @@ aimfile = None
aiwfile = None aiwfile = None
aigheader = True aigheader = True
vlogtbfile = None vlogtbfile = None
vlogtbtop = None
inconstr = list() inconstr = list()
outconstr = None outconstr = None
gentrace = False gentrace = False
@ -107,6 +108,11 @@ yosys-smtbmc [options] <yosys_smt2_output>
--dump-vlogtb <verilog_filename> --dump-vlogtb <verilog_filename>
write trace as Verilog test bench write trace as Verilog test bench
--vlogtb-top <hierarchical_name>
use the given entity as top module for the generated
Verilog test bench. The <hierarchical_name> is relative
to the design top module without the top module name.
--dump-smtc <constr_filename> --dump-smtc <constr_filename>
write trace as constraints file write trace as constraints file
@ -126,7 +132,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
try: try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader",
"dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="]) "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append="])
except: except:
usage() usage()
@ -165,6 +171,8 @@ for o, a in opts:
vcdfile = a vcdfile = a
elif o == "--dump-vlogtb": elif o == "--dump-vlogtb":
vlogtbfile = a vlogtbfile = a
elif o == "--vlogtb-top":
vlogtbtop = a
elif o == "--dump-smtc": elif o == "--dump-smtc":
outconstr = a outconstr = a
elif o == "--dump-all": elif o == "--dump-all":
@ -661,6 +669,15 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
filename = vlogtbfile.replace("%", index) filename = vlogtbfile.replace("%", index)
print_msg("Writing trace to Verilog testbench: %s" % (filename)) print_msg("Writing trace to Verilog testbench: %s" % (filename))
vlogtb_topmod = topmod
vlogtb_state = "s@@step_idx@@"
if vlogtbtop is not None:
for item in vlogtbtop.split("."):
assert item in smt.modinfo[vlogtb_topmod].cells
vlogtb_state = "(|%s_h %s| %s)" % (vlogtb_topmod, item, vlogtb_state)
vlogtb_topmod = smt.modinfo[vlogtb_topmod].cells[item]
with open(filename, "w") as f: with open(filename, "w") as f:
print("module testbench;", file=f) print("module testbench;", file=f)
print(" reg [4095:0] vcdfile;", file=f) print(" reg [4095:0] vcdfile;", file=f)
@ -669,10 +686,10 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
primary_inputs = list() primary_inputs = list()
clock_inputs = set() clock_inputs = set()
for name in smt.modinfo[topmod].inputs: for name in smt.modinfo[vlogtb_topmod].inputs:
if name in ["clk", "clock", "CLK", "CLOCK"]: if name in ["clk", "clock", "CLK", "CLOCK"]:
clock_inputs.add(name) clock_inputs.add(name)
width = smt.modinfo[topmod].wsize[name] width = smt.modinfo[vlogtb_topmod].wsize[name]
primary_inputs.append((name, width)) primary_inputs.append((name, width))
for name, width in primary_inputs: for name, width in primary_inputs:
@ -681,7 +698,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
else: else:
print(" reg [%d:0] PI_%s;" % (width-1, name), file=f) print(" reg [%d:0] PI_%s;" % (width-1, name), file=f)
print(" %s UUT (" % topmod, file=f) print(" %s UUT (" % vlogtb_topmod, file=f)
print(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f) print(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
print(" );", file=f) print(" );", file=f)
@ -698,8 +715,8 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
print(" initial begin", file=f) print(" initial begin", file=f)
regs = sorted(smt.hiernets(topmod, regs_only=True)) regs = sorted(smt.hiernets(vlogtb_topmod, regs_only=True))
regvals = smt.get_net_bin_list(topmod, regs, "s%d" % steps_start) regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps_start)))
print(" #1;", file=f) print(" #1;", file=f)
for reg, val in zip(regs, regvals): for reg, val in zip(regs, regvals):
@ -709,23 +726,23 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
hidden_net = True hidden_net = True
print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f) print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
anyconsts = sorted(smt.hieranyconsts(topmod)) anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod))
for info in anyconsts: for info in anyconsts:
if info[3] is not None: if info[3] is not None:
modstate = smt.net_expr(topmod, "s%d" % steps_start, info[0]) modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0])
value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate))) value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f); print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
mems = sorted(smt.hiermems(topmod)) mems = sorted(smt.hiermems(vlogtb_topmod))
for mempath in mems: for mempath in mems:
abits, width, rports, wports = smt.mem_info(topmod, mempath) abits, width, rports, wports = smt.mem_info(vlogtb_topmod, mempath)
addr_expr_list = list() addr_expr_list = list()
data_expr_list = list() data_expr_list = list()
for i in range(steps_start, steps_stop): for i in range(steps_start, steps_stop):
for j in range(rports): for j in range(rports):
addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j)) addr_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
data_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j)) data_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
addr_list = smt.get_list(addr_expr_list) addr_list = smt.get_list(addr_expr_list)
data_list = smt.get_list(data_expr_list) data_list = smt.get_list(data_expr_list)
@ -740,11 +757,11 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for addr, data in addr_data.items(): for addr, data in addr_data.items():
print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f) print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
anyseqs = sorted(smt.hieranyseqs(topmod)) anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))
for i in range(steps_start, steps_stop): for i in range(steps_start, steps_stop):
pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs] pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
pi_values = smt.get_net_bin_list(topmod, pi_names, "s%d" % i) pi_values = smt.get_net_bin_list(vlogtb_topmod, pi_names, vlogtb_state.replace("@@step_idx@@", str(i)))
print(" #1;", file=f) print(" #1;", file=f)
print(" // state %d" % i, file=f) print(" // state %d" % i, file=f)
@ -755,7 +772,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for info in anyseqs: for info in anyseqs:
if info[3] is not None: if info[3] is not None:
modstate = smt.net_expr(topmod, "s%d" % i, info[0]) modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0])
value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate))) value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
print(" UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f); print(" UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);