From 8a62780b9df4d2584e41cdd42cab92fddcd75b31 Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Tue, 24 Mar 2020 17:12:12 +0100 Subject: [PATCH 1/7] Fix primegen example Signed-off-by: Claire Wolf --- docs/examples/puzzles/primegen.sby | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/examples/puzzles/primegen.sby b/docs/examples/puzzles/primegen.sby index 9e6da21..20e5072 100644 --- a/docs/examples/puzzles/primegen.sby +++ b/docs/examples/puzzles/primegen.sby @@ -12,6 +12,7 @@ primes_fail: expect fail smtbmc --dumpsmt2 --progress --stbv z3 [script] +read -noverific read -formal primegen.sv primes_fail: chparam -set offset 7 primes primegen: prep -top primegen From f22b6921c5fe26d0d695b77cc129a98f6fb3b482 Mon Sep 17 00:00:00 2001 From: matt venn Date: Wed, 25 Mar 2020 18:00:48 +0100 Subject: [PATCH 2/7] add --init-config option --- sbysrc/sby.py | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index cdcaff4..72dcd79 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -68,6 +68,8 @@ parser.add_argument("--dumpfiles", action="store_true", dest="dump_files", help="print the list of source files") parser.add_argument("--setup", action="store_true", dest="setupmode", help="set up the working directory and exit") +parser.add_argument("--init-config", action="store_true", dest="initconfig", + help="create a default .sby config file") parser.add_argument("sbyfile", metavar=".sby | ", nargs="?", help=".sby file OR directory containing config.sby file") @@ -89,6 +91,23 @@ dump_tasks = args.dump_tasks dump_files = args.dump_files reusedir = False setupmode = args.setupmode +initconfig = args.initconfig + +def init_config(filename): + with open(filename, 'w') as config: + config.write(""" +[options] +mode bmc + +[engines] +smtbmc + +[script] +read -formal default.v +prep -top top + +[files] +default.v""") if sbyfile is not None: if os.path.isdir(sbyfile): @@ -115,6 +134,11 @@ if sbyfile is not None: print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr) sys.exit(1) +elif initconfig: + print("default sby config written to default.sby", file=sys.stderr) + init_config("default.sby") + sys.exit(0) + early_logmsgs = list() def early_log(workdir, msg): @@ -122,7 +146,6 @@ def early_log(workdir, msg): early_logmsgs.append("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg)) print(early_logmsgs[-1]) - def read_sbyconfig(sbydata, taskname): cfgdata = list() tasklist = list() From 5eee219127ccf938e89c4c60a4bfed050c6c0a50 Mon Sep 17 00:00:00 2001 From: matt venn Date: Thu, 26 Mar 2020 18:24:56 +0100 Subject: [PATCH 3/7] use argument for name of .sby and .sv files --- sbysrc/sby.py | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 72dcd79..f17e842 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -68,9 +68,9 @@ parser.add_argument("--dumpfiles", action="store_true", dest="dump_files", help="print the list of source files") parser.add_argument("--setup", action="store_true", dest="setupmode", help="set up the working directory and exit") -parser.add_argument("--init-config", action="store_true", dest="initconfig", - help="create a default .sby config file") +parser.add_argument("--init-config-file", dest="init_config_file", + help="create a default .sby config file") parser.add_argument("sbyfile", metavar=".sby | ", nargs="?", help=".sby file OR directory containing config.sby file") parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*", @@ -91,23 +91,7 @@ dump_tasks = args.dump_tasks dump_files = args.dump_files reusedir = False setupmode = args.setupmode -initconfig = args.initconfig - -def init_config(filename): - with open(filename, 'w') as config: - config.write(""" -[options] -mode bmc - -[engines] -smtbmc - -[script] -read -formal default.v -prep -top top - -[files] -default.v""") +init_config_file = args.init_config_file if sbyfile is not None: if os.path.isdir(sbyfile): @@ -134,9 +118,25 @@ if sbyfile is not None: print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr) sys.exit(1) -elif initconfig: - print("default sby config written to default.sby", file=sys.stderr) - init_config("default.sby") +elif init_config_file is not None: + sv_file = init_config_file + ".sv" + sby_file = init_config_file + ".sby" + with open(sby_file, 'w') as config: + config.write("""[options] +mode bmc + +[engines] +smtbmc + +[script] +read -formal {0} +prep -top top + +[files] +{0} +""".format(sv_file)) + + print("sby config written to {}".format(sby_file), file=sys.stderr) sys.exit(0) early_logmsgs = list() From 0c0215de910597d6ae5bad8109987296bfebf141 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Thu, 2 Apr 2020 17:21:48 +0200 Subject: [PATCH 4/7] fix formatting error --- sbysrc/sby_engine_abc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 306bb36..49d044d 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -89,7 +89,7 @@ def run(mode, job, engine_idx, engine): "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), - job.opt_append, i=engine_idx, engine_idx, engine_idx, engine_idx), + job.opt_append, i=engine_idx), logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) task2_status = None From e9af1a65f106115a8823ae48a89d9520bdd99671 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Thu, 2 Apr 2020 17:36:54 +0200 Subject: [PATCH 5/7] and another --- sbysrc/sby_engine_btor.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 1130a3a..95aba66 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -109,7 +109,7 @@ def run(mode, job, engine_idx, engine): setupcmd = "cd {};".format(job.workdir) finalwit = "engine_{}/trace.wit".format(engine_idx) else: - setupcmd = "cd {}; { echo sat; btorsim --states model/design_btor.btor engine_{i}/trace.wit; } > engine_{i}/simtrace.wit &&".format(job.workdir, i=engine_idx) + setupcmd = "cd {}; {{ echo sat; btorsim --states model/design_btor.btor engine_{i}/trace.wit; }} > engine_{i}/simtrace.wit &&".format(job.workdir, i=engine_idx) finalwit = "engine_{}/simtrace.wit".format(engine_idx) if mode == "live": From d18656084c66506f5822484a63a8fd0b0fc39e55 Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Fri, 3 Apr 2020 15:18:52 +0200 Subject: [PATCH 6/7] Fix typo Signed-off-by: Claire Wolf --- docs/examples/abstract/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/examples/abstract/README.md b/docs/examples/abstract/README.md index b13f74c..b1c04c5 100644 --- a/docs/examples/abstract/README.md +++ b/docs/examples/abstract/README.md @@ -10,7 +10,7 @@ This can be solved by replacing counter with the abstraction in `abstr.sv`. In order to do this we must first prove that the abstraction is correct. This is done with `sby -f abstr.sby`. -Then we apply the abstriction by assuming what we have just proven and otherwise +Then we apply the abstraction by assuming what we have just proven and otherwise turn `counter` into a cutpoint. See `props.sby` for details. Running `sby -f props.sby prv` proves the properties and `sby -f props.sby cvr` From a4885ce4942367e4e170d7e36f19a2388acc538d Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Fri, 3 Apr 2020 15:28:23 +0200 Subject: [PATCH 7/7] Get rid of verific warning in abstraction example Signed-off-by: Claire Wolf --- docs/examples/abstract/demo.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/examples/abstract/demo.v b/docs/examples/abstract/demo.v index 9e5ed2b..a19150f 100644 --- a/docs/examples/abstract/demo.v +++ b/docs/examples/abstract/demo.v @@ -9,7 +9,7 @@ module demo ( if (reset) counter <= 0; else - counter <= counter + 1; + counter <= counter + 20'd 1; end assign A = counter == 123456;