diff options
| author | Andrew Zonenberg <azonenberg@drawersteak.com> | 2017-01-15 09:43:15 -0800 |
|---|---|---|
| committer | Andrew Zonenberg <azonenberg@drawersteak.com> | 2017-01-15 09:43:15 -0800 |
| commit | 0c83a30f950d766ddd09bb744ee93e2433095b5c (patch) | |
| tree | ebcd15a0e73b9737d64a723a20214960d033e467 | |
| parent | ac90de73becaeac034b226def9c387645698c363 (diff) | |
| parent | 78f65f89ffc1d5c5237009c19e84e625ce3085aa (diff) | |
| download | yosys-0c83a30f950d766ddd09bb744ee93e2433095b5c.tar.gz yosys-0c83a30f950d766ddd09bb744ee93e2433095b5c.tar.bz2 yosys-0c83a30f950d766ddd09bb744ee93e2433095b5c.zip | |
Merge https://github.com/cliffordwolf/yosys
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 2 | ||||
| -rw-r--r-- | frontends/ast/simplify.cc | 2 |
3 files changed, 7 insertions, 3 deletions
@@ -86,7 +86,7 @@ OBJS = kernel/version_$(GIT_REV).o # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 55cd83f432c0 +ABCREV = f8cadfe3861f ABCPULL = 1 ABCURL ?= https://bitbucket.org/alanmi/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" @@ -174,7 +174,7 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s LDLIBS := $(filter-out -lrt,$(LDLIBS)) -ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -x c++ -fpermissive -w" +ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=1 CC="$(CXX)" CXX="$(CXX)" EXE = .exe @@ -185,7 +185,7 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS)) LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s LDLIBS := $(filter-out -lrt,$(LDLIBS)) -ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -x c++ -fpermissive -w" +ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w" ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=0 CC="$(CXX)" CXX="$(CXX)" EXE = .exe diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 8dbb047aa..ecee6795e 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -789,6 +789,7 @@ else: # not tempind for i in range(1, step_size): if step+i < num_steps: smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod)) + smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step+i)) smt.write("(assert (|%s_u| s%d))" % (topmod, step+i)) smt.write("(assert (|%s_h| s%d))" % (topmod, step+i)) smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i)) @@ -812,6 +813,7 @@ else: # not tempind for i in range(last_check_step+1, last_check_step+1+append_steps): print_msg("Appending additional step %d." % i) smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod)) + smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i)) smt.write("(assert (|%s_u| s%d))" % (topmod, i)) smt.write("(assert (|%s_h| s%d))" % (topmod, i)) smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i)) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index de85355b5..c1e77c6ec 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -3079,6 +3079,8 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod, if (bit_part_sel) children.push_back(bit_part_sel); + + did_something = true; } log_assert(id2ast == NULL || mem2reg_set.count(id2ast) == 0); |