492e2a57f01a248c97ec39cb698bfc1b334c4de5
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
35 task
.precise_prop_status
= True
37 opts
, args
= getopt
.getopt(engine
[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
38 "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
51 elif o
== "--nopresat":
55 elif o
== "--nounroll":
57 elif o
== "--dumpsmt2":
59 elif o
== "--progress":
61 elif o
== "--basecase":
63 task
.error("smtbmc options --basecase and --induction are exclusive.")
65 elif o
== "--induction":
67 task
.error("smtbmc options --basecase and --induction are exclusive.")
72 task
.error(f
"Invalid smtbmc options {o}.")
75 for i
, a
in enumerate(args
):
76 if i
== 0 and a
== "z3" and unroll_opt
is None:
84 smtbmc_opts
+= ["-s" if i
== 0 else "-S", a
]
87 smtbmc_opts
+= ["--presat"]
89 if unroll_opt
is None or unroll_opt
:
90 smtbmc_opts
+= ["--unroll"]
92 if task
.opt_smtc
is not None:
93 smtbmc_opts
+= ["--smtc", f
"src/{task.opt_smtc}"]
95 if task
.opt_tbtop
is not None:
96 smtbmc_opts
+= ["--vlogtb-top", task
.opt_tbtop
]
99 if syn_opt
: model_name
+= "_syn"
100 if nomem_opt
: model_name
+= "_nomem"
101 if stbv_opt
: model_name
+= "_stbv"
102 if stdt_opt
: model_name
+= "_stdt"
105 if not induction_only
:
106 run("prove_basecase", task
, engine_idx
, engine
)
107 if not basecase_only
:
108 run("prove_induction", task
, engine_idx
, engine
)
111 procname
= f
"engine_{engine_idx}"
112 trace_prefix
= f
"engine_{engine_idx}/trace"
113 logfile_prefix
= f
"{task.workdir}/engine_{engine_idx}/logfile"
115 if mode
== "prove_basecase":
116 procname
+= ".basecase"
117 logfile_prefix
+= "_basecase"
119 if mode
== "prove_induction":
120 procname
+= ".induction"
121 trace_prefix
+= "_induct"
122 logfile_prefix
+= "_induction"
123 smtbmc_opts
.append("-i")
126 smtbmc_opts
.append("-c")
130 smtbmc_opts
+= ["--dump-smt2", trace_prefix
.replace("%", "") + ".smt2"]
133 smtbmc_opts
.append("--noprogress")
136 if task
.opt_skip
is not None:
137 t_opt
= "{}:{}".format(task
.opt_skip
, task
.opt_depth
)
139 t_opt
= "{}".format(task
.opt_depth
)
141 random_seed
= f
"--info \"(set-option :random-seed {random_seed})\"" if random_seed
else ""
145 task
.model(model_name
),
146 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""",
147 logfile
=open(logfile_prefix
+ ".txt", "w"),
148 logstderr
=(not progress
)
151 if mode
== "prove_basecase":
152 task
.basecase_procs
.append(proc
)
154 if mode
== "prove_induction":
155 task
.induction_procs
.append(proc
)
160 def output_callback(line
):
164 match
= re
.match(r
"^## [0-9: ]+ Status: FAILED", line
)
167 return line
.replace("FAILED", "failed")
169 match
= re
.match(r
"^## [0-9: ]+ Status: PASSED", line
)
172 return line
.replace("PASSED", "passed")
174 match
= re
.match(r
"^## [0-9: ]+ Status: PREUNSAT", line
)
176 proc_status
= "ERROR"
179 match
= re
.match(r
"^## [0-9: ]+ Unexpected response from solver:", line
)
181 proc_status
= "ERROR"
184 match
= re
.match(r
"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line
)
187 prop
= task
.design_hierarchy
.find_property_by_cellname(cell_name
)
192 match
= re
.match(r
"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line
)
195 prop
= task
.design_hierarchy
.find_property_by_cellname(cell_name
)
200 match
= re
.match(r
"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line
)
201 if match
and last_prop
:
202 last_prop
.tracefile
= match
[1]
206 match
= re
.match(r
"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line
)
209 prop
= task
.design_hierarchy
.find_property_by_cellname(cell_name
)
214 def exit_callback(retcode
):
215 if proc_status
is None:
216 task
.error(f
"engine_{engine_idx}: Engine terminated without status.")
218 if mode
== "bmc" or mode
== "cover":
219 task
.update_status(proc_status
)
220 proc_status_lower
= proc_status
.lower() if proc_status
== "PASS" else proc_status
221 task
.log(f
"engine_{engine_idx}: Status returned by engine: {proc_status_lower}")
222 task
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower}""")
224 if proc_status
== "FAIL" and mode
!= "cover":
225 if os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace.vcd"):
226 task
.summary
.append(f
"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
227 elif proc_status
== "PASS" and mode
== "cover":
229 for i
in range(print_traces_max
):
230 if os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace{i}.vcd"):
231 task
.summary
.append(f
"trace: {task.workdir}/engine_{engine_idx}/trace{i}.vcd")
236 while os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace{print_traces_max + excess_traces}.vcd"):
238 if excess_traces
> 0:
239 task
.summary
.append(f
"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
240 elif proc_status
== "PASS" and mode
== "bmc":
241 for prop
in task
.design_hierarchy
:
242 if prop
.type == prop
.Type
.ASSERT
and prop
.status
== "UNKNOWN":
247 elif mode
in ["prove_basecase", "prove_induction"]:
248 proc_status_lower
= proc_status
.lower() if proc_status
== "PASS" else proc_status
249 task
.log(f
"""engine_{engine_idx}: Status returned by engine for {mode.split("_")[1]}: {proc_status_lower}""")
250 task
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower} for {mode.split("_")[1]}""")
252 if mode
== "prove_basecase":
253 for proc
in task
.basecase_procs
:
256 if proc_status
== "PASS":
257 task
.basecase_pass
= True
260 task
.update_status(proc_status
)
261 if os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace.vcd"):
262 task
.summary
.append(f
"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
265 elif mode
== "prove_induction":
266 for proc
in task
.induction_procs
:
269 if proc_status
== "PASS":
270 task
.induction_pass
= True
275 if task
.basecase_pass
and task
.induction_pass
:
276 for prop
in task
.design_hierarchy
:
277 if prop
.type == prop
.Type
.ASSERT
and prop
.status
== "UNKNOWN":
279 task
.update_status("PASS")
280 task
.summary
.append("successful proof by k-induction.")
286 proc
.output_callback
= output_callback
287 proc
.exit_callback
= exit_callback