azonenberg · Sep 2, 2016 · Sep 2, 2016 · Sep 2, 2016 · Sep 2, 2016 · Sep 2, 2016
diff --git a/Makefile b/Makefile
@@ -82,7 +82,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 = a86455b00da5
+ABCREV = 8e08604f8ad3
 ABCPULL = 1
 ABCURL ?= https://bitbucket.org/alanmi/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"
@@ -279,6 +279,7 @@ $(eval $(call add_include_file,kernel/log.h))
 $(eval $(call add_include_file,kernel/rtlil.h))
 $(eval $(call add_include_file,kernel/register.h))
 $(eval $(call add_include_file,kernel/celltypes.h))
+$(eval $(call add_include_file,kernel/celledges.h))
 $(eval $(call add_include_file,kernel/consteval.h))
 $(eval $(call add_include_file,kernel/sigtools.h))
 $(eval $(call add_include_file,kernel/modtools.h))
@@ -403,16 +404,22 @@ endif
 yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE)
 	$(P) cp abc/abc-$(ABCREV)$(EXE) yosys-abc$(EXE)
 
+ifneq ($(SEED),)
+SEEDOPT="-S $(SEED)"
+else
+SEEDOPT=""
+endif
+
 test: $(TARGETS) $(EXTRA_TARGETS)
-	+cd tests/simple && bash run-test.sh
-	+cd tests/hana && bash run-test.sh
-	+cd tests/asicworld && bash run-test.sh
-	+cd tests/realmath && bash run-test.sh
-	+cd tests/share && bash run-test.sh
-	+cd tests/fsm && bash run-test.sh
+	+cd tests/simple && bash run-test.sh $(SEEDOPT)
+	+cd tests/hana && bash run-test.sh $(SEEDOPT)
+	+cd tests/asicworld && bash run-test.sh $(SEEDOPT)
+	+cd tests/realmath && bash run-test.sh $(SEEDOPT)
+	+cd tests/share && bash run-test.sh $(SEEDOPT)
+	+cd tests/fsm && bash run-test.sh $(SEEDOPT)
 	+cd tests/techmap && bash run-test.sh
-	+cd tests/memories && bash run-test.sh
-	+cd tests/bram && bash run-test.sh
+	+cd tests/memories && bash run-test.sh $(SEEDOPT)
+	+cd tests/bram && bash run-test.sh $(SEEDOPT)
 	+cd tests/various && bash run-test.sh
 	+cd tests/sat && bash run-test.sh
 	@echo ""

diff --git a/README b/README
@@ -52,12 +52,12 @@ You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is
 recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make.
 TCL, readline and libffi are optional (see ENABLE_* settings in Makefile).
 Xdot (graphviz) is used by the "show" command in yosys to display schematics.
-For example on Ubuntu Linux 14.04 LTS the following commands will install all
+For example on Ubuntu Linux 16.04 LTS the following commands will install all
 prerequisites for building yosys:
 
-	$ yosys_deps="build-essential clang bison flex libreadline-dev gawk
-	       tcl-dev libffi-dev git mercurial graphviz xdot pkg-config python3"
-	$ sudo apt-get install $yosys_deps
+	$ sudo apt-get install build-essential clang bison flex \
+		libreadline-dev gawk tcl-dev libffi-dev git mercurial \
+		graphviz xdot pkg-config python3
 
 There are also pre-compiled Yosys binary packages for Ubuntu and Win32 as well
 as a source distribution for Visual Studio. Visit the Yosys download page for
@@ -354,8 +354,8 @@ Verilog Attributes and non-standard features
       endmodule
 
 - A limited subset of DPI-C functions is supported. The plugin mechanism
-  (see "help plugin") can be used load .so files with implementations of
-  DPI-C routines. As a non-standard extension it is possible to specify
+  (see "help plugin") can be used to load .so files with implementations
+  of DPI-C routines. As a non-standard extension it is possible to specify
   a plugin alias using the "<alias>:" syntax. for example:
 
       module dpitest;
@@ -370,7 +370,7 @@ Verilog Attributes and non-standard features
   must be put in parentheses. Examples: WIDTH'd42, (4+2)'b101010
 
 - The system tasks $finish and $display are supported in initial blocks
