From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 14 Dec 2017 01:12:08 +0000 (+0100)
Subject: Disable unrolling per default for z3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25936009bbc2cffd289c607ddf42a578527aa59c;p=SymbiYosys.git

Disable unrolling per default for z3
---

diff --git a/docs/examples/multiclk/dpmem.sby b/docs/examples/multiclk/dpmem.sby
index 08e44a6..574e79e 100644
--- a/docs/examples/multiclk/dpmem.sby
+++ b/docs/examples/multiclk/dpmem.sby
@@ -8,7 +8,6 @@ smtbmc
 [script]
 read_verilog -sv -formal dpmem.sv
 prep -nordff -top top
-memory_map
 chformal -early -assume
 clk2fflogic
 opt_clean
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 715404a..690dfcc 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -23,7 +23,7 @@ def run(mode, job, engine_idx, engine):
     smtbmc_opts = []
     nomem_opt = False
     presat_opt = True
-    unroll_opt = True
+    unroll_opt = None
     syn_opt = False
     stbv_opt = False
     dumpsmt2 = False
@@ -50,15 +50,17 @@ def run(mode, job, engine_idx, engine):
         else:
             assert False
 
+    for i, a in enumerate(args):
+        if i == 0 and a == "z3" and unroll_opt is None:
+                unroll_opt = False
+        smtbmc_opts += ["-s" if i == 0 else "-S", a]
+
     if presat_opt:
         smtbmc_opts += ["--presat"]
 
-    if unroll_opt:
+    if unroll_opt is None or unroll_opt:
         smtbmc_opts += ["--unroll"]
 
-    for i, a in enumerate(args):
-        smtbmc_opts += ["-s" if i == 0 else "-S", a]
-
     if job.opt_smtc is not None:
         smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc]