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