919cc359f98a11900ddf59f3064acf97b2b99e9f
2 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
4 # Copyright (C) 2016 Clifford Wolf <clifford@clifford.at>
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 SbyTask
22 def run(mode
, job
, engine_idx
, engine
):
23 abc_opts
, abc_command
= getopt
.getopt(engine
[1:], "", [])
25 if len(abc_command
) == 0:
26 job
.error("Missing ABC command.")
29 job
.error("Unexpected ABC engine options.")
31 if abc_command
[0] == "bmc3":
33 job
.error("ABC command 'bmc3' is only valid in bmc mode.")
34 abc_command
[0] += f
" -F {job.opt_depth} -v"
36 elif abc_command
[0] == "sim3":
38 job
.error("ABC command 'sim3' is only valid in bmc mode.")
39 abc_command
[0] += f
" -F {job.opt_depth} -v"
41 elif abc_command
[0] == "pdr":
43 job
.error("ABC command 'pdr' is only valid in prove mode.")
46 job
.error(f
"Invalid ABC command {abc_command[0]}.")
50 f
"engine_{engine_idx}",
52 f
"""cd {job.workdir}; {job.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
"{job.workdir}/engine_{engine_idx}/logfile.txt", "w")
56 task
.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
: task_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
: task_status
= "UNKNOWN"
68 match
= re
.match(r
"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line
)
69 if match
: task_status
= "PASS"
71 match
= re
.match(r
"^No output asserted in [0-9]+ frames.", line
)
72 if match
: task_status
= "PASS"
74 match
= re
.match(r
"^Property proved.", line
)
75 if match
: task_status
= "PASS"
79 def exit_callback(retcode
):
81 assert task_status
is not None
83 job
.update_status(task_status
)
84 job
.log(f
"engine_{engine_idx}: Status returned by engine: {task_status}")
85 job
.summary
.append(f
"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status}""")
89 if task_status
== "FAIL" and job
.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 (job
.workdir
, job
.exe_paths
["smtbmc"], job
.opt_aigsmt
,
97 "" if job
.opt_tbtop
is None else f
" --vlogtb-top {job.opt_tbtop}",
98 job
.opt_append
, i
=engine_idx
),
99 logfile
=open(f
"{job.workdir}/engine_{engine_idx}/logfile2.txt", "w")
104 def output_callback2(line
):
105 nonlocal task2_status
107 match
= re
.match(r
"^## [0-9: ]+ Status: FAILED", line
)
108 if match
: task2_status
= "FAIL"
110 match
= re
.match(r
"^## [0-9: ]+ Status: PASSED", line
)
111 if match
: task2_status
= "PASS"
115 def exit_callback2(line
):
116 assert task2_status
is not None
117 assert task2_status
== "FAIL"
119 if os
.path
.exists(f
"{job.workdir}/engine_{engine_idx}/trace.vcd"):
120 job
.summary
.append(f
"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
122 task2
.output_callback
= output_callback2
123 task2
.exit_callback
= exit_callback2
125 task
.output_callback
= output_callback
126 task
.exit_callback
= exit_callback