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