From 54166ae0c59dd7fd53466fd2cca0d84c6c5d44b1 Mon Sep 17 00:00:00 2001 From: Jakob Wenzel Date: Tue, 6 Oct 2020 11:24:29 +0200 Subject: [PATCH] smtbmc: escape identifiers in verilog testbench --- backends/smt2/smtbmc.py | 40 +++++++++++++++++++++++++++++----------- 1 file changed, 29 insertions(+), 11 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 69dab5590..da5a7f57e 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -817,6 +817,24 @@ def write_vcd_trace(steps_start, steps_stop, index): 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): filename = vlogtbfile.replace("%", index) @@ -858,12 +876,12 @@ def write_vlogtb_trace(steps_start, steps_stop, index): for name, width in primary_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: - 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(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f) + print(" %s UUT (" % escape_identifier(vlogtb_topmod), 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("`ifndef VERILATOR", file=f) @@ -893,14 +911,14 @@ def write_vlogtb_trace(steps_start, steps_stop, index): for n in reg: if n.startswith("$"): 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)) for info in anyconsts: if info[3] is not None: 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))) - 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)) for mempath in mems: @@ -924,7 +942,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index): addr_data[addr] = data 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) 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): 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: - 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: if info[3] is not None: 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))) 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: - 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: print(" end", file=f) -- 2.30.2