sbysrc/sby_engine_aiger.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     opts, solver_args = getopt.getopt(engine[1:], "", [])
  24
  25     if len(solver_args) == 0:
  26         task.error("Missing solver command.")
  27
  28     for o, a in opts:
  29         task.error("Unexpected AIGER engine options.")
  30
  31     status_2 = "UNKNOWN"
  32
  33     if solver_args[0] == "suprove":
  34         if mode not in ["live", "prove"]:
  35             task.error("The aiger solver 'suprove' is only supported in live and prove modes.")
  36         if mode == "live" and (len(solver_args) == 1 or solver_args[1][0] != "+"):
  37             solver_args.insert(1, "+simple_liveness")
  38         solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:])
  39
  40     elif solver_args[0] == "avy":
  41         if mode != "prove":
  42             task.error("The aiger solver 'avy' is only supported in prove mode.")
  43         solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:])
  44
  45     elif solver_args[0] == "aigbmc":
  46         if mode != "bmc":
  47             task.error("The aiger solver 'aigbmc' is only supported in bmc mode.")
  48         solver_cmd = " ".join([task.exe_paths["aigbmc"], str(task.opt_depth - 1)] + solver_args[1:])
  49         status_2 = "PASS"  # aigbmc outputs status 2 when BMC passes
  50
  51     else:
  52         task.error(f"Invalid solver command {solver_args[0]}.")
  53
  54     proc = SbyProc(
  55         task,
  56         f"engine_{engine_idx}",
  57         task.model("aig"),
  58         f"cd {task.workdir}; {solver_cmd} model/design_aiger.aig",
  59         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
  60     )
  61
  62     proc_status = None
  63     produced_cex = False
  64     end_of_cex = False
  65     aiw_file = open(f"{task.workdir}/engine_{engine_idx}/trace.aiw", "w")
  66
  67     def output_callback(line):
  68         nonlocal proc_status
  69         nonlocal produced_cex
  70         nonlocal end_of_cex
  71
  72         if proc_status is not None:
  73             if not end_of_cex and not produced_cex and line.isdigit():
  74                 produced_cex = True
  75             if not end_of_cex:
  76                 print(line, file=aiw_file)
  77             if line == ".":
  78                 end_of_cex = True
  79             return None
  80
  81         if line.startswith("u"):
  82             return f"No CEX up to depth {int(line[1:])-1}."
  83
  84         if line in ["0", "1", "2"]:
  85             print(line, file=aiw_file)
  86             if line == "0": proc_status = "PASS"
  87             if line == "1": proc_status = "FAIL"
  88             if line == "2": proc_status = status_2
  89
  90         return None
  91
  92     def exit_callback(retcode):
  93         if solver_args[0] not in ["avy"]:
  94             assert retcode == 0
  95         assert proc_status is not None
  96
  97         aiw_file.close()
  98
  99         task.update_status(proc_status)
 100         task.log(f"engine_{engine_idx}: Status returned by engine: {proc_status}")
 101         task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""")
 102
 103         task.terminate()
 104
 105         if proc_status == "FAIL" and task.opt_aigsmt != "none":
 106             if produced_cex:
 107                 if mode == "live":
 108                     proc2 = SbyProc(
 109                         task,
 110                         f"engine_{engine_idx}",
 111                         task.model("smt2"),
 112                         ("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
 113                              "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
 114                                     (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
 115                                     "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
 116                                     i=engine_idx),
 117                         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
 118                     )
 119                 else:
 120                     proc2 = SbyProc(
 121                         task,
 122                         f"engine_{engine_idx}",
 123                         task.model("smt2"),
 124                         ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
 125                              "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
 126                                     (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
 127                                     "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
 128                                     task.opt_append, i=engine_idx),
 129                         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
 130                     )
 131
 132                 proc2_status = None
 133
 134                 def output_callback2(line):
 135                     nonlocal proc2_status
 136
 137                     match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
 138                     if match: proc2_status = "FAIL"
 139
 140                     match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
 141                     if match: proc2_status = "PASS"
 142
 143                     return line
 144
 145                 def exit_callback2(line):
 146                     assert proc2_status is not None
 147                     if mode == "live":
 148                         assert proc2_status == "PASS"
 149                     else:
 150                         assert proc2_status == "FAIL"
 151
 152                     if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"):
 153                         task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
 154
 155                 proc2.output_callback = output_callback2
 156                 proc2.exit_callback = exit_callback2
 157
 158             else:
 159                 task.log(f"engine_{engine_idx}: Engine did not produce a counter example.")
 160
 161     proc.output_callback = output_callback
 162     proc.exit_callback = exit_callback