46656915eb49d5015cf5c01a5601cb06c5bc99b8
2 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
4 # Copyright (C) 2016 Claire Xenia Wolf <claire@yosyshq.com>
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.
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.
20 from sby_core
import SbyProc
22 def run(mode
, task
, engine_idx
, engine
):
23 opts
, solver_args
= getopt
.getopt(engine
[1:], "", [])
25 if len(solver_args
) == 0:
26 task
.error("Missing solver command.")
29 task
.error("Unexpected AIGER engine options.")
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:])
36 elif solver_args
[0] == "avy":
37 solver_cmd
= " ".join([task
.exe_paths
["avy"], "--cex", "-"] + solver_args
[1:])
39 elif solver_args
[0] == "aigbmc":
40 solver_cmd
= " ".join([task
.exe_paths
["aigbmc"]] + solver_args
[1:])
43 task
.error(f
"Invalid solver command {solver_args[0]}.")
47 f
"engine_{engine_idx}",
49 f
"cd {task.workdir}; {solver_cmd} model/design_aiger.aig",
50 logfile
=open(f
"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
56 aiw_file
= open(f
"{task.workdir}/engine_{engine_idx}/trace.aiw", "w")
58 def output_callback(line
):
63 if proc_status
is not None:
64 if not end_of_cex
and not produced_cex
and line
.isdigit():
67 print(line
, file=aiw_file
)
72 if line
.startswith("u"):
73 return f
"No CEX up to depth {int(line[1:])-1}."
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"
83 def exit_callback(retcode
):
84 if solver_args
[0] not in ["avy"]:
86 assert proc_status
is not None
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}""")
96 if proc_status
== "FAIL" and task
.opt_aigsmt
!= "none":
101 f
"engine_{engine_idx}",
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}",
108 logfile
=open(f
"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
113 f
"engine_{engine_idx}",
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")
125 def output_callback2(line
):
126 nonlocal proc2_status
128 match
= re
.match(r
"^## [0-9: ]+ Status: FAILED", line
)
129 if match
: proc2_status
= "FAIL"
131 match
= re
.match(r
"^## [0-9: ]+ Status: PASSED", line
)
132 if match
: proc2_status
= "PASS"
136 def exit_callback2(line
):
137 assert proc2_status
is not None
139 assert proc2_status
== "PASS"
141 assert proc2_status
== "FAIL"
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")
146 proc2
.output_callback
= output_callback2
147 proc2
.exit_callback
= exit_callback2
150 task
.log(f
"engine_{engine_idx}: Engine did not produce a counter example.")
152 proc
.output_callback
= output_callback
153 proc
.exit_callback
= exit_callback