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 SbyTask
23 def run(mode
, job
, engine_idx
, engine
):
26 opts
, solver_args
= getopt
.getopt(engine
[1:], "", ["seed="])
28 if len(solver_args
) == 0:
29 job
.error("Missing solver command.")
35 job
.error("Unexpected BTOR engine options.")
37 if solver_args
[0] == "btormc":
40 solver_cmd
+= f
"BTORSEED={random_seed} "
41 solver_cmd
+= job
.exe_paths
["btormc"] + f
""" --stop-first {0 if mode == "cover" else 1} -v 1 -kmax {job.opt_depth - 1}"""
42 if job
.opt_skip
is not None:
43 solver_cmd
+= f
" -kmin {job.opt_skip}"
44 solver_cmd
+= " ".join([""] + solver_args
[1:])
46 elif solver_args
[0] == "pono":
48 job
.error("Setting the random seed is not available for the pono solver.")
49 solver_cmd
= job
.exe_paths
["pono"] + f
" -v 1 -e bmc -k {job.opt_depth - 1}"
52 job
.error(f
"Invalid solver command {solver_args[0]}.")
54 common_state
= SimpleNamespace()
55 common_state
.solver_status
= None
56 common_state
.produced_cex
= 0
57 common_state
.expected_cex
= 1
58 common_state
.wit_file
= None
59 common_state
.assert_fail
= False
60 common_state
.produced_traces
= []
61 common_state
.print_traces_max
= 5
62 common_state
.running_tasks
= 0
64 def print_traces_and_terminate():
66 if common_state
.assert_fail
:
68 elif common_state
.expected_cex
== 0:
70 elif common_state
.solver_status
== "sat":
72 elif common_state
.solver_status
== "unsat":
75 job
.error(f
"engine_{engine_idx}: Engine terminated without status.")
77 if common_state
.expected_cex
== 0:
79 elif common_state
.solver_status
== "sat":
81 elif common_state
.solver_status
== "unsat":
84 job
.error(f
"engine_{engine_idx}: Engine terminated without status.")
86 job
.update_status(task_status
.upper())
87 job
.log(f
"engine_{engine_idx}: Status returned by engine: {task_status}")
88 job
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status}""")
90 if len(common_state
.produced_traces
) == 0:
91 job
.log(f
"""engine_{engine_idx}: Engine did not produce a{" counter" if mode != "cover" else "n "}example.""")
92 elif len(common_state
.produced_traces
) <= common_state
.print_traces_max
:
93 job
.summary
.extend(common_state
.produced_traces
)
95 job
.summary
.extend(common_state
.produced_traces
[:common_state
.print_traces_max
])
96 excess_traces
= len(common_state
.produced_traces
) - common_state
.print_traces_max
97 job
.summary
.append(f
"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
102 def output_callback2(line
):
103 match
= re
.search(r
"Assert failed in test", line
)
105 common_state
.assert_fail
= True
108 def output_callback2(line
):
111 def make_exit_callback(suffix
):
112 def exit_callback2(retcode
):
115 vcdpath
= f
"{job.workdir}/engine_{engine_idx}/trace{suffix}.vcd"
116 if os
.path
.exists(vcdpath
):
117 common_state
.produced_traces
.append(f
"""{"" if mode == "cover" else "counterexample "}trace: {vcdpath}""")
119 common_state
.running_tasks
-= 1
120 if (common_state
.running_tasks
== 0):
121 print_traces_and_terminate()
123 return exit_callback2
125 def output_callback(line
):
127 if solver_args
[0] == "btormc":
128 match
= re
.search(r
"calling BMC on ([0-9]+) properties", line
)
130 common_state
.expected_cex
= int(match
[1])
131 assert common_state
.produced_cex
== 0
134 job
.error(f
"engine_{engine_idx}: BTOR solver '{solver_args[0]}' is currently not supported in cover mode.")
136 if (common_state
.produced_cex
< common_state
.expected_cex
) and line
== "sat":
137 assert common_state
.wit_file
== None
138 if common_state
.expected_cex
== 1:
139 common_state
.wit_file
= open(f
"{job.workdir}/engine_{engine_idx}/trace.wit", "w")
141 common_state
.wit_file
= open(f
"""{job.workdir}/engine_{engine_idx}/trace{common_state.produced_cex}.wit""", "w")
142 if solver_args
[0] != "btormc":
143 task
.log("Found satisfiability witness.")
145 if common_state
.wit_file
:
146 print(line
, file=common_state
.wit_file
)
148 if common_state
.expected_cex
== 1:
151 suffix
= common_state
.produced_cex
154 f
"engine_{engine_idx}_{common_state.produced_cex}",
156 "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=job
.workdir
, idx
=engine_idx
, i
=suffix
),
157 logfile
=open(f
"{job.workdir}/engine_{engine_idx}/logfile2.txt", "w")
159 task2
.output_callback
= output_callback2
160 task2
.exit_callback
= make_exit_callback(suffix
)
161 task2
.checkretcode
= True
162 common_state
.running_tasks
+= 1
164 common_state
.produced_cex
+= 1
165 common_state
.wit_file
.close()
166 common_state
.wit_file
= None
167 if common_state
.produced_cex
== common_state
.expected_cex
:
168 common_state
.solver_status
= "sat"
171 if solver_args
[0] == "btormc":
172 if "calling BMC on" in line
:
174 if "SATISFIABLE" in line
:
176 if "bad state properties at bound" in line
:
178 if "deleting model checker:" in line
:
179 if common_state
.solver_status
is None:
180 common_state
.solver_status
= "unsat"
183 elif solver_args
[0] == "pono":
184 if line
== "unknown":
185 if common_state
.solver_status
is None:
186 common_state
.solver_status
= "unsat"
187 return "No CEX found."
188 if line
not in ["b0"]:
191 print(line
, file=task
.logfile
)
195 def exit_callback(retcode
):
196 if solver_args
[0] == "pono":
197 assert retcode
in [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2
200 if common_state
.expected_cex
!= 0:
201 assert common_state
.solver_status
is not None
203 if common_state
.solver_status
== "unsat":
204 if common_state
.expected_cex
== 1:
205 with
open(f
"""{job.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
"{job.workdir}/engine_{engine_idx}/trace{i}.wit", "w") as wit_file
:
210 print("unsat", file=wit_file
)
212 common_state
.running_tasks
-= 1
213 if (common_state
.running_tasks
== 0):
214 print_traces_and_terminate()
218 f
"engine_{engine_idx}", job
.model("btor"),
219 f
"cd {job.workdir}; {solver_cmd} model/design_btor.btor",
220 logfile
=open(f
"{job.workdir}/engine_{engine_idx}/logfile.txt", "w")
223 task
.output_callback
= output_callback
224 task
.exit_callback
= exit_callback
225 common_state
.running_tasks
+= 1