Merge pull request #147 from jix/smtbmc-keepgoing

Support and tests for smtbmc `--keep-going`

diff --combined sbysrc/sby_engine_smtbmc.py
index a9c5c804226ea14f084c79d4de605d031b4e2ab4,9b7ff2b8695921425e4892613d847719c67ee2c6..18cfb092e5a273740860761a2c064baa63ef754f
--- 1/sbysrc/sby_engine_smtbmc.py
--- 2/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@@ -31,11 -31,12 +31,12 @@@ def run(mode, task, engine_idx, engine)
      progress = False
      basecase_only = False
      induction_only = False
+     keep_going = False
      random_seed = None
      task.precise_prop_status = True
  
      opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
-             "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
+             "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "keep-going", "seed="])
  
      for o, a in opts:
          if o == "--nomem":
@@@ -66,6 -67,10 +67,10 @@@
              if basecase_only:
                  task.error("smtbmc options --basecase and --induction are exclusive.")
              induction_only = True
+         elif o == "--keep-going":
+             if mode not in ("bmc", "prove", "prove_basecase", "prove_induction"):
+                 task.error("smtbmc option --keep-going is only supported in bmc and prove mode.")
+             keep_going = True
          elif o == "--seed":
              random_seed = a
          else:
@@@ -126,6 -131,10 +131,10 @@@
          smtbmc_opts.append("-c")
          trace_prefix += "%"
  
+     if keep_going:
+         smtbmc_opts.append("--keep-going")
+         trace_prefix += "%"
+ 
      if dumpsmt2:
          smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]
  
@@@ -155,12 -164,11 +164,12 @@@
          task.induction_procs.append(proc)
  
      proc_status = None
 -    last_prop = None
 +    last_prop = []
  
      def output_callback(line):
          nonlocal proc_status
          nonlocal last_prop
 +        smt2_trans = {'\\':'/', '|':'/'}
  
          match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
          if match:
@@@ -185,30 -193,29 +194,30 @@@
          match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
          if match:
              cell_name = match[3]
 -            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
 +            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
              prop.status = "FAIL"
 -            last_prop = prop
 +            last_prop.append(prop)
              return line
  
          match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
          if match:
              cell_name = match[2]
 -            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
 +            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
              prop.status = "PASS"
 -            last_prop = prop
 +            last_prop.append(prop)
              return line
  
          match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
          if match and last_prop:
 -            last_prop.tracefile = match[1]
 -            last_prop = None
 +            for p in last_prop:
 +                p.tracefile = match[1]
 +            last_prop = []
              return line
  
          match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)
          if match:
              cell_name = match[2]
 -            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
 +            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
              prop.status = "FAIL"
  
          return line

diff --combined tests/.gitignore
index 120675bec4354855a2ba9fe51cff81368d3f05b8,86d3851aaf89cdb7e4f1dad49f9beff9dee019f6..23d000849d886622aefc2e48115fb37ed990da18
--- 1/tests/.gitignore
--- 2/tests/.gitignore
+++ b/tests/.gitignore
@@@ -8,6 -8,6 +8,7 @@@
  /redxor*/
  /stopfirst*/
  /junit_*/
+ /keepgoing_*/
  /submod_props*/
  /multi_assert*/
 +/aim_vs_smt2_nonzero_start_offset*/