diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/btor/btor.cc | 22 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 105 | ||||
| -rw-r--r-- | backends/verilog/verilog_backend.cc | 2 |
3 files changed, 119 insertions, 10 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 58d2a8625..ab2702807 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -506,6 +506,18 @@ struct BtorWorker } } + Const initval; + for (int i = 0; i < GetSize(sig_q); i++) + if (initbits.count(sig_q[i])) + initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); + else + initval.bits.push_back(State::Sx); + + int nid_init_val = -1; + + if (!initval.is_fully_undef()) + nid_init_val = get_sig_nid(initval); + int sid = get_bv_sid(GetSize(sig_q)); int nid = next_nid++; @@ -514,15 +526,7 @@ struct BtorWorker else btorf("%d state %d %s\n", nid, sid, log_id(symbol)); - Const initval; - for (int i = 0; i < GetSize(sig_q); i++) - if (initbits.count(sig_q[i])) - initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); - else - initval.bits.push_back(State::Sx); - - if (!initval.is_fully_undef()) { - int nid_init_val = get_sig_nid(initval); + if (nid_init_val >= 0) { int nid_init = next_nid++; if (verbose) btorf("; initval = %s\n", log_signal(initval)); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index b944ee004..721a395e3 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -32,6 +32,7 @@ cexfile = None aimfile = None aiwfile = None aigheader = True +btorwitfile = None vlogtbfile = None vlogtbtop = None inconstr = list() @@ -92,6 +93,9 @@ yosys-smtbmc [options] <yosys_smt2_output> the AIGER witness file does not include the status and properties lines. + --btorwit <btor_witness_filename> + read a BTOR witness. + --noinfo only run the core proof, do not collect and print any additional information (e.g. which assert failed) @@ -152,7 +156,7 @@ yosys-smtbmc [options] <yosys_smt2_output> try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat", + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat", "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "smtc-init", "smtc-top=", "noinit"]) except: @@ -189,6 +193,8 @@ for o, a in opts: aiwfile = a + ".aiw" elif o == "--aig-noheader": aigheader = False + elif o == "--btorwit": + btorwitfile = a elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -575,6 +581,103 @@ if aimfile is not None: num_steps = max(num_steps, step+1) step += 1 +if btorwitfile is not None: + with open(btorwitfile, "r") as f: + step = None + suffix = None + altsuffix = None + header_okay = False + + for line in f: + line = line.strip() + + if line == "sat": + header_okay = True + continue + + if not header_okay: + continue + + if line == "" or line[0] == "b" or line[0] == "j": + continue + + if line == ".": + break + + if line[0] == '#' or line[0] == '@': + step = int(line[1:]) + suffix = line + altsuffix = suffix + if suffix[0] == "@": + altsuffix = "#" + suffix[1:] + else: + altsuffix = "@" + suffix[1:] + continue + + line = line.split() + + if len(line) == 0: + continue + + if line[-1].endswith(suffix): + line[-1] = line[-1][0:len(line[-1]) - len(suffix)] + + if line[-1].endswith(altsuffix): + line[-1] = line[-1][0:len(line[-1]) - len(altsuffix)] + + if line[-1][0] == "$": + continue + + # BV assignments + if len(line) == 3 and line[1][0] != "[": + value = line[1] + name = line[2] + + path = smt.get_path(topmod, name) + + if not smt.net_exists(topmod, path): + continue + + width = smt.net_width(topmod, path) + + if width == 1: + assert value in ["0", "1"] + value = "true" if value == "1" else "false" + else: + value = "#b" + value + + smtexpr = "(= [%s] %s)" % (name, value) + constr_assumes[step].append((btorwitfile, smtexpr)) + + # Array assignments + if len(line) == 4 and line[1][0] == "[": + index = line[1] + value = line[2] + name = line[3] + + path = smt.get_path(topmod, name) + + if not smt.mem_exists(topmod, path): + continue + + meminfo = smt.mem_info(topmod, path) + + if meminfo[1] == 1: + assert value in ["0", "1"] + value = "true" if value == "1" else "false" + else: + value = "#b" + value + + assert index[0] == "[" + assert index[-1] == "]" + index = "#b" + index[1:-1] + + smtexpr = "(= (select [%s] %s) %s)" % (name, index, value) + constr_assumes[step].append((btorwitfile, smtexpr)) + + skip_steps = step + num_steps = step+1 + def write_vcd_trace(steps_start, steps_stop, index): filename = vcdfile.replace("%", index) print_msg("Writing trace to VCD file: %s" % (filename)) diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 850abfad7..3a47b478f 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -1352,6 +1352,8 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo if (sync->type == RTLIL::STa) { f << stringf("%s" "always @* begin\n", indent.c_str()); + } else if (sync->type == RTLIL::STi) { + f << stringf("%s" "initial begin\n", indent.c_str()); } else { f << stringf("%s" "always @(", indent.c_str()); if (sync->type == RTLIL::STp || sync->type == RTLIL::ST1) |