10e12687c6b86f4f66e4e821ca4277185253916b
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 abc_opts
, abc_command
= getopt
.getopt(engine
[1:], "", [])
25 if len(abc_command
) == 0:
26 task
.error("Missing ABC command.")
29 task
.error("Unexpected ABC engine options.")
31 if abc_command
[0] == "bmc3":
33 task
.error("ABC command 'bmc3' is only valid in bmc mode.")
34 abc_command
[0] += f
" -F {task.opt_depth} -v"
36 elif abc_command
[0] == "sim3":
38 task
.error("ABC command 'sim3' is only valid in bmc mode.")
39 abc_command
[0] += f
" -F {task.opt_depth} -v"
41 elif abc_command
[0] == "pdr":
43 task
.error("ABC command 'pdr' is only valid in prove mode.")
46 task
.error(f
"Invalid ABC command {abc_command[0]}.")
50 f
"engine_{engine_idx}",
52 f
"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
53 logfile
=open(f
"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
56 proc
.noprintregex
= re
.compile(r
"^\.+$")
59 def output_callback(line
):
62 match
= re
.match(r
"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line
)
63 if match
: proc_status
= "FAIL"
65 match
= re
.match(r
"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", line
)
66 if match
: proc_status
= "UNKNOWN"
68 match
= re
.match(r
"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line
)
69 if match
: proc_status
= "PASS"
71 match
= re
.match(r
"^No output asserted in [0-9]+ frames.", line
)
72 if match
: proc_status
= "PASS"
74 match
= re
.match(r
"^Property proved.", line
)
75 if match
: proc_status
= "PASS"
79 def exit_callback(retcode
):
81 assert proc_status
is not None
83 task
.update_status(proc_status
)
84 task
.log(f
"engine_{engine_idx}: Status returned by engine: {proc_status}")
85 task
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""")
89 if proc_status
== "FAIL" and task
.opt_aigsmt
!= "none":
92 f
"engine_{engine_idx}",
94 ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
95 "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format
96 (task
.workdir
, task
.exe_paths
["smtbmc"], task
.opt_aigsmt
,
97 "" if task
.opt_tbtop
is None else f
" --vlogtb-top {task.opt_tbtop}",
98 task
.opt_append
, i
=engine_idx
),
99 logfile
=open(f
"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
104 def output_callback2(line
):
105 nonlocal proc2_status
107 match
= re
.match(r
"^## [0-9: ]+ Status: FAILED", line
)
108 if match
: proc2_status
= "FAIL"
110 match
= re
.match(r
"^## [0-9: ]+ Status: PASSED", line
)
111 if match
: proc2_status
= "PASS"
115 def exit_callback2(line
):
116 assert proc2_status
is not None
117 assert proc2_status
== "FAIL"
119 if os
.path
.exists(f
"{task.workdir}/engine_{engine_idx}/trace.vcd"):
120 task
.summary
.append(f
"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
122 proc2
.output_callback
= output_callback2
123 proc2
.exit_callback
= exit_callback2
125 proc
.output_callback
= output_callback
126 proc
.exit_callback
= exit_callback