From 36c7185393066e0c1faafaaa5a22384bd8a0e7fd Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 27 Mar 2018 16:23:57 +0200 Subject: [PATCH] More improvements in sby error handling Signed-off-by: Clifford Wolf --- sbysrc/sby_engine_abc.py | 18 +++++++++++------- sbysrc/sby_engine_aiger.py | 8 +++++--- sbysrc/sby_engine_smtbmc.py | 8 +++++--- sbysrc/sby_mode_bmc.py | 2 +- sbysrc/sby_mode_cover.py | 2 +- sbysrc/sby_mode_live.py | 2 +- sbysrc/sby_mode_prove.py | 2 +- 7 files changed, 25 insertions(+), 17 deletions(-) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 6e5bb09..38222e9 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -21,25 +21,29 @@ from sby_core import SbyTask def run(mode, job, engine_idx, engine): abc_opts, abc_command = getopt.getopt(engine[1:], "", []) - assert len(abc_command) > 0 + + if len(abc_command) == 0: + job.error("Missing ABC command.") for o, a in abc_opts: - assert False + job.error("Unexpected ABC engine options.") if abc_command[0] == "bmc3": - assert mode == "bmc" - assert len(abc_command) == 1 + if mode != "bmc": + job.error("ABC command 'bmc3' is only valid in bmc mode.") abc_command[0] += " -F %d -v" % job.opt_depth elif abc_command[0] == "sim3": - assert mode == "bmc" + if mode != "bmc": + job.error("ABC command 'sim3' is only valid in bmc mode.") abc_command[0] += " -F %d -v" % job.opt_depth elif abc_command[0] == "pdr": - assert mode == "prove" + if mode != "prove": + job.error("ABC command 'pdr' is only valid in prove mode.") else: - assert False + job.error("Invalid ABC command %s." % abc_command[0]) task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), ("cd %s; %s -c 'read_aiger model/design_aiger.aig; fold; strash; %s; write_cex -a engine_%d/trace.aiw'") % diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index d67a9c6..1e3594c 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -21,10 +21,12 @@ from sby_core import SbyTask def run(mode, job, engine_idx, engine): opts, solver_args = getopt.getopt(engine[1:], "", []) - assert len(solver_args) > 0 + + if len(solver_args) == 0: + job.error("Missing solver command.") for o, a in opts: - assert False + job.error("Unexpected AIGER engine options.") if solver_args[0] == "suprove": if mode == "live" and (len(solver_args) == 1 or solver_args[1][0] != "+"): @@ -38,7 +40,7 @@ def run(mode, job, engine_idx, engine): solver_cmd = " ".join([job.exe_paths["aigbmc"]] + solver_args[1:]) else: - assert False + job.error("Invalid solver command %s." % solver_args[0]) task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), "cd %s; %s model/design_aiger.aig" % (job.workdir, solver_cmd), diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index fe82c7f..23ec693 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -57,13 +57,15 @@ def run(mode, job, engine_idx, engine): elif o == "--progress": progress = True elif o == "--basecase": - assert not induction_only + if induction_only: + job.error("smtbmc options --basecase and --induction are exclusive.") basecase_only = True elif o == "--induction": - assert not basecase_only + if basecase_only: + job.error("smtbmc options --basecase and --induction are exclusive.") induction_only = True else: - assert False + job.error("Invalid smtbmc options %s." % o) for i, a in enumerate(args): if i == 0 and a == "z3" and unroll_opt is None: diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index 203a224..5e6236d 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -40,5 +40,5 @@ def run(job): sby_engine_abc.run("bmc", job, engine_idx, engine) else: - assert False + job.error("Invalid engine '%s' for bmc mode." % engine[0]) diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index a37c7f2..a4f3597 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -35,5 +35,5 @@ def run(job): sby_engine_smtbmc.run("cover", job, engine_idx, engine) else: - assert False + job.error("Invalid engine '%s' for cover mode." % engine[0]) diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index 6b22487..bee065c 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -36,5 +36,5 @@ def run(job): sby_engine_aiger.run("live", job, engine_idx, engine) else: - assert False + job.error("Invalid engine '%s' for live mode." % engine[0]) diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index f1fee35..d7742e7 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -51,5 +51,5 @@ def run(job): sby_engine_abc.run("prove", job, engine_idx, engine) else: - assert False + job.error("Invalid engine '%s' for prove mode." % engine[0]) -- 2.30.2