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
):
33 induction_only
= False
36 task
.precise_prop_status
= True
38 opts
, args
= getopt
.getopt(engine
[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
39 "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "keep-going", "seed="])
52 elif o
== "--nopresat":
56 elif o
== "--nounroll":
58 elif o
== "--dumpsmt2":
60 elif o
== "--progress":
62 elif o
== "--basecase":
64 task
.error("smtbmc options --basecase and --induction are exclusive.")
66 elif o
== "--induction":
68 task
.error("smtbmc options --basecase and --induction are exclusive.")
70 elif o
== "--keep-going":
71 if mode
not in ("bmc", "prove", "prove_basecase", "prove_induction"):
72 task
.error("smtbmc option --keep-going is only supported in bmc and prove mode.")
77 task
.error(f
"Invalid smtbmc options {o}.")
80 for i
, a
in enumerate(args
):
81 if i
== 0 and a
== "z3" and unroll_opt
is None:
89 smtbmc_opts
+= ["-s" if i
== 0 else "-S", a
]
92 smtbmc_opts
+= ["--presat"]
94 if unroll_opt
is None or unroll_opt
:
95 smtbmc_opts
+= ["--unroll"]
97 if task
.opt_smtc
is not None:
98 smtbmc_opts
+= ["--smtc", f
"src/{task.opt_smtc}"]
100 if task
.opt_tbtop
is not None:
101 smtbmc_opts
+= ["--vlogtb-top", task
.opt_tbtop
]
104 if syn_opt
: model_name
+= "_syn"
105 if nomem_opt
: model_name
+= "_nomem"
106 if stbv_opt
: model_name
+= "_stbv"
107 if stdt_opt
: model_name
+= "_stdt"
110 if not induction_only
:
111 run("prove_basecase", task
, engine_idx
, engine
)
112 if not basecase_only
:
113 run("prove_induction", task
, engine_idx
, engine
)
116 procname
= f
"engine_{engine_idx}"
117 trace_prefix
= f
"engine_{engine_idx}/trace"
118 logfile_prefix
= f
"{task.workdir}/engine_{engine_idx}/logfile"
120 if mode
== "prove_basecase":
121 procname
+= ".basecase"
122 logfile_prefix
+= "_basecase"
124 if mode
== "prove_induction":
125 procname
+= ".induction"
126 trace_prefix
+= "_induct"
127 logfile_prefix
+= "_induction"
128 smtbmc_opts
.append("-i")
131 smtbmc_opts
.append("-c")
135 smtbmc_opts
.append("--keep-going")
139 smtbmc_opts
+= ["--dump-smt2", trace_prefix
.replace("%", "") + ".smt2"]
142 smtbmc_opts
.append("--noprogress")
145 if task
.opt_skip
is not None:
146 t_opt
= "{}:{}".format(task
.opt_skip
, task
.opt_depth
)
148 t_opt
= "{}".format(task
.opt_depth
)
150 random_seed
= f
"--info \"(set-option :random-seed {random_seed})\"" if random_seed
else ""
154 task
.model(model_name
),
155 f
"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
156 logfile
=open(logfile_prefix
+ ".txt", "w"),
157 logstderr
=(not progress
)
160 if mode
== "prove_basecase":
161 task
.basecase_procs
.append(proc
)
163 if mode
== "prove_induction":
164 task
.induction_procs
.append(proc
)
169 def output_callback(line
):
173 match
= re
.match(r
"^## [0-9: ]+ Status: FAILED", line
)
176 return line
.replace("FAILED", "failed")
178 match
= re
.match(r
"^## [0-9: ]+ Status: PASSED", line
)
181 return line
.replace("PASSED", "passed")
183 match
= re
.match(r
"^## [0-9: ]+ Status: PREUNSAT", line
)
185 proc_status
= "ERROR"
188 match
= re
.match(r
"^## [0-9: ]+ Unexpected response from solver:", line
)
190 proc_status
= "ERROR"
193 match
= re
.match(r
"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line
)
196 prop
= task
.design_hierarchy
.find_property_by_cellname(cell_name
)
201 match
= re
.match(r
"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line
)
204 prop
= task
.design_hierarchy
.find_property_by_cellname(cell_name
)
209 match
= re
.match(r
"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line
)
210 if match
and last_prop
:
211 last_prop
.tracefile
= match
[1]
215 match
= re
.match(r
"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line
)
218 prop
= task
.design_hierarchy
.find_property_by_cellname(cell_name
)
223 def exit_callback(retcode
):
224 if proc_status
is None:
225 task
.error(f
"engine_{engine_idx}: Engine terminated without status.")
227 if mode
== "bmc" or mode
== "cover":
228 task
.update_status(proc_status
)
229 proc_status_lower
= proc_status
.lower() if proc_status
== "PASS" else proc_status
230 task
.log(f
"engine_{engine_idx}: Status returned by engine: {proc_status_lower}")
231 task
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower}""")
233 if proc_status
== "FAIL" and mode
!= "cover":
234 if os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace.vcd"):
235 task
.summary
.append(f
"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
236 elif proc_status
== "PASS" and mode
== "cover":
238 for i
in range(print_traces_max
):
239 if os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace{i}.vcd"):
240 task
.summary
.append(f
"trace: {task.workdir}/engine_{engine_idx}/trace{i}.vcd")
245 while os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace{print_traces_max + excess_traces}.vcd"):
247 if excess_traces
> 0:
248 task
.summary
.append(f
"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
249 elif proc_status
== "PASS" and mode
== "bmc":
250 for prop
in task
.design_hierarchy
:
251 if prop
.type == prop
.Type
.ASSERT
and prop
.status
== "UNKNOWN":
256 elif mode
in ["prove_basecase", "prove_induction"]:
257 proc_status_lower
= proc_status
.lower() if proc_status
== "PASS" else proc_status
258 task
.log(f
"""engine_{engine_idx}: Status returned by engine for {mode.split("_")[1]}: {proc_status_lower}""")
259 task
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower} for {mode.split("_")[1]}""")
261 if mode
== "prove_basecase":
262 for proc
in task
.basecase_procs
:
265 if proc_status
== "PASS":
266 task
.basecase_pass
= True
269 task
.update_status(proc_status
)
270 if os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace.vcd"):
271 task
.summary
.append(f
"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
274 elif mode
== "prove_induction":
275 for proc
in task
.induction_procs
:
278 if proc_status
== "PASS":
279 task
.induction_pass
= True
284 if task
.basecase_pass
and task
.induction_pass
:
285 for prop
in task
.design_hierarchy
:
286 if prop
.type == prop
.Type
.ASSERT
and prop
.status
== "UNKNOWN":
288 task
.update_status("PASS")
289 task
.summary
.append("successful proof by k-induction.")
295 proc
.output_callback
= output_callback
296 proc
.exit_callback
= exit_callback