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 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" -F {job.opt_depth} -v"
  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" -F {job.opt_depth} -v"
  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(f"Invalid ABC command {abc_command[0]}.")
  47
  48     task = SbyTask(
  49         job,
  50         f"engine_{engine_idx}",
  51         job.model("aig"),
  52         f"""cd {job.workdir}; {job.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
  53         logfile=open(f"{job.workdir}/engine_{engine_idx}/logfile.txt", "w")
  54     )
  55
  56     task.noprintregex = re.compile(r"^\.+$")
  57     task_status = None
  58
  59     def output_callback(line):
  60         nonlocal task_status
  61
  62         match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line)
  63         if match: task_status = "FAIL"
  64
  65         match = re.match(r"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", line)
  66         if match: task_status = "UNKNOWN"
  67
  68         match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line)
  69         if match: task_status = "PASS"
  70
  71         match = re.match(r"^No output asserted in [0-9]+ frames.", line)
  72         if match: task_status = "PASS"
  73
  74         match = re.match(r"^Property proved.", line)
  75         if match: task_status = "PASS"
  76
  77         return line
  78
  79     def exit_callback(retcode):
  80         assert retcode == 0
  81         assert task_status is not None
  82
  83         job.update_status(task_status)
  84         job.log(f"engine_{engine_idx}: Status returned by engine: {task_status}")
  85         job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status}""")
  86
  87         job.terminate()
  88
  89         if task_status == "FAIL" and job.opt_aigsmt != "none":
  90             task2 = SbyTask(
  91                 job,
  92                 f"engine_{engine_idx}",
  93                 job.model("smt2"),
  94                 ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
  95                      "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format
  96                             (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt,
  97                             "" if job.opt_tbtop is None else f" --vlogtb-top {job.opt_tbtop}",
  98                             job.opt_append, i=engine_idx),
  99                 logfile=open(f"{job.workdir}/engine_{engine_idx}/logfile2.txt", "w")
 100             )
 101
 102             task2_status = None
 103
 104             def output_callback2(line):
 105                 nonlocal task2_status
 106
 107                 match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
 108                 if match: task2_status = "FAIL"
 109
 110                 match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
 111                 if match: task2_status = "PASS"
 112
 113                 return line
 114
 115             def exit_callback2(line):
 116                 assert task2_status is not None
 117                 assert task2_status == "FAIL"
 118
 119                 if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
 120                     job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
 121
 122             task2.output_callback = output_callback2
 123             task2.exit_callback = exit_callback2
 124
 125     task.output_callback = output_callback
 126     task.exit_callback = exit_callback