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 types
import SimpleNamespace
21 from sby_core
import SbyProc
23 def run(mode
, task
, engine_idx
, engine
):
26 opts
, solver_args
= getopt
.getopt(engine
[1:], "", ["seed="])
28 if len(solver_args
) == 0:
29 task
.error("Missing solver command.")
35 task
.error("Unexpected BTOR engine options.")
37 if solver_args
[0] == "btormc":
40 solver_cmd
+= f
"BTORSEED={random_seed} "
41 solver_cmd
+= task
.exe_paths
["btormc"] + f
""" --stop-first {0 if mode == "cover" else 1} -v 1 -kmax {task.opt_depth - 1}"""
42 if task
.opt_skip
is not None:
43 solver_cmd
+= f
" -kmin {task.opt_skip}"
44 solver_cmd
+= " ".join([""] + solver_args
[1:])
46 elif solver_args
[0] == "pono":
48 task
.error("Setting the random seed is not available for the pono solver.")
49 if task
.opt_skip
is not None:
50 task
.error("The btor engine supports the option skip only for the btormc solver.")
51 solver_cmd
= task
.exe_paths
["pono"] + f
" --witness -v 1 -e bmc -k {task.opt_depth - 1}"
52 solver_cmd
+= " ".join([""] + solver_args
[1:])
55 task
.error(f
"Invalid solver command {solver_args[0]}.")
57 common_state
= SimpleNamespace()
58 common_state
.solver_status
= None
59 common_state
.produced_cex
= 0
60 common_state
.expected_cex
= 1
61 common_state
.wit_file
= None
62 common_state
.assert_fail
= False
63 common_state
.produced_traces
= []
64 common_state
.print_traces_max
= 5
65 common_state
.running_procs
= 0
67 def print_traces_and_terminate():
69 if common_state
.assert_fail
:
71 elif common_state
.expected_cex
== 0:
73 elif common_state
.solver_status
== "sat":
75 elif common_state
.solver_status
== "unsat":
78 task
.error(f
"engine_{engine_idx}: Engine terminated without status.")
80 if common_state
.expected_cex
== 0:
82 elif common_state
.solver_status
== "sat":
84 elif common_state
.solver_status
== "unsat":
87 task
.error(f
"engine_{engine_idx}: Engine terminated without status.")
89 task
.update_status(proc_status
.upper())
90 task
.log(f
"engine_{engine_idx}: Status returned by engine: {proc_status}")
91 task
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""")
93 if len(common_state
.produced_traces
) == 0:
94 task
.log(f
"""engine_{engine_idx}: Engine did not produce a{" counter" if mode != "cover" else "n "}example.""")
95 elif len(common_state
.produced_traces
) <= common_state
.print_traces_max
:
96 task
.summary
.extend(common_state
.produced_traces
)
98 task
.summary
.extend(common_state
.produced_traces
[:common_state
.print_traces_max
])
99 excess_traces
= len(common_state
.produced_traces
) - common_state
.print_traces_max
100 task
.summary
.append(f
"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
105 def output_callback2(line
):
106 match
= re
.search(r
"Assert failed in test", line
)
108 common_state
.assert_fail
= True
111 def output_callback2(line
):
114 def make_exit_callback(suffix
):
115 def exit_callback2(retcode
):
116 vcdpath
= f
"{task.workdir}/engine_{engine_idx}/trace{suffix}.vcd"
117 if os
.path
.exists(vcdpath
):
118 common_state
.produced_traces
.append(f
"""{"" if mode == "cover" else "counterexample "}trace: {vcdpath}""")
120 common_state
.running_procs
-= 1
121 if (common_state
.running_procs
== 0):
122 print_traces_and_terminate()
124 return exit_callback2
126 def output_callback(line
):
128 if solver_args
[0] == "btormc":
129 match
= re
.search(r
"calling BMC on ([0-9]+) properties", line
)
131 common_state
.expected_cex
= int(match
[1])
132 if common_state
.produced_cex
!= 0:
133 task
.error(f
"engine_{engine_idx}: Unexpected engine output (property count).")
136 task
.error(f
"engine_{engine_idx}: BTOR solver '{solver_args[0]}' is currently not supported in cover mode.")
138 if (common_state
.produced_cex
< common_state
.expected_cex
) and line
== "sat":
139 if common_state
.wit_file
!= None:
140 task
.error(f
"engine_{engine_idx}: Unexpected engine output (sat).")
141 if common_state
.expected_cex
== 1:
142 common_state
.wit_file
= open(f
"{task.workdir}/engine_{engine_idx}/trace.wit", "w")
144 common_state
.wit_file
= open(f
"""{task.workdir}/engine_{engine_idx}/trace{common_state.produced_cex}.wit""", "w")
145 if solver_args
[0] != "btormc":
146 proc
.log("Found satisfiability witness.")
148 if common_state
.wit_file
:
149 print(line
, file=common_state
.wit_file
)
151 if common_state
.expected_cex
== 1:
154 suffix
= common_state
.produced_cex
157 f
"engine_{engine_idx}_{common_state.produced_cex}",
159 "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor{s}.info model/design_btor{s}.btor engine_{idx}/trace{i}.wit".format(dir=task
.workdir
, idx
=engine_idx
, i
=suffix
, s
='_single' if solver_args
[0] == 'pono' else ''),
160 logfile
=open(f
"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
162 proc2
.output_callback
= output_callback2
163 proc2
.exit_callback
= make_exit_callback(suffix
)
164 proc2
.checkretcode
= True
165 common_state
.running_procs
+= 1
167 common_state
.produced_cex
+= 1
168 common_state
.wit_file
.close()
169 common_state
.wit_file
= None
170 if common_state
.produced_cex
== common_state
.expected_cex
:
171 common_state
.solver_status
= "sat"
174 if solver_args
[0] == "btormc":
175 if "calling BMC on" in line
:
177 if "SATISFIABLE" in line
:
179 if "bad state properties at bound" in line
:
181 if "deleting model checker:" in line
:
182 if common_state
.solver_status
is None:
183 common_state
.solver_status
= "unsat"
186 elif solver_args
[0] == "pono":
187 if line
== "unknown":
188 if common_state
.solver_status
is None:
189 common_state
.solver_status
= "unsat"
190 return "No CEX found."
191 if line
not in ["b0"]:
194 print(line
, file=proc
.logfile
)
198 def exit_callback(retcode
):
199 if common_state
.expected_cex
!= 0:
200 if common_state
.solver_status
is None:
201 task
.error(f
"engine_{engine_idx}: Could not determine engine status.")
203 if common_state
.solver_status
== "unsat":
204 if common_state
.expected_cex
== 1:
205 with
open(f
"""{task.workdir}/engine_{engine_idx}/trace.wit""", "w") as wit_file
:
206 print("unsat", file=wit_file
)
208 for i
in range(common_state
.produced_cex
, common_state
.expected_cex
):
209 with
open(f
"{task.workdir}/engine_{engine_idx}/trace{i}.wit", "w") as wit_file
:
210 print("unsat", file=wit_file
)
212 common_state
.running_procs
-= 1
213 if (common_state
.running_procs
== 0):
214 print_traces_and_terminate()
218 f
"engine_{engine_idx}", task
.model("btor"),
219 f
"cd {task.workdir}; {solver_cmd} model/design_btor{'_single' if solver_args[0]=='pono' else ''}.btor",
220 logfile
=open(f
"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
222 proc
.checkretcode
= True
223 if solver_args
[0] == "pono":
224 proc
.retcodes
= [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2
225 proc
.output_callback
= output_callback
226 proc
.exit_callback
= exit_callback
227 common_state
.running_procs
+= 1