-  in and unconditional context (only if/case statements on parameters
+  in an unconditional context (only if/case statements on parameters
   and constant values). The intended use for this is synthesis-time DRC.
 
 
@@ -410,7 +410,7 @@ On Ubuntu, texlive needs these packages to be able to build the manual:
 	sudo apt-get install texlive-fonts-extra  # gets skull.sty and dsfont.sty
 	sudo apt-get install texlive-publishers   # IEEEtran.cls
 
-Also the non-free font luximono should be installed, there is unfortulately
+Also the non-free font luximono should be installed, there is unfortunately
 no Ubuntu package for this so it should be installed separately using
 `getnonfreefonts`:
 

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
@@ -37,7 +37,7 @@ struct Smt2Worker
 
 	std::vector<std::string> decls, trans, hier;
 	std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
-	std::set<RTLIL::Cell*> exported_cells, hiercells;
+	std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
 	pool<Cell*> recursive_cells, registers;
 
 	std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
@@ -581,23 +581,8 @@ struct Smt2Worker
 					get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
 
 			hiercells.insert(cell);
+			hiercells_queue.insert(cell);
 			recursive_cells.erase(cell);
-
-			for (auto &conn : cell->connections())
-			{
-				Wire *w = m->wire(conn.first);
-				SigSpec sig = sigmap(conn.second);
-
-				if (bvmode || GetSize(w) == 1) {
-					hier.push_back(stringf("  (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
-							get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
-				} else {
-					for (int i = 0; i < GetSize(w); i++)
-						hier.push_back(stringf("  (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
-								get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
-				}
-			}
-
 			return;
 		}
 
@@ -736,10 +721,64 @@ struct Smt2Worker
 					std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
 					std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
 					trans.push_back(stringf("  (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
+
+					Const init_data = cell->getParam("\\INIT");
+					int memsize = cell->getParam("\\SIZE").as_int();
+
+					for (int i = 0; i < memsize; i++)
+					{
+						if (i*width >= GetSize(init_data))
+							break;
+
+						Const initword = init_data.extract(i*width, width, State::Sx);
+						bool gen_init_constr = false;
+
+						for (auto bit : initword.bits)
+							if (bit == State::S0 || bit == State::S1)
+								gen_init_constr = true;
+
+						if (gen_init_constr) {
+							init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+									get_id(module), arrayid, Const(i, abits).as_string().c_str(),
+									initword.as_string().c_str(), get_id(cell), i));
+						}
+					}
 				}
 			}
 		}
 
+		if (verbose) log("=> export logic driving hierarchical cells\n");
+
+		while (!hiercells_queue.empty())
+		{
+			std::set<RTLIL::Cell*> queue;
+			queue.swap(hiercells_queue);
+
+			for (auto cell : queue)
+			{
+				string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
+				Module *m = module->design->module(cell->type);
+				log_assert(m != nullptr);
+
+				for (auto &conn : cell->connections())
+				{
+					Wire *w = m->wire(conn.first);
+					SigSpec sig = sigmap(conn.second);
+
+					if (bvmode || GetSize(w) == 1) {
+						hier.push_back(stringf("  (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
+								get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
+					} else {
+						for (int i = 0; i < GetSize(w); i++)
+							hier.push_back(stringf("  (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
+									get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
+					}
+				}
+			}
+		}
+
+		if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module));
+
 		for (auto c : hiercells) {
 			assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
 			assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name)));
@@ -751,27 +790,39 @@ struct Smt2Worker
 
 		string assert_expr = assert_list.empty() ? "true" : "(and";
 		if (!assert_list.empty()) {
-			for (auto &str : assert_list)
-				assert_expr += stringf("\n  %s", str.c_str());
-			assert_expr += "\n)";
+			if (GetSize(assert_list) == 1) {
+				assert_expr = "\n  " + assert_list.front() + "\n";
+			} else {
+				for (auto &str : assert_list)
+					assert_expr += stringf("\n  %s", str.c_str());
+				assert_expr += "\n)";
+			}
 		}
 		decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n",
 				get_id(module), get_id(module), assert_expr.c_str()));
 
 		string assume_expr = assume_list.empty() ? "true" : "(and";
 		if (!assume_list.empty()) {
-			for (auto &str : assume_list)
-				assume_expr += stringf("\n  %s", str.c_str());
-			assume_expr += "\n)";
+			if (GetSize(assume_list) == 1) {
+				assume_expr = "\n  " + assume_list.front() + "\n";
+			} else {
+				for (auto &str : assume_list)
+					assume_expr += stringf("\n  %s", str.c_str());
+				assume_expr += "\n)";
+			}
 		}
 		decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n",
 				get_id(module), get_id(module), assume_expr.c_str()));
 
 		string init_expr = init_list.empty() ? "true" : "(and";
 		if (!init_list.empty()) {
-			for (auto &str : init_list)
-				init_expr += stringf("\n  %s", str.c_str());
-			init_expr += "\n)";
+			if (GetSize(init_list) == 1) {
+				init_expr = "\n  " + init_list.front() + "\n";
+			} else {
+				for (auto &str : init_list)
+					init_expr += stringf("\n  %s", str.c_str());
+				init_expr += "\n)";
+			}
 		}
 		decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n",
 				get_id(module), get_id(module), init_expr.c_str()));
@@ -852,8 +903,8 @@ struct Smt2Backend : public Backend {
 		log("        this will print the recursive walk used to export the modules.\n");
 		log("\n");
 		log("    -nobv\n");
-		log("        disable support for BitVec (FixedSizeBitVectors theory). with this\n");
-		log("        option set multi-bit wires are represented using the BitVec sort and\n");
+		log("        disable support for BitVec (FixedSizeBitVectors theory). without this\n");
+		log("        option multi-bit wires are represented using the BitVec sort and\n");
 		log("        support for coarse grain cells (incl. arithmetic) is enabled.\n");
 		log("\n");
 		log("    -nomem\n");
@@ -866,7 +917,7 @@ struct Smt2Backend : public Backend {
 		log("\n");
 		log("    -wires\n");
 		log("        create '<mod>_n' functions for all public wires. by default only ports,\n");
-		log("        registers, and wires with the 'keep' attribute set are exported.\n");
+		log("        registers, and wires with the 'keep' attribute are exported.\n");
 		log("\n");
 		log("    -tpl <template_file>\n");
 		log("        use the given template file. the line containing only the token '%%%%'\n");
@@ -947,7 +998,7 @@ struct Smt2Backend : public Backend {
 				continue;
 			}
 			if (args[argidx] == "-nomem") {
-				bvmode = false;
+				memmode = false;
 				continue;
 			}
 			if (args[argidx] == "-wires") {
@@ -976,6 +1027,12 @@ struct Smt2Backend : public Backend {
 
 		*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
 
+		if (!bvmode)
+			*f << stringf("; yosys-smt2-nobv\n");
+
+		if (!memmode)
+			*f << stringf("; yosys-smt2-nomem\n");
+
 		std::vector<RTLIL::Module*> sorted_modules;
 
 		// extract module dependencies