Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/yosys
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 8eb534854387
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: d527ed917475
Choose a head ref
  • 3 commits
  • 2 files changed
  • 2 contributors

Commits on Aug 4, 2017

  1. Copy the full SHA
    1dc921d View commit details
  2. Copy the full SHA
    48b2b37 View commit details
  3. Copy the full SHA
    d527ed9 View commit details
Showing with 71 additions and 21 deletions.
  1. +5 −1 Makefile
  2. +66 −20 backends/smt2/smtbmc.py
6 changes: 5 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -57,12 +57,15 @@ VPATH := $(YOSYS_SRC)
CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -D_YOSYS_ -fPIC -I$(PREFIX)/include
LDFLAGS := $(LDFLAGS) -L$(LIBDIR)
LDLIBS := $(LDLIBS) -lstdc++ -lm
PLUGIN_LDFLAGS :=

PKG_CONFIG ?= pkg-config
SED ?= sed
BISON ?= bison

ifeq (Darwin,$(findstring Darwin,$(shell uname)))
PLUGIN_LDFLAGS += -undefined dynamic_lookup

# homebrew search paths
ifneq ($(shell which brew),)
BREW_PREFIX := $(shell brew --prefix)/opt
@@ -80,6 +83,7 @@ LDFLAGS += -L$(PORT_PREFIX)/lib
PKG_CONFIG_PATH := $(PORT_PREFIX)/lib/pkgconfig:$(PKG_CONFIG_PATH)
export PATH := $(PORT_PREFIX)/bin:$(PATH)
endif

else
LDFLAGS += -rdynamic
LDLIBS += -lrt
@@ -407,7 +411,7 @@ kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile

yosys-config: misc/yosys-config.in
$(P) $(SED) -e 's#@CXXFLAGS@#$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(CXXFLAGS))#;' \
-e 's#@CXX@#$(CXX)#;' -e 's#@LDFLAGS@#$(LDFLAGS)#;' -e 's#@LDLIBS@#$(LDLIBS)#;' \
-e 's#@CXX@#$(CXX)#;' -e 's#@LDFLAGS@#$(LDFLAGS) $(PLUGIN_LDFLAGS)#;' -e 's#@LDLIBS@#$(LDLIBS)#;' \
-e 's#@BINDIR@#$(BINDIR)#;' -e 's#@DATDIR@#$(DATDIR)#;' < $< > yosys-config
$(Q) chmod +x yosys-config

86 changes: 66 additions & 20 deletions backends/smt2/smtbmc.py
Original file line number Diff line number Diff line change
@@ -45,6 +45,9 @@
topmod = None
noinfo = False
presat = False
smtcinit = False
smtctop = None
noinit = False
so = SmtOpts()


@@ -124,6 +127,16 @@ def usage():
--dump-smtc <constr_filename>
write trace as constraints file
--smtc-init
write just the last state as initial constraint to smtc file
--smtc-top <old>[:<new>]
replace <old> with <new> in constraints dumped to smtc
file and only dump object below <old> in design hierarchy.
--noinit
do not assume initial conditions in state 0
--dump-all
when using -g or -i, create a dump file for each
step. The character '%' is replaces in all dump
@@ -140,7 +153,8 @@ def usage():
try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
"dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append="])
"dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
"smtc-init", "smtc-top=", "noinit"])
except:
usage()

@@ -183,12 +197,22 @@ def usage():
vlogtbtop = a
elif o == "--dump-smtc":
outconstr = a
elif o == "--smtc-init":
smtcinit = True
elif o == "--smtc-top":
smtctop = a.split(":")
if len(smtctop) == 1:
smtctop.append("")
assert len(smtctop) == 2
smtctop = tuple(smtctop)
elif o == "--dump-all":
dumpall = True
elif o == "--presat":
presat = True
elif o == "--noinfo":
noinfo = True
elif o == "--noinit":
noinit = True
elif o == "--append":
append_steps = int(a)
elif o == "-i":
@@ -826,34 +850,49 @@ def write_constr_trace(steps_start, steps_stop, index):
filename = outconstr.replace("%", index)
print_msg("Writing trace to constraints file: %s" % (filename))

