mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Disable unrolling per default for z3

Browse source
This commit is contained in:
Clifford Wolf 2017-12-14 02:12:08 +01:00
parent 770c6441d8
commit 25936009bb
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
docs/examples/multiclk/dpmem.sby
View file

@ -8,7 +8,6 @@ smtbmc
[script] [script]
read_verilog -sv -formal dpmem.sv read_verilog -sv -formal dpmem.sv
prep -nordff -top top prep -nordff -top top
memory_map
chformal -early -assume chformal -early -assume
clk2fflogic clk2fflogic
opt_clean opt_clean

12
sbysrc/sby_engine_smtbmc.py
View file

@ -23,7 +23,7 @@ def run(mode, job, engine_idx, engine):
smtbmc_opts = [] smtbmc_opts = []
nomem_opt = False nomem_opt = False
presat_opt = True presat_opt = True
unroll_opt = True unroll_opt = None
syn_opt = False syn_opt = False
stbv_opt = False stbv_opt = False
dumpsmt2 = False dumpsmt2 = False
@ -50,15 +50,17 @@ def run(mode, job, engine_idx, engine):
else: else:
assert False 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: if presat_opt:
smtbmc_opts += ["--presat"] smtbmc_opts += ["--presat"]
if unroll_opt: if unroll_opt is None or unroll_opt:
smtbmc_opts += ["--unroll"] 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: if job.opt_smtc is not None:
smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc] smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc]