d9e0a5c9df58c818140d3bd8b26b2977b30c2ac9
3 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
5 # Copyright (C) 2016 Claire Xenia Wolf <claire@yosyshq.com>
7 # Permission to use, copy, modify, and/or distribute this software for any
8 # purpose with or without fee is hereby granted, provided that the above
9 # copyright notice and this permission notice appear in all copies.
11 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
12 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
13 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
14 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
15 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
16 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
17 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
20 import argparse
, json
, os
, sys
, shutil
, tempfile
, re
22 from sby_core
import SbyConfig
, SbyTask
, SbyAbort
, process_filename
25 class DictAction(argparse
.Action
):
26 def __call__(self
, parser
, namespace
, values
, option_string
=None):
27 assert isinstance(getattr(namespace
, self
.dest
), dict), f
"Use ArgumentParser.set_defaults() to initialize {self.dest} to dict()"
28 name
= option_string
.lstrip(parser
.prefix_chars
).replace("-", "_")
29 getattr(namespace
, self
.dest
)[name
] = values
31 parser
= argparse
.ArgumentParser(prog
="sby",
32 usage
="%(prog)s [options] [<jobname>.sby [tasknames] | <dirname>]")
33 parser
.set_defaults(exe_paths
=dict())
35 parser
.add_argument("-d", metavar
="<dirname>", dest
="workdir",
36 help="set workdir name. default: <jobname> or <jobname>_<taskname>. When there is more than one task, use --prefix instead")
37 parser
.add_argument("--prefix", metavar
="<dirname>", dest
="workdir_prefix",
38 help="set the workdir name prefix. `_<taskname>` will be appended to the path for each task")
39 parser
.add_argument("-f", action
="store_true", dest
="force",
40 help="remove workdir if it already exists")
41 parser
.add_argument("-b", action
="store_true", dest
="backup",
42 help="backup workdir if it already exists")
43 parser
.add_argument("-t", action
="store_true", dest
="tmpdir",
44 help="run in a temporary workdir (remove when finished)")
45 parser
.add_argument("-T", metavar
="<taskname>", action
="append", dest
="tasknames", default
=list(),
46 help="add taskname (useful when sby file is read from stdin)")
47 parser
.add_argument("-E", action
="store_true", dest
="throw_err",
48 help="throw an exception (incl stack trace) for most errors")
50 parser
.add_argument("--yosys", metavar
="<path_to_executable>",
51 action
=DictAction
, dest
="exe_paths")
52 parser
.add_argument("--abc", metavar
="<path_to_executable>",
53 action
=DictAction
, dest
="exe_paths")
54 parser
.add_argument("--smtbmc", metavar
="<path_to_executable>",
55 action
=DictAction
, dest
="exe_paths")
56 parser
.add_argument("--suprove", metavar
="<path_to_executable>",
57 action
=DictAction
, dest
="exe_paths")
58 parser
.add_argument("--aigbmc", metavar
="<path_to_executable>",
59 action
=DictAction
, dest
="exe_paths")
60 parser
.add_argument("--avy", metavar
="<path_to_executable>",
61 action
=DictAction
, dest
="exe_paths")
62 parser
.add_argument("--btormc", metavar
="<path_to_executable>",
63 action
=DictAction
, dest
="exe_paths")
64 parser
.add_argument("--pono", metavar
="<path_to_executable>",
65 action
=DictAction
, dest
="exe_paths",
66 help="configure which executable to use for the respective tool")
67 parser
.add_argument("--dumpcfg", action
="store_true", dest
="dump_cfg",
68 help="print the pre-processed configuration file")
69 parser
.add_argument("--dumptags", action
="store_true", dest
="dump_tags",
70 help="print the list of task tags")
71 parser
.add_argument("--dumptasks", action
="store_true", dest
="dump_tasks",
72 help="print the list of tasks")
73 parser
.add_argument("--dumpdefaults", action
="store_true", dest
="dump_defaults",
74 help="print the list of default tasks")
75 parser
.add_argument("--dumptaskinfo", action
="store_true", dest
="dump_taskinfo",
76 help="output a summary of tasks as JSON")
77 parser
.add_argument("--dumpfiles", action
="store_true", dest
="dump_files",
78 help="print the list of source files")
79 parser
.add_argument("--setup", action
="store_true", dest
="setupmode",
80 help="set up the working directory and exit")
82 parser
.add_argument("--init-config-file", dest
="init_config_file",
83 help="create a default .sby config file")
84 parser
.add_argument("sbyfile", metavar
="<jobname>.sby | <dirname>", nargs
="?",
85 help=".sby file OR directory containing config.sby file")
86 parser
.add_argument("arg_tasknames", metavar
="tasknames", nargs
="*",
87 help="tasks to run (only valid when <jobname>.sby is used)")
89 args
= parser
.parse_args()
91 sbyfile
= args
.sbyfile
92 workdir
= args
.workdir
93 workdir_prefix
= args
.workdir_prefix
94 if workdir
is not None and workdir_prefix
is not None:
95 print("ERROR: -d and --prefix are mutually exclusive.", file=sys
.stderr
)
97 tasknames
= args
.arg_tasknames
+ args
.tasknames
98 opt_force
= args
.force
99 opt_backup
= args
.backup
100 opt_tmpdir
= args
.tmpdir
101 exe_paths
= args
.exe_paths
102 throw_err
= args
.throw_err
103 dump_cfg
= args
.dump_cfg
104 dump_tags
= args
.dump_tags
105 dump_tasks
= args
.dump_tasks
106 dump_defaults
= args
.dump_defaults
107 dump_taskinfo
= args
.dump_taskinfo
108 dump_files
= args
.dump_files
110 setupmode
= args
.setupmode
111 init_config_file
= args
.init_config_file
113 if sbyfile
is not None:
114 if os
.path
.isdir(sbyfile
):
115 if workdir
is not None:
116 print("ERROR: Can't use -d when running in existing directory.", file=sys
.stderr
)
119 sbyfile
+= "/config.sby"
121 if not opt_force
and os
.path
.exists(workdir
+ "/model"):
122 print("ERROR: Use -f to re-run in existing directory.", file=sys
.stderr
)
125 print("ERROR: Can't use tasks when running in existing directory.", file=sys
.stderr
)
128 print("ERROR: Can't use --setup with existing directory.", file=sys
.stderr
)
131 for f
in "PASS FAIL UNKNOWN ERROR TIMEOUT".split():
132 if os
.path
.exists(workdir
+ "/" + f
):
133 os
.remove(workdir
+ "/" + f
)
134 elif not sbyfile
.endswith(".sby"):
135 print("ERROR: Sby file does not have .sby file extension.", file=sys
.stderr
)
138 elif init_config_file
is not None:
139 sv_file
= init_config_file
+ ".sv"
140 sby_file
= init_config_file
+ ".sby"
141 with
open(sby_file
, 'w') as config
:
142 config
.write(f
"""[options]
149 read -formal {sv_file}
156 print(f
"sby config written to {sby_file}", file=sys
.stderr
)
159 early_logmsgs
= list()
161 def early_log(workdir
, msg
):
162 tm
= time
.localtime()
163 early_logmsgs
.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm
.tm_hour
, tm
.tm_min
, tm
.tm_sec
, workdir
, msg
))
164 print(early_logmsgs
[-1])
166 def read_sbyconfig(sbydata
, taskname
):
173 tasks_section
= False
174 task_tags_active
= set()
175 task_tags_all
= set()
176 task_skip_block
= False
177 task_skiping_blocks
= False
179 def handle_line(line
):
180 nonlocal pycode
, tasks_section
, task_tags_active
, task_tags_all
181 nonlocal task_skip_block
, task_skiping_blocks
, task_matched
184 line
= line
.rstrip("\n")
185 line
= line
.rstrip("\r")
187 if pycode
is not None:
188 if line
== "--pycode-end--":
189 gdict
= globals().copy()
190 gdict
["task"] = taskname
191 gdict
["tags"] = set(task_tags_active
)
192 gdict
["output_lines"] = list()
193 exec("def output(line):\n output_lines.append(line)\n" + pycode
, gdict
)
195 for line
in gdict
["output_lines"]:
198 pycode
+= line
+ "\n"
201 if line
== "--pycode-begin--":
205 if tasks_section
and line
.startswith("["):
206 tasks_section
= False
208 if task_skiping_blocks
:
210 task_skip_block
= False
211 task_skiping_blocks
= False
214 if not tasks_section
:
215 found_task_tag
= False
216 task_skip_line
= False
218 for t
in task_tags_all
:
219 if line
.startswith(t
+":"):
220 line
= line
[len(t
)+1:].lstrip()
221 match
= t
in task_tags_active
222 elif line
.startswith("~"+t
+":"):
223 line
= line
[len(t
)+2:].lstrip()
224 match
= t
not in task_tags_active
229 task_skiping_blocks
= True
230 task_skip_block
= not match
231 task_skip_line
= True
233 task_skip_line
= not match
235 found_task_tag
= True
238 if len(task_tags_all
) and not found_task_tag
:
239 tokens
= line
.split()
240 if len(tokens
) > 0 and tokens
[0][0] == line
[0] and tokens
[0].endswith(":"):
241 print(f
"ERROR: Invalid task specifier \"{tokens[0]}\".", file=sys
.stderr
)
244 if task_skip_line
or task_skip_block
:
250 if line
.startswith("#"):
253 line
= line
.split(":")
255 line
= line
[0].split()
257 lhs
, rhs
= line
[:1], line
[1:]
261 lhs
, rhs
= line
[0].split(), line
[1].split()
263 print("ERROR: Syntax error in tasks block.", file=sys
.stderr
)
267 if tagname
== "default":
269 if all(map(lambda c
: c
not in "(?*.[]|)", tagname
)):
270 task_tags_all
.add(tagname
)
273 if all(map(lambda c
: c
not in "(?*.[]|)", tname
)):
274 if tname
not in tasklist
:
275 tasklist
.append(tname
)
277 if defaultlist
is None:
279 if tname
not in defaultlist
:
280 defaultlist
.append(tname
)
281 task_tags_all
.add(tname
)
283 if taskname
is not None and re
.fullmatch(tname
, taskname
):
285 task_tags_active
.add(tname
)
287 if tagname
== "default":
289 if all(map(lambda c
: c
not in "(?*.[]|)", tagname
)):
290 task_tags_active
.add(tagname
)
292 for t
in task_tags_all
:
293 if re
.fullmatch(tagname
, t
):
294 task_tags_active
.add(t
)
296 elif line
== "[tasks]":
307 if taskname
is not None and not task_matched
:
308 print(f
"ERROR: Task name '{taskname}' didn't match any lines in [tasks].", file=sys
.stderr
)
311 if defaultlist
is None:
312 defaultlist
= tasklist
314 return cfgdata
, tasklist
, defaultlist
, sorted(list(task_tags_all
))
318 with (open(sbyfile
, "r") if sbyfile
is not None else sys
.stdin
) as f
:
323 assert len(tasknames
) < 2
324 sbyconfig
, _
, _
, _
= read_sbyconfig(sbydata
, tasknames
[0] if len(tasknames
) else None)
325 print("\n".join(sbyconfig
))
331 def find_files(taskname
):
332 sbyconfig
, _
, _
, _
= read_sbyconfig(sbydata
, taskname
)
335 for i
in range(len(sbyconfig
)):
336 if sbyconfig
[i
].strip() == "[files]":
340 if start_index
== -1:
343 for line
in sbyconfig
[start_index
+1:]:
345 if line
.startswith("["):
347 if line
== "" or line
.startswith("#"):
349 filename
= line
.split()[-1]
350 file_set
.add(process_filename(filename
))
353 for taskname
in tasknames
:
357 print("\n".join(file_set
))
361 _
, _
, _
, tagnames
= read_sbyconfig(sbydata
, None)
366 if dump_tasks
or dump_defaults
or dump_tags
:
367 _
, tasks
, dtasks
, tags
= read_sbyconfig(sbydata
, None)
368 for name
in tasks
if dump_tasks
else dtasks
if dump_defaults
else tags
:
374 _
, _
, tasknames
, _
= read_sbyconfig(sbydata
, None)
376 for taskname
in tasknames
or [None]:
377 task_sbyconfig
, _
, _
, _
= read_sbyconfig(sbydata
, taskname
)
378 taskinfo
[taskname
or ""] = info
= {}
380 cfg
.parse_config(task_sbyconfig
)
381 taskinfo
[taskname
or ""] = {
382 "mode": cfg
.options
.get("mode"),
383 "engines": cfg
.engines
,
384 "script": cfg
.script
,
386 print(json
.dumps(taskinfo
, indent
=2))
389 if len(tasknames
) == 0:
390 _
, _
, tasknames
, _
= read_sbyconfig(sbydata
, None)
391 if len(tasknames
) == 0:
394 if (workdir
is not None) and (len(tasknames
) != 1):
395 print("ERROR: Exactly one task is required when workdir is specified. Specify the task or use --prefix instead of -d.", file=sys
.stderr
)
398 def run_task(taskname
):
399 my_opt_tmpdir
= opt_tmpdir
402 if workdir
is not None:
404 elif workdir_prefix
is not None:
405 my_workdir
= workdir_prefix
+ "_" + taskname
407 if my_workdir
is None and sbyfile
is not None and not my_opt_tmpdir
:
408 my_workdir
= sbyfile
[:-4]
409 if taskname
is not None:
410 my_workdir
+= "_" + taskname
412 if my_workdir
is not None:
415 while os
.path
.exists("{}.bak{:03d}".format(my_workdir
, backup_idx
)):
417 early_log(my_workdir
, "Moving directory '{}' to '{}'.".format(my_workdir
, "{}.bak{:03d}".format(my_workdir
, backup_idx
)))
418 shutil
.move(my_workdir
, "{}.bak{:03d}".format(my_workdir
, backup_idx
))
420 if opt_force
and not reusedir
:
421 early_log(my_workdir
, f
"Removing directory '{os.path.abspath(my_workdir)}'.")
423 shutil
.rmtree(my_workdir
, ignore_errors
=True)
427 elif os
.path
.isdir(my_workdir
):
428 print(f
"ERROR: Directory '{my_workdir}' already exists, use -f to overwrite the existing directory.")
431 os
.makedirs(my_workdir
)
435 my_workdir
= tempfile
.mkdtemp()
437 if os
.getenv("SBY_WORKDIR_GITIGNORE"):
438 with
open(f
"{my_workdir}/.gitignore", "w") as gitignore
:
439 print("*", file=gitignore
)
441 junit_ts_name
= os
.path
.basename(sbyfile
[:-4]) if sbyfile
is not None else workdir
if workdir
is not None else "stdin"
442 junit_tc_name
= taskname
if taskname
is not None else "default"
445 junit_filename
= os
.path
.basename(my_workdir
)
446 elif sbyfile
is not None:
447 junit_filename
= os
.path
.basename(sbyfile
[:-4])
448 if taskname
is not None:
449 junit_filename
+= "_" + taskname
450 elif taskname
is not None:
451 junit_filename
= taskname
453 junit_filename
= "junit"
455 sbyconfig
, _
, _
, _
= read_sbyconfig(sbydata
, taskname
)
456 task
= SbyTask(sbyconfig
, my_workdir
, early_logmsgs
, reusedir
)
458 for k
, v
in exe_paths
.items():
459 task
.exe_paths
[k
] = v
470 task
.log(f
"Removing directory '{my_workdir}'.")
471 shutil
.rmtree(my_workdir
, ignore_errors
=True)
474 task
.log(f
"SETUP COMPLETE (rc={task.retcode})")
476 task
.log(f
"DONE ({task.status}, rc={task.retcode})")
479 if not my_opt_tmpdir
and not setupmode
:
480 with
open("{}/{}.xml".format(task
.workdir
, junit_filename
), "w") as f
:
481 task
.print_junit_result(f
, junit_ts_name
, junit_tc_name
, junit_format_strict
=False)
483 with
open(f
"{task.workdir}/status", "w") as f
:
484 print(f
"{task.status} {task.retcode} {task.total_time}", file=f
)
491 for task
in tasknames
:
492 task_retcode
= run_task(task
)
493 retcode |
= task_retcode
497 if failed
and (len(tasknames
) > 1 or tasknames
[0] is not None):
498 tm
= time
.localtime()
499 print("SBY {:2d}:{:02d}:{:02d} The following tasks failed: {}".format(tm
.tm_hour
, tm
.tm_min
, tm
.tm_sec
, failed
))