sbysrc/sby_engine_smtbmc.py

   1 #
   2 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
   3 #
   4 # Copyright (C) 2016  Clifford Wolf <clifford@clifford.at>
   5 #
   6 # Permission to use, copy, modify, and/or distribute this software for any
   7 # purpose with or without fee is hereby granted, provided that the above
   8 # copyright notice and this permission notice appear in all copies.
   9 #
  10 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17 #
  18
  19 import re, os, getopt
  20 from sby_core import SbyTask
  21
  22 def run(mode, job, engine_idx, engine):
  23     smtbmc_opts = []
  24     nomem_opt = False
  25     presat_opt = True
  26     unroll_opt = None
  27     syn_opt = False
  28     stbv_opt = False
  29     stdt_opt = False
  30     dumpsmt2 = False
  31     progress = False
  32     basecase_only = False
  33     induction_only = False
  34     random_seed = None
  35
  36     opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
  37             "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
  38
  39     for o, a in opts:
  40         if o == "--nomem":
  41             nomem_opt = True
  42         elif o == "--syn":
  43             syn_opt = True
  44         elif o == "--stbv":
  45             stbv_opt = True
  46         elif o == "--stdt":
  47             stdt_opt = True
  48         elif o == "--presat":
  49             presat_opt = True
  50         elif o == "--nopresat":
  51             presat_opt = False
  52         elif o == "--unroll":
  53             unroll_opt = True
  54         elif o == "--nounroll":
  55             unroll_opt = False
  56         elif o == "--dumpsmt2":
  57             dumpsmt2 = True
  58         elif o == "--progress":
  59             progress = True
  60         elif o == "--basecase":
  61             if induction_only:
  62                 job.error("smtbmc options --basecase and --induction are exclusive.")
  63             basecase_only = True
  64         elif o == "--induction":
  65             if basecase_only:
  66                 job.error("smtbmc options --basecase and --induction are exclusive.")
  67             induction_only = True
  68         elif o == "--seed":
  69             random_seed = a
  70         else:
  71             job.error(f"Invalid smtbmc options {o}.")
  72
  73     xtra_opts = False
  74     for i, a in enumerate(args):
  75         if i == 0 and a == "z3" and unroll_opt is None:
  76                 unroll_opt = False
  77         if a == "--":
  78             xtra_opts = True
  79             continue
  80         if xtra_opts:
  81             smtbmc_opts.append(a)
  82         else:
  83             smtbmc_opts += ["-s" if i == 0 else "-S", a]
  84
  85     if presat_opt:
  86         smtbmc_opts += ["--presat"]
  87
  88     if unroll_opt is None or unroll_opt:
  89         smtbmc_opts += ["--unroll"]
  90
  91     if job.opt_smtc is not None:
  92         smtbmc_opts += ["--smtc", f"src/{job.opt_smtc}"]
  93
  94     if job.opt_tbtop is not None:
  95          smtbmc_opts += ["--vlogtb-top", job.opt_tbtop]
  96
  97     model_name = "smt2"
  98     if syn_opt: model_name += "_syn"
  99     if nomem_opt: model_name += "_nomem"
 100     if stbv_opt: model_name += "_stbv"
 101     if stdt_opt: model_name += "_stdt"
 102
 103     if mode == "prove":
 104         if not induction_only:
 105             run("prove_basecase", job, engine_idx, engine)
 106         if not basecase_only:
 107             run("prove_induction", job, engine_idx, engine)
 108         return
 109
 110     taskname = f"engine_{engine_idx}"
 111     trace_prefix = f"engine_{engine_idx}/trace"
 112     logfile_prefix = f"{job.workdir}/engine_{engine_idx}/logfile"
 113
 114     if mode == "prove_basecase":
 115         taskname += ".basecase"
 116         logfile_prefix += "_basecase"
 117
 118     if mode == "prove_induction":
 119         taskname += ".induction"
 120         trace_prefix += "_induct"
 121         logfile_prefix += "_induction"
 122         smtbmc_opts.append("-i")
 123
 124     if mode == "cover":
 125         smtbmc_opts.append("-c")
 126         trace_prefix += "%"
 127
 128     if dumpsmt2:
 129         smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]
 130
 131     if not progress:
 132         smtbmc_opts.append("--noprogress")
 133
 134
 135     if job.opt_skip is not None:
 136         t_opt = "{}:{}".format(job.opt_skip, job.opt_depth)
 137     else:
 138         t_opt = "{}".format(job.opt_depth)
 139
 140     random_seed = f"--info \"(set-option :random-seed {random_seed})\"" if random_seed else ""
 141     task = SbyTask(
 142         job,
 143         taskname,
 144         job.model(model_name),
 145         f"""cd {job.workdir}; {job.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {job.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
 146         logfile=open(logfile_prefix + ".txt", "w"),
 147         logstderr=(not progress)
 148     )
 149
 150     if mode == "prove_basecase":
 151         job.basecase_tasks.append(task)
 152
 153     if mode == "prove_induction":
 154         job.induction_tasks.append(task)
 155
 156     task_status = None
 157
 158     def output_callback(line):
 159         nonlocal task_status
 160
 161         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
 162         if match:
 163             task_status = "FAIL"
 164             return line.replace("FAILED", "failed")
 165
 166         match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
 167         if match:
 168             task_status = "PASS"
 169             return line.replace("PASSED", "passed")
 170
 171         match = re.match(r"^## [0-9: ]+ Status: PREUNSAT", line)
 172         if match:
 173             task_status = "ERROR"
 174             return line
 175
 176         match = re.match(r"^## [0-9: ]+ Unexpected response from solver:", line)
 177         if match:
 178             task_status = "ERROR"
 179             return line
 180
 181         return line
 182
 183     def exit_callback(retcode):
 184         if task_status is None:
 185             job.error(f"engine_{engine_idx}: Engine terminated without status.")
 186
 187         if mode == "bmc" or mode == "cover":
 188             job.update_status(task_status)
 189             task_status_lower = task_status.lower() if task_status == "PASS" else task_status
 190             job.log(f"engine_{engine_idx}: Status returned by engine: {task_status_lower}")
 191             job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status_lower}""")
 192
 193             if task_status == "FAIL" and mode != "cover":
 194                 if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
 195                     job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
 196             elif task_status == "PASS" and mode == "cover":
 197                 print_traces_max = 5
 198                 for i in range(print_traces_max):
 199                     if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace{i}.vcd"):
 200                         job.summary.append(f"trace: {job.workdir}/engine_{engine_idx}/trace{i}.vcd")
 201                     else:
 202                         break
 203                 else:
 204                     excess_traces = 0
 205                     while os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace{print_traces_max + excess_traces}.vcd"):
 206                         excess_traces += 1
 207                     if excess_traces > 0:
 208                         job.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
 209
 210             job.terminate()
 211
 212         elif mode in ["prove_basecase", "prove_induction"]:
 213             task_status_lower = task_status.lower() if task_status == "PASS" else task_status
 214             job.log(f"""engine_{engine_idx}: Status returned by engine for {mode.split("_")[1]}: {task_status_lower}""")
 215             job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status_lower} for {mode.split("_")[1]}""")
 216
 217             if mode == "prove_basecase":
 218                 for task in job.basecase_tasks:
 219                     task.terminate()
 220
 221                 if task_status == "PASS":
 222                     job.basecase_pass = True
 223
 224                 else:
 225                     job.update_status(task_status)
 226                     if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
 227                         job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
 228                     job.terminate()
 229
 230             elif mode == "prove_induction":
 231                 for task in job.induction_tasks:
 232                     task.terminate()
 233
 234                 if task_status == "PASS":
 235                     job.induction_pass = True
 236
 237             else:
 238                 assert False
 239
 240             if job.basecase_pass and job.induction_pass:
 241                 job.update_status("PASS")
 242                 job.summary.append("successful proof by k-induction.")
 243                 job.terminate()
 244
 245         else:
 246             assert False
 247
 248     task.output_callback = output_callback
 249     task.exit_callback = exit_callback