merge master

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`

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;

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

sbysrc/sby.py

@@ -69,6 +69,8 @@ parser.add_argument("--dumpfiles", action="store_true", dest="dump_files",
 parser.add_argument("--setup", action="store_true", dest="setupmode",
         help="set up the working directory and exit")
 
+parser.add_argument("--init-config-file", dest="init_config_file",
+        help="create a default .sby config file")
 parser.add_argument("sbyfile", metavar="<jobname>.sby | <dirname>", nargs="?",
         help=".sby file OR directory containing config.sby file")
 parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*",
@@ -89,6 +91,7 @@ dump_tasks = args.dump_tasks
 dump_files = args.dump_files
 reusedir = False
 setupmode = args.setupmode
+init_config_file = args.init_config_file
 
 if sbyfile is not None:
     if os.path.isdir(sbyfile):
@@ -115,6 +118,27 @@ if sbyfile is not None:
         print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr)
         sys.exit(1)
 
+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()
 
 def early_log(workdir, msg):
@@ -122,7 +146,6 @@ def early_log(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])
 
-
 def read_sbyconfig(sbydata, taskname):
     cfgdata = list()
     tasklist = list()

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