From 25936009bbc2cffd289c607ddf42a578527aa59c Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 14 Dec 2017 02:12:08 +0100
Subject: [PATCH] Disable unrolling per default for z3
---
docs/examples/multiclk/dpmem.sby | 1 -
sbysrc/sby_engine_smtbmc.py | 12 +++++++-----
2 files changed, 7 insertions(+), 6 deletions(-)
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]