constr_topmod = topmod
constr_state = "s@@step_idx@@"
constr_prefix = ""

if smtctop is not None:
for item in smtctop[0].split("."):
assert item in smt.modinfo[constr_topmod].cells
constr_state = "(|%s_h %s| %s)" % (constr_topmod, item, constr_state)
constr_topmod = smt.modinfo[constr_topmod].cells[item]
if smtctop[1] != "":
constr_prefix = smtctop[1] + "."

if smtcinit:
steps_start = steps_stop - 1

with open(filename, "w") as f:
primary_inputs = list()

for name in smt.modinfo[topmod].inputs:
width = smt.modinfo[topmod].wsize[name]
for name in smt.modinfo[constr_topmod].inputs:
width = smt.modinfo[constr_topmod].wsize[name]
primary_inputs.append((name, width))

if steps_start == 0:
if steps_start == 0 or smtcinit:
print("initial", file=f)
else:
print("state %d" % steps_start, file=f)

regnames = sorted(smt.hiernets(topmod, regs_only=True))
regvals = smt.get_net_list(topmod, regnames, "s%d" % steps_start)
regnames = sorted(smt.hiernets(constr_topmod, regs_only=True))
regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start)))

for name, val in zip(regnames, regvals):
print("assume (= [%s] %s)" % (".".join(name), val), file=f)
print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)

mems = sorted(smt.hiermems(topmod))
mems = sorted(smt.hiermems(constr_topmod))
for mempath in mems:
abits, width, rports, wports = smt.mem_info(topmod, mempath)
abits, width, rports, wports = smt.mem_info(constr_topmod, mempath)

addr_expr_list = list()
data_expr_list = list()
for i in range(steps_start, steps_stop):
for j in range(rports):
addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
data_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))

addr_list = smt.get_list(addr_expr_list)
data_list = smt.get_list(data_expr_list)
@@ -864,17 +903,18 @@ def write_constr_trace(steps_start, steps_stop, index):
addr_data[addr] = data

for addr, data in addr_data.items():
print("assume (= (select [%s] %s) %s)" % (".".join(mempath), addr, data), file=f)
print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f)

for k in range(steps_start, steps_stop):
print("", file=f)
print("state %d" % k, file=f)
if not smtcinit:
print("", file=f)
print("state %d" % k, file=f)

pi_names = [[name] for name, _ in sorted(primary_inputs)]
pi_values = smt.get_net_list(topmod, pi_names, "s%d" % k)
pi_values = smt.get_net_list(constr_topmod, pi_names, constr_state.replace("@@step_idx@@", str(k)))

for name, val in zip(pi_names, pi_values):
print("assume (= [%s] %s)" % (".".join(name), val), file=f)
print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)


def write_trace(steps_start, steps_stop, index):
@@ -1034,8 +1074,11 @@ def get_cover_list(mod, base):
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))

if step == 0:
smt.write("(assert (|%s_i| s0))" % (topmod))
smt.write("(assert (|%s_is| s0))" % (topmod))
if noinit:
smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
else:
smt.write("(assert (|%s_i| s0))" % (topmod))
smt.write("(assert (|%s_is| s0))" % (topmod))

else:
smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))
@@ -1114,8 +1157,11 @@ def get_cover_list(mod, base):
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))

if step == 0:
smt.write("(assert (|%s_i| s0))" % (topmod))
smt.write("(assert (|%s_is| s0))" % (topmod))
if noinit:
smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
else:
smt.write("(assert (|%s_i| s0))" % (topmod))
smt.write("(assert (|%s_is| s0))" % (topmod))

else:
smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))