mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 14:04:07 +00:00
Code Activity

modified the mode runners to accept the modified engine layout in preperation for the per-mode engine sections

Browse source
This commit is contained in:
Aki Van Ness 2022-07-29 10:21:48 -04:00
parent f1a645bb18
commit 9293081308
No known key found for this signature in database
GPG key ID: C629E8EC06327BEE
5 changed files with 32 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
sbysrc/sby_core.py
View file

@ -247,7 +247,7 @@ class SbyConfig:
def __init__(self): def __init__(self):
self.options = dict() self.options = dict()
# Define a default case for the engine block # Define a default case for the engine block
self.engines = list() # { None: list() } self.engines = { None: list() }
self.setup = dict() self.setup = dict()
self.stage = dict() self.stage = dict()
self.script = list() self.script = list()
@ -387,8 +387,7 @@ class SbyConfig:
if mode == "engines": if mode == "engines":
entries = line.split() entries = line.split()
# self.engines[engine_mode].append(entries) self.engines[engine_mode].append(entries)
self.engines.append(entries)
continue continue
if mode == "setup": if mode == "setup":
@ -565,7 +564,7 @@ class SbyTask(SbyConfig):
print(line, file=f) print(line, file=f)
def engine_list(self): def engine_list(self):
return list(enumerate(self.engines)) return list(enumerate(self.engines.items()))
def check_timeout(self): def check_timeout(self):
if self.opt_timeout is not None: if self.opt_timeout is not None:

9
sbysrc/sby_mode_bmc.py
View file

@ -24,10 +24,15 @@ def run(task):
task.handle_int_option("append", 0) task.handle_int_option("append", 0)
task.handle_str_option("aigsmt", "yices") task.handle_str_option("aigsmt", "yices")
for engine_idx, engine in task.engine_list(): for engine_idx, engine_section in task.engine_list():
engine = engine_section[1][0]
engine_name = engine_section[0]
if engine_name is None:
engine_name = engine_idx
assert len(engine) > 0 assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
task.makedirs(f"{task.workdir}/engine_{engine_idx}") task.makedirs(f"{task.workdir}/engine_{engine_idx}")
if engine[0] == "smtbmc": if engine[0] == "smtbmc":

10
sbysrc/sby_mode_cover.py
View file

@ -23,10 +23,16 @@ def run(task):
task.handle_int_option("depth", 20) task.handle_int_option("depth", 20)
task.handle_int_option("append", 0) task.handle_int_option("append", 0)
for engine_idx, engine in task.engine_list(): for engine_idx, engine_section in task.engine_list():
engine = engine_section[1][0]
engine_name = engine_section[0]
if engine_name is None:
engine_name = engine_idx
assert len(engine) > 0 assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
task.makedirs(f"{task.workdir}/engine_{engine_idx}") task.makedirs(f"{task.workdir}/engine_{engine_idx}")
if engine[0] == "smtbmc": if engine[0] == "smtbmc":

9
sbysrc/sby_mode_live.py
View file

@ -24,10 +24,15 @@ def run(task):
task.status = "UNKNOWN" task.status = "UNKNOWN"
for engine_idx, engine in task.engine_list(): for engine_idx, engine_section in task.engine_list():
engine = engine_section[1][0]
engine_name = engine_section[0]
if engine_name is None:
engine_name = engine_idx
assert len(engine) > 0 assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
task.makedirs(f"{task.workdir}/engine_{engine_idx}") task.makedirs(f"{task.workdir}/engine_{engine_idx}")
if engine[0] == "aiger": if engine[0] == "aiger":

9
sbysrc/sby_mode_prove.py
View file

@ -31,10 +31,15 @@ def run(task):
task.basecase_procs = list() task.basecase_procs = list()
task.induction_procs = list() task.induction_procs = list()
for engine_idx, engine in task.engine_list(): for engine_idx, engine_section in task.engine_list():
engine = engine_section[1][0]
engine_name = engine_section[0]
if engine_name is None:
engine_name = engine_idx
assert len(engine) > 0 assert len(engine) > 0
task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
task.makedirs(f"{task.workdir}/engine_{engine_idx}") task.makedirs(f"{task.workdir}/engine_{engine_idx}")
if engine[0] == "smtbmc": if engine[0] == "smtbmc":