mirror of
https://github.com/YosysHQ/sby.git
synced 2025-08-28 07:28:57 +00:00
Add failing test case
This commit is contained in:
Tom Alcorn
parent
13fef4a710
commit
ad5b9ceed5
4 changed files with 202 additions and 155 deletions
2
.gitignore
vendored
2
.gitignore
vendored
|
|
@ -1,4 +1,4 @@
|
||||||
/docs/build
|
/docs/build
|
||||||
/sbysrc/demo[0-9]
|
/sbysrc/demo[0-9]
|
||||||
/sbysrc/__pycache__
|
/sbysrc/__pycache__
|
||||||
|
*.pyc
|
||||||
|
|
|
||||||
314
sbysrc/sby.py
314
sbysrc/sby.py
|
|
@ -28,126 +28,129 @@ class DictAction(argparse.Action):
|
||||||
name = option_string.lstrip(parser.prefix_chars).replace("-", "_")
|
name = option_string.lstrip(parser.prefix_chars).replace("-", "_")
|
||||||
getattr(namespace, self.dest)[name] = values
|
getattr(namespace, self.dest)[name] = values
|
||||||
|
|
||||||
parser = argparse.ArgumentParser(prog="sby",
|
if __name__ == '__main__':
|
||||||
usage="%(prog)s [options] [<jobname>.sby [tasknames] | <dirname>]")
|
parser = argparse.ArgumentParser(prog="sby",
|
||||||
parser.set_defaults(exe_paths=dict())
|
usage="%(prog)s [options] [<jobname>.sby [tasknames] | <dirname>]")
|
||||||
|
parser.set_defaults(exe_paths=dict())
|
||||||
|
|
||||||
parser.add_argument("-d", metavar="<dirname>", dest="workdir",
|
parser.add_argument("-d", metavar="<dirname>", dest="workdir",
|
||||||
help="set workdir name. default: <jobname> or <jobname>_<taskname>")
|
help="set workdir name. default: <jobname> or <jobname>_<taskname>")
|
||||||
parser.add_argument("-f", action="store_true", dest="force",
|
parser.add_argument("-f", action="store_true", dest="force",
|
||||||
help="remove workdir if it already exists")
|
help="remove workdir if it already exists")
|
||||||
parser.add_argument("-b", action="store_true", dest="backup",
|
parser.add_argument("-b", action="store_true", dest="backup",
|
||||||
help="backup workdir if it already exists")
|
help="backup workdir if it already exists")
|
||||||
parser.add_argument("-t", action="store_true", dest="tmpdir",
|
parser.add_argument("-t", action="store_true", dest="tmpdir",
|
||||||
help="run in a temporary workdir (remove when finished)")
|
help="run in a temporary workdir (remove when finished)")
|
||||||
parser.add_argument("-T", metavar="<taskname>", action="append", dest="tasknames", default=list(),
|
parser.add_argument("-T", metavar="<taskname>", action="append", dest="tasknames", default=list(),
|
||||||
help="add taskname (useful when sby file is read from stdin)")
|
help="add taskname (useful when sby file is read from stdin)")
|
||||||
parser.add_argument("-E", action="store_true", dest="throw_err",
|
parser.add_argument("-E", action="store_true", dest="throw_err",
|
||||||
help="throw an exception (incl stack trace) for most errors")
|
help="throw an exception (incl stack trace) for most errors")
|
||||||
|
|
||||||
parser.add_argument("--yosys", metavar="<path_to_executable>",
|
parser.add_argument("--yosys", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths")
|
action=DictAction, dest="exe_paths")
|
||||||
parser.add_argument("--abc", metavar="<path_to_executable>",
|
parser.add_argument("--abc", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths")
|
action=DictAction, dest="exe_paths")
|
||||||
parser.add_argument("--smtbmc", metavar="<path_to_executable>",
|
parser.add_argument("--smtbmc", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths")
|
action=DictAction, dest="exe_paths")
|
||||||
parser.add_argument("--suprove", metavar="<path_to_executable>",
|
parser.add_argument("--suprove", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths")
|
action=DictAction, dest="exe_paths")
|
||||||
parser.add_argument("--aigbmc", metavar="<path_to_executable>",
|
parser.add_argument("--aigbmc", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths")
|
action=DictAction, dest="exe_paths")
|
||||||
parser.add_argument("--avy", metavar="<path_to_executable>",
|
parser.add_argument("--avy", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths")
|
action=DictAction, dest="exe_paths")
|
||||||
parser.add_argument("--btormc", metavar="<path_to_executable>",
|
parser.add_argument("--btormc", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths")
|
action=DictAction, dest="exe_paths")
|
||||||
parser.add_argument("--cosa2", metavar="<path_to_executable>",
|
parser.add_argument("--cosa2", metavar="<path_to_executable>",
|
||||||
action=DictAction, dest="exe_paths",
|
action=DictAction, dest="exe_paths",
|
||||||
help="configure which executable to use for the respective tool")
|
help="configure which executable to use for the respective tool")
|
||||||
parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg",
|
parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg",
|
||||||
help="print the pre-processed configuration file")
|
help="print the pre-processed configuration file")
|
||||||
parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks",
|
parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks",
|
||||||
help="print the list of tasks")
|
help="print the list of tasks")
|
||||||
parser.add_argument("--dumpfiles", action="store_true", dest="dump_files",
|
parser.add_argument("--dumpfiles", action="store_true", dest="dump_files",
|
||||||
help="print the list of source files")
|
help="print the list of source files")
|
||||||
parser.add_argument("--setup", action="store_true", dest="setupmode",
|
parser.add_argument("--setup", action="store_true", dest="setupmode",
|
||||||
help="set up the working directory and exit")
|
help="set up the working directory and exit")
|
||||||
|
|
||||||
parser.add_argument("--init-config-file", dest="init_config_file",
|
parser.add_argument("--init-config-file", dest="init_config_file",
|
||||||
help="create a default .sby config file")
|
help="create a default .sby config file")
|
||||||
parser.add_argument("sbyfile", metavar="<jobname>.sby | <dirname>", nargs="?",
|
parser.add_argument("sbyfile", metavar="<jobname>.sby | <dirname>", nargs="?",
|
||||||
help=".sby file OR directory containing config.sby file")
|
help=".sby file OR directory containing config.sby file")
|
||||||
parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*",
|
parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*",
|
||||||
help="tasks to run (only valid when <jobname>.sby is used)")
|
help="tasks to run (only valid when <jobname>.sby is used)")
|
||||||
|
|
||||||
args = parser.parse_args()
|
args = parser.parse_args()
|
||||||
|
|
||||||
sbyfile = args.sbyfile
|
sbyfile = args.sbyfile
|
||||||
workdir = args.workdir
|
workdir = args.workdir
|
||||||
tasknames = args.arg_tasknames + args.tasknames
|
tasknames = args.arg_tasknames + args.tasknames
|
||||||
opt_force = args.force
|
opt_force = args.force
|
||||||
opt_backup = args.backup
|
opt_backup = args.backup
|
||||||
opt_tmpdir = args.tmpdir
|
opt_tmpdir = args.tmpdir
|
||||||
exe_paths = args.exe_paths
|
exe_paths = args.exe_paths
|
||||||
throw_err = args.throw_err
|
throw_err = args.throw_err
|
||||||
dump_cfg = args.dump_cfg
|
dump_cfg = args.dump_cfg
|
||||||
dump_tasks = args.dump_tasks
|
dump_tasks = args.dump_tasks
|
||||||
dump_files = args.dump_files
|
dump_files = args.dump_files
|
||||||
reusedir = False
|
reusedir = False
|
||||||
setupmode = args.setupmode
|
setupmode = args.setupmode
|
||||||
init_config_file = args.init_config_file
|
init_config_file = args.init_config_file
|
||||||
|
|
||||||
if sbyfile is not None:
|
if sbyfile is not None:
|
||||||
if os.path.isdir(sbyfile):
|
if os.path.isdir(sbyfile):
|
||||||
if workdir is not None:
|
if workdir is not None:
|
||||||
print("ERROR: Can't use -d when running in existing directory.", file=sys.stderr)
|
print("ERROR: Can't use -d when running in existing directory.", file=sys.stderr)
|
||||||
|
sys.exit(1)
|
||||||
|
workdir = sbyfile
|
||||||
|
sbyfile += "/config.sby"
|
||||||
|
reusedir = True
|
||||||
|
if not opt_force and os.path.exists(workdir + "/model"):
|
||||||
|
print("ERROR: Use -f to re-run in existing directory.", file=sys.stderr)
|
||||||
|
sys.exit(1)
|
||||||
|
if tasknames:
|
||||||
|
print("ERROR: Can't use tasks when running in existing directory.", file=sys.stderr)
|
||||||
|
sys.exit(1)
|
||||||
|
if setupmode:
|
||||||
|
print("ERROR: Can't use --setup with existing directory.", file=sys.stderr)
|
||||||
|
sys.exit(1)
|
||||||
|
if opt_force:
|
||||||
|
for f in "PASS FAIL UNKNOWN ERROR TIMEOUT".split():
|
||||||
|
if os.path.exists(workdir + "/" + f):
|
||||||
|
os.remove(workdir + "/" + f)
|
||||||
|
elif not sbyfile.endswith(".sby"):
|
||||||
|
print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr)
|
||||||
sys.exit(1)
|
sys.exit(1)
|
||||||
workdir = sbyfile
|
|
||||||
sbyfile += "/config.sby"
|
|
||||||
reusedir = True
|
|
||||||
if not opt_force and os.path.exists(workdir + "/model"):
|
|
||||||
print("ERROR: Use -f to re-run in existing directory.", file=sys.stderr)
|
|
||||||
sys.exit(1)
|
|
||||||
if tasknames:
|
|
||||||
print("ERROR: Can't use tasks when running in existing directory.", file=sys.stderr)
|
|
||||||
sys.exit(1)
|
|
||||||
if setupmode:
|
|
||||||
print("ERROR: Can't use --setup with existing directory.", file=sys.stderr)
|
|
||||||
sys.exit(1)
|
|
||||||
if opt_force:
|
|
||||||
for f in "PASS FAIL UNKNOWN ERROR TIMEOUT".split():
|
|
||||||
if os.path.exists(workdir + "/" + f):
|
|
||||||
os.remove(workdir + "/" + f)
|
|
||||||
elif not sbyfile.endswith(".sby"):
|
|
||||||
print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr)
|
|
||||||
sys.exit(1)
|
|
||||||
|
|
||||||
elif init_config_file is not None:
|
elif init_config_file is not None:
|
||||||
sv_file = init_config_file + ".sv"
|
sv_file = init_config_file + ".sv"
|
||||||
sby_file = init_config_file + ".sby"
|
sby_file = init_config_file + ".sby"
|
||||||
with open(sby_file, 'w') as config:
|
with open(sby_file, 'w') as config:
|
||||||
config.write("""[options]
|
config.write("""[options]
|
||||||
mode bmc
|
mode bmc
|
||||||
|
|
||||||
[engines]
|
[engines]
|
||||||
smtbmc
|
smtbmc
|
||||||
|
|
||||||
[script]
|
[script]
|
||||||
read -formal {0}
|
read -formal {0}
|
||||||
prep -top top
|
prep -top top
|
||||||
|
|
||||||
[files]
|
[files]
|
||||||
{0}
|
{0}
|
||||||
""".format(sv_file))
|
""".format(sv_file))
|
||||||
|
|
||||||
print("sby config written to {}".format(sby_file), file=sys.stderr)
|
print("sby config written to {}".format(sby_file), file=sys.stderr)
|
||||||
sys.exit(0)
|
sys.exit(0)
|
||||||
|
|
||||||
|
early_logmsgs = list()
|
||||||
|
|
||||||
early_logmsgs = list()
|
|
||||||
|
|
||||||
def early_log(workdir, msg):
|
def early_log(workdir, msg):
|
||||||
tm = localtime()
|
tm = localtime()
|
||||||
early_logmsgs.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg))
|
early_logmsgs.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg))
|
||||||
print(early_logmsgs[-1])
|
print(early_logmsgs[-1])
|
||||||
|
|
||||||
|
|
||||||
def read_sbyconfig(sbydata, taskname):
|
def read_sbyconfig(sbydata, taskname):
|
||||||
cfgdata = list()
|
cfgdata = list()
|
||||||
tasklist = list()
|
tasklist = list()
|
||||||
|
|
@ -269,63 +272,65 @@ def read_sbyconfig(sbydata, taskname):
|
||||||
return cfgdata, tasklist
|
return cfgdata, tasklist
|
||||||
|
|
||||||
|
|
||||||
sbydata = list()
|
if __name__ == '__main__':
|
||||||
with (open(sbyfile, "r") if sbyfile is not None else sys.stdin) as f:
|
sbydata = list()
|
||||||
for line in f:
|
with (open(sbyfile, "r") if sbyfile is not None else sys.stdin) as f:
|
||||||
sbydata.append(line)
|
for line in f:
|
||||||
|
sbydata.append(line)
|
||||||
|
|
||||||
if dump_cfg:
|
if dump_cfg:
|
||||||
assert len(tasknames) < 2
|
assert len(tasknames) < 2
|
||||||
sbyconfig, _ = read_sbyconfig(sbydata, tasknames[0] if len(tasknames) else None)
|
sbyconfig, _ = read_sbyconfig(sbydata, tasknames[0] if len(tasknames) else None)
|
||||||
print("\n".join(sbyconfig))
|
print("\n".join(sbyconfig))
|
||||||
sys.exit(0)
|
sys.exit(0)
|
||||||
|
|
||||||
if dump_files:
|
if dump_files:
|
||||||
file_set = set()
|
file_set = set()
|
||||||
|
|
||||||
def find_files(taskname):
|
def find_files(taskname):
|
||||||
sbyconfig, _ = read_sbyconfig(sbydata, taskname)
|
sbyconfig, _ = read_sbyconfig(sbydata, taskname)
|
||||||
|
|
||||||
start_index = -1
|
start_index = -1
|
||||||
for i in range(len(sbyconfig)):
|
for i in range(len(sbyconfig)):
|
||||||
if sbyconfig[i].strip() == "[files]":
|
if sbyconfig[i].strip() == "[files]":
|
||||||
start_index = i
|
start_index = i
|
||||||
break
|
break
|
||||||
|
|
||||||
if start_index == -1:
|
if start_index == -1:
|
||||||
return
|
return
|
||||||
|
|
||||||
for line in sbyconfig[start_index+1:]:
|
for line in sbyconfig[start_index+1:]:
|
||||||
line = line.strip()
|
line = line.strip()
|
||||||
if line.startswith("["):
|
if line.startswith("["):
|
||||||
break
|
break
|
||||||
if line == "" or line.startswith("#"):
|
if line == "" or line.startswith("#"):
|
||||||
continue
|
continue
|
||||||
filename = line.split()[-1]
|
filename = line.split()[-1]
|
||||||
file_set.add(process_filename(filename))
|
file_set.add(process_filename(filename))
|
||||||
|
|
||||||
if len(tasknames):
|
if len(tasknames):
|
||||||
for taskname in tasknames:
|
for taskname in tasknames:
|
||||||
find_files(taskname)
|
find_files(taskname)
|
||||||
else:
|
else:
|
||||||
find_files(None)
|
find_files(None)
|
||||||
print("\n".join(file_set))
|
print("\n".join(file_set))
|
||||||
sys.exit(0)
|
sys.exit(0)
|
||||||
|
|
||||||
if len(tasknames) == 0:
|
|
||||||
_, tasknames = read_sbyconfig(sbydata, None)
|
|
||||||
if len(tasknames) == 0:
|
if len(tasknames) == 0:
|
||||||
tasknames = [None]
|
_, tasknames = read_sbyconfig(sbydata, None)
|
||||||
|
if len(tasknames) == 0:
|
||||||
|
tasknames = [None]
|
||||||
|
|
||||||
if dump_tasks:
|
if dump_tasks:
|
||||||
for task in tasknames:
|
for task in tasknames:
|
||||||
if task is not None:
|
if task is not None:
|
||||||
print(task)
|
print(task)
|
||||||
sys.exit(0)
|
sys.exit(0)
|
||||||
|
|
||||||
|
if (workdir is not None) and (len(tasknames) != 1):
|
||||||
|
print("ERROR: Exactly one task is required when workdir is specified.", file=sys.stderr)
|
||||||
|
sys.exit(1)
|
||||||
|
|
||||||
if (workdir is not None) and (len(tasknames) != 1):
|
|
||||||
print("ERROR: Exactly one task is required when workdir is specified.", file=sys.stderr)
|
|
||||||
sys.exit(1)
|
|
||||||
|
|
||||||
def run_job(taskname):
|
def run_job(taskname):
|
||||||
my_workdir = workdir
|
my_workdir = workdir
|
||||||
|
|
@ -425,12 +430,13 @@ def run_job(taskname):
|
||||||
return job.retcode
|
return job.retcode
|
||||||
|
|
||||||
|
|
||||||
retcode = 0
|
if __name__ == '__main__':
|
||||||
for t in tasknames:
|
retcode = 0
|
||||||
retcode |= run_job(t)
|
for t in tasknames:
|
||||||
|
retcode |= run_job(t)
|
||||||
|
|
||||||
if retcode and (len(tasknames) > 1 or tasknames[0] is not None):
|
if retcode and (len(tasknames) > 1 or tasknames[0] is not None):
|
||||||
tm = localtime()
|
tm = localtime()
|
||||||
print("SBY {:2d}:{:02d}:{:02d} One or more tasks produced a non-zero return code.".format(tm.tm_hour, tm.tm_min, tm.tm_sec))
|
print("SBY {:2d}:{:02d}:{:02d} One or more tasks produced a non-zero return code.".format(tm.tm_hour, tm.tm_min, tm.tm_sec))
|
||||||
|
|
||||||
sys.exit(retcode)
|
sys.exit(retcode)
|
||||||
|
|
|
||||||
|
|
@ -499,6 +499,7 @@ class SbyJob:
|
||||||
for line in f:
|
for line in f:
|
||||||
raw_line = line
|
raw_line = line
|
||||||
if mode in ["options", "engines", "files"]:
|
if mode in ["options", "engines", "files"]:
|
||||||
|
# delete trailing whitespace and comments
|
||||||
line = re.sub(r"\s*(\s#.*)?$", "", line)
|
line = re.sub(r"\s*(\s#.*)?$", "", line)
|
||||||
if line == "" or line[0] == "#":
|
if line == "" or line[0] == "#":
|
||||||
continue
|
continue
|
||||||
|
|
|
||||||
40
sbysrc/test_sby.py
Normal file
40
sbysrc/test_sby.py
Normal file
|
|
@ -0,0 +1,40 @@
|
||||||
|
import unittest
|
||||||
|
|
||||||
|
from sby import *
|
||||||
|
|
||||||
|
|
||||||
|
class TestSby(unittest.TestCase):
|
||||||
|
def test_read_sbyconfig(self):
|
||||||
|
cfg = '''
|
||||||
|
[tasks]
|
||||||
|
a
|
||||||
|
b
|
||||||
|
|
||||||
|
[options]
|
||||||
|
a:
|
||||||
|
mode prove
|
||||||
|
depth 100
|
||||||
|
|
||||||
|
b:
|
||||||
|
mode cover
|
||||||
|
depth 100
|
||||||
|
|
||||||
|
[engines]
|
||||||
|
smtbmc
|
||||||
|
|
||||||
|
[script]
|
||||||
|
read -formal foo.v
|
||||||
|
prep -top foo
|
||||||
|
|
||||||
|
[files]
|
||||||
|
foo.v
|
||||||
|
'''
|
||||||
|
sbydata = cfg.split('\n')
|
||||||
|
cfgdata, tasklist = read_sbyconfig(sbydata, 'a')
|
||||||
|
|
||||||
|
self.assertIn('[engines]', cfgdata)
|
||||||
|
i = cfgdata.index('[engines]')
|
||||||
|
self.assertSequenceEqual(['[engines]', 'smtbmc'], cfgdata[index:index+1])
|
||||||
|
print(cfgdata)
|
||||||
|
print(tasklist)
|
||||||
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue