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
  35     opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
  36             "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction"])
  37
  38     for o, a in opts:
  39         if o == "--nomem":
  40             nomem_opt = True
  41         elif o == "--syn":
  42             syn_opt = True
  43         elif o == "--stbv":
  44             stbv_opt = True
  45         elif o == "--stdt":
  46             stdt_opt = True
  47         elif o == "--presat":
  48             presat_opt = True
  49         elif o == "--nopresat":
  50             presat_opt = False
  51         elif o == "--unroll":
  52             unroll_opt = True
  53         elif o == "--nounroll":
  54             unroll_opt = False
  55         elif o == "--dumpsmt2":
  56             dumpsmt2 = True
  57         elif o == "--progress":
  58             progress = True
  59         elif o == "--basecase":
  60             if induction_only:
  61                 job.error("smtbmc options --basecase and --induction are exclusive.")
  62             basecase_only = True
  63         elif o == "--induction":
  64             if basecase_only:
  65                 job.error("smtbmc options --basecase and --induction are exclusive.")
  66             induction_only = True
  67         else:
  68             job.error("Invalid smtbmc options %s." % o)
  69
  70     xtra_opts = False
  71     for i, a in enumerate(args):
  72         if i == 0 and a == "z3" and unroll_opt is None:
  73                 unroll_opt = False
  74         if a == "--":
  75             xtra_opts = True
  76             continue
  77         if xtra_opts:
  78             smtbmc_opts.append(a)
  79         else:
  80             smtbmc_opts += ["-s" if i == 0 else "-S", a]
  81
  82     if presat_opt:
  83         smtbmc_opts += ["--presat"]
  84
  85     if unroll_opt is None or unroll_opt:
  86         smtbmc_opts += ["--unroll"]
  87
  88     if job.opt_smtc is not None:
  89         smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc]
  90
  91     if job.opt_tbtop is not None:
  92          smtbmc_opts += ["--vlogtb-top", job.opt_tbtop]
  93
  94     model_name = "smt2"
  95     if syn_opt: model_name += "_syn"
  96     if nomem_opt: model_name += "_nomem"
  97     if stbv_opt: model_name += "_stbv"
  98     if stdt_opt: model_name += "_stdt"
  99
 100     if mode == "prove":
 101         if not induction_only:
 102             run("prove_basecase", job, engine_idx, engine)
 103         if not basecase_only:
 104             run("prove_induction", job, engine_idx, engine)
 105         return
 106
 107     taskname = "engine_%d" % engine_idx
 108     trace_prefix = "engine_%d/trace" % engine_idx
 109     logfile_prefix = "%s/engine_%d/logfile" % (job.workdir, engine_idx)
 110
 111     if mode == "prove_basecase":
 112         taskname += ".basecase"
 113         logfile_prefix += "_basecase"
 114
 115     if mode == "prove_induction":
 116         taskname += ".induction"
 117         trace_prefix += "_induct"
 118         logfile_prefix += "_induction"
 119         smtbmc_opts.append("-i")
 120
 121     if mode == "cover":
 122         smtbmc_opts.append("-c")
 123         trace_prefix += "%"
 124
 125     if dumpsmt2:
 126         smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]
 127
 128     if not progress:
 129         smtbmc_opts.append("--noprogress")
 130
 131
 132     if job.opt_skip is not None:
 133         t_opt = "%d:%d" % (job.opt_skip, job.opt_depth)
 134     else:
 135         t_opt = "%d" % job.opt_depth
 136
 137     task = SbyTask(job, taskname, job.model(model_name),
 138             "cd %s; %s %s -t %s --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
 139                     (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),
 140             logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress))
 141
 142     if mode == "prove_basecase":
 143         job.basecase_tasks.append(task)
 144
 145     if mode == "prove_induction":
 146         job.induction_tasks.append(task)
 147
 148     task_status = None
 149
 150     def output_callback(line):
 151         nonlocal task_status
 152
 153         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
 154         if match:
 155             task_status = "FAIL"
 156             return line.replace("FAILED", "failed")
 157
 158         match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
 159         if match:
 160             task_status = "PASS"
 161             return line.replace("PASSED", "passed")
 162
 163         match = re.match(r"^## [0-9: ]+ Status: PREUNSAT", line)
 164         if match:
 165             task_status = "ERROR"
 166             return line
 167
 168         return line
 169
 170     def exit_callback(retcode):
 171         if task_status is None:
 172             job.error("engine_%d: Engine terminated without status." % engine_idx)
 173
 174         if mode == "bmc" or mode == "cover":
 175             job.update_status(task_status)
 176             task_status_lower = task_status.lower() if task_status == "PASS" else task_status
 177             job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status_lower))
 178             job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status_lower))
 179
 180             if task_status == "FAIL" and mode != "cover":
 181                 if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)):
 182                     job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 183
 184             job.terminate()
 185
 186         elif mode in ["prove_basecase", "prove_induction"]:
 187             task_status_lower = task_status.lower() if task_status == "PASS" else task_status
 188             job.log("engine_%d: Status returned by engine for %s: %s" % (engine_idx, mode.split("_")[1], task_status_lower))
 189             job.summary.append("engine_%d (%s) returned %s for %s" % (engine_idx, " ".join(engine), task_status_lower, mode.split("_")[1]))
 190
 191             if mode == "prove_basecase":
 192                 for task in job.basecase_tasks:
 193                     task.terminate()
 194
 195                 if task_status == "PASS":
 196                     job.basecase_pass = True
 197
 198                 else:
 199                     job.update_status(task_status)
 200                     if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)):
 201                         job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 202                     job.terminate()
 203
 204             elif mode == "prove_induction":
 205                 for task in job.induction_tasks:
 206                     task.terminate()
 207
 208                 if task_status == "PASS":
 209                     job.induction_pass = True
 210
 211             else:
 212                 assert False
 213
 214             if job.basecase_pass and job.induction_pass:
 215                 job.update_status("PASS")
 216                 job.summary.append("successful proof by k-induction.")
 217                 job.terminate()
 218
 219         else:
 220             assert False
 221
 222     task.output_callback = output_callback
 223     task.exit_callback = exit_callback
 224
 225