sbysrc/sby_engine_abc.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     abc_opts, abc_command = getopt.getopt(engine[1:], "", [])
  24
  25     if len(abc_command) == 0:
  26         job.error("Missing ABC command.")
  27
  28     for o, a in abc_opts:
  29         job.error("Unexpected ABC engine options.")
  30
  31     if abc_command[0] == "bmc3":
  32         if mode != "bmc":
  33             job.error("ABC command 'bmc3' is only valid in bmc mode.")
  34         abc_command[0] += " -F %d -v" % job.opt_depth
  35
  36     elif abc_command[0] == "sim3":
  37         if mode != "bmc":
  38             job.error("ABC command 'sim3' is only valid in bmc mode.")
  39         abc_command[0] += " -F %d -v" % job.opt_depth
  40
  41     elif abc_command[0] == "pdr":
  42         if mode != "prove":
  43             job.error("ABC command 'pdr' is only valid in prove mode.")
  44
  45     else:
  46         job.error("Invalid ABC command %s." % abc_command[0])
  47
  48     task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
  49             ("cd %s; %s -c 'read_aiger model/design_aiger.aig; fold; strash; %s; write_cex -a engine_%d/trace.aiw'") %
  50             (job.workdir, job.exe_paths["abc"], " ".join(abc_command), engine_idx),
  51             logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
  52
  53     task.noprintregex = re.compile(r"^\.+$")
  54     task_status = None
  55
  56     def output_callback(line):
  57         nonlocal task_status
  58
  59         match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line)
  60         if match: task_status = "FAIL"
  61
  62         match = re.match(r"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", line)
  63         if match: task_status = "UNKNOWN"
  64
  65         match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line)
  66         if match: task_status = "PASS"
  67
  68         match = re.match(r"^No output asserted in [0-9]+ frames.", line)
  69         if match: task_status = "PASS"
  70
  71         match = re.match(r"^Property proved.", line)
  72         if match: task_status = "PASS"
  73
  74         return line
  75
  76     def exit_callback(retcode):
  77         assert retcode == 0
  78         assert task_status is not None
  79
  80         job.update_status(task_status)
  81         job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
  82         job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status))
  83
  84         job.terminate()
  85
  86         if task_status == "FAIL" and job.opt_aigsmt != "none":
  87             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
  88                     ("cd %s; %s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
  89                      "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") %
  90                             (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt,
  91                             "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop,
  92                             job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx),
  93                     logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
  94
  95             task2_status = None
  96
  97             def output_callback2(line):
  98                 nonlocal task2_status
  99
 100                 match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
 101                 if match: task2_status = "FAIL"
 102
 103                 match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
 104                 if match: task2_status = "PASS"
 105
 106                 return line
 107
 108             def exit_callback2(line):
 109                 assert task2_status is not None
 110                 assert task2_status == "FAIL"
 111
 112                 if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)):
 113                     job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 114
 115             task2.output_callback = output_callback2
 116             task2.exit_callback = exit_callback2
 117
 118     task.output_callback = output_callback
 119     task.exit_callback = exit_callback
 120