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     syn_opt = False
  26
  27     opts, args = getopt.getopt(engine[1:], "s:", ["nomem", "syn"])
  28
  29     for o, a in opts:
  30         if o == "--nomem":
  31             nomem_opt = True
  32         elif o == "--syn":
  33             syn_opt = True
  34         else:
  35             assert False
  36
  37     for i, a in enumerate(args):
  38         smtbmc_opts += ["-s" if i == 0 else "-S", a]
  39
  40     model_name = "smt2"
  41     if syn_opt: model_name += "_syn"
  42     if nomem_opt: model_name += "_nomem"
  43
  44     if mode == "prove":
  45         run("prove_basecase", job, engine_idx, engine)
  46         run("prove_induction", job, engine_idx, engine)
  47         return
  48
  49     taskname = "engine_%d" % engine_idx
  50     trace_prefix = "engine_%d/trace" % engine_idx
  51     logfile_prefix = "%s/engine_%d/logfile" % (job.workdir, engine_idx)
  52
  53     if mode == "prove_basecase":
  54         taskname += ".basecase"
  55         logfile_prefix += "_basecase"
  56
  57     if mode == "prove_induction":
  58         taskname += ".induction"
  59         trace_prefix += "_induct"
  60         logfile_prefix += "_induction"
  61         smtbmc_opts.append("-i")
  62
  63     if mode == "cover":
  64         smtbmc_opts.append("-c")
  65         trace_prefix += "%"
  66
  67     task = SbyTask(job, taskname, job.model(model_name),
  68             "cd %s; %s --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
  69                     (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix, model_name),
  70             logfile=open(logfile_prefix + ".txt", "w"))
  71
  72     if mode == "prove_basecase":
  73         job.basecase_tasks.append(task)
  74
  75     if mode == "prove_induction":
  76         job.induction_tasks.append(task)
  77
  78     task_status = None
  79
  80     def output_callback(line):
  81         nonlocal task_status
  82
  83         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
  84         if match: task_status = "FAIL"
  85
  86         match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
  87         if match: task_status = "PASS"
  88
  89         return line
  90
  91     def exit_callback(retcode):
  92         assert task_status is not None
  93
  94         if mode == "bmc" or mode == "cover":
  95             job.update_status(task_status)
  96             job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
  97             job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status))
  98
  99             if task_status == "FAIL" and mode != "cover":
 100                 job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 101
 102             job.terminate()
 103
 104         elif mode in ["prove_basecase", "prove_induction"]:
 105             job.log("engine_%d: Status returned by engine for %s: %s" % (engine_idx, mode.split("_")[1], task_status))
 106             job.summary.append("engine_%d (%s) returned %s for %s" % (engine_idx, " ".join(engine), task_status, mode.split("_")[1]))
 107
 108             if mode == "prove_basecase":
 109                 for task in job.basecase_tasks:
 110                     task.terminate()
 111
 112                 if task_status == "PASS":
 113                     job.basecase_pass = True
 114
 115                 else:
 116                     job.update_status(task_status)
 117                     job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 118                     job.terminate()
 119
 120             elif mode == "prove_induction":
 121                 for task in job.induction_tasks:
 122                     task.terminate()
 123
 124                 if task_status == "PASS":
 125                     job.induction_pass = True
 126
 127             else:
 128                 assert False
 129
 130             if job.basecase_pass and job.induction_pass:
 131                 job.update_status("PASS")
 132                 job.summary.append("successful proof by k-induction.")
 133                 job.terminate()
 134
 135         else:
 136             assert False
 137
 138     task.output_callback = output_callback
 139     task.exit_callback = exit_callback
 140
 141