riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

smtbmc: escape identifiers in verilog testbench

This commit is contained in:
Jakob Wenzel 2020-10-06 11:24:29 +02:00
parent fd306b0520
commit 54166ae0c5
1 changed files with 29 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
backends/smt2/smtbmc.py
View File

@ -817,6 +817,24 @@ def write_vcd_trace(steps_start, steps_stop, index):
vcd.set_time(steps_stop) vcd.set_time(steps_stop)
def char_ok_in_verilog(c,i):
if ('A' <= c <= 'Z'): return True
if ('a' <= c <= 'z'): return True
if ('0' <= c <= '9' and i>0): return True
if (c == '_'): return True
if (c == '$'): return True
return False
def escape_identifier(identifier):
if type(identifier) is list:
return map(escape_identifier, identifier)
if "." in identifier:
return ".".join(escape_identifier(identifier.split(".")))
if (all(char_ok_in_verilog(identifier[i],i) for i in range(0, len(identifier)))):
return identifier
return "\\"+identifier+" "
def write_vlogtb_trace(steps_start, steps_stop, index): def write_vlogtb_trace(steps_start, steps_stop, index):
filename = vlogtbfile.replace("%", index) filename = vlogtbfile.replace("%", index)
@ -858,12 +876,12 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for name, width in primary_inputs: for name, width in primary_inputs:
if name in clock_inputs: if name in clock_inputs:
print(" wire [%d:0] PI_%s = clock;" % (width-1, name), file=f) print(" wire [%d:0] %s = clock;" % (width-1, escape_identifier("PI_"+name)), file=f)
else: else:
print(" reg [%d:0] PI_%s;" % (width-1, name), file=f) print(" reg [%d:0] %s;" % (width-1, escape_identifier("PI_"+name)), file=f)
print(" %s UUT (" % vlogtb_topmod, file=f) print(" %s UUT (" % escape_identifier(vlogtb_topmod), file=f)
print(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f) print(",\n".join(" .%s(%s)" % (escape_identifier(name), escape_identifier("PI_"+name)) for name, _ in primary_inputs), file=f)
print(" );", file=f) print(" );", file=f)
print("`ifndef VERILATOR", file=f) print("`ifndef VERILATOR", file=f)
@ -893,14 +911,14 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for n in reg: for n in reg:
if n.startswith("$"): if n.startswith("$"):
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(escape_identifier(reg)), len(val), val), file=f)
anyconsts = sorted(smt.hieranyconsts(vlogtb_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(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(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(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);
mems = sorted(smt.hiermems(vlogtb_topmod)) mems = sorted(smt.hiermems(vlogtb_topmod))
for mempath in mems: for mempath in mems:
@ -924,7 +942,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
addr_data[addr] = data addr_data[addr] = data
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(escape_identifier(mempath)), len(addr), addr, len(data), data), file=f)
print("", file=f) print("", file=f)
anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod)) anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))
@ -940,18 +958,18 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
for name, val in zip(pi_names, pi_values): for name, val in zip(pi_names, pi_values):
if i > 0: if i > 0:
print(" PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f) print(" %s <= %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f)
else: else:
print(" PI_%s = %d'b%s;" % (".".join(name), len(val), val), file=f) print(" %s = %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f)
for info in anyseqs: for info in anyseqs:
if info[3] is not None: if info[3] is not None:
modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(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)))
if i > 0: if i > 0:
print(" UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f); print(" UUT.%s <= %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);
else: else:
print(" UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f); print(" UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);
if i > 0: if i > 0:
print(" end", file=f) print(" end", file=f)