sbysrc/sby_engine_abc.py

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