Merge remote-tracking branch 'origin/master' into xaig_dff

4 files changed, 103 insertions, 21 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 3e8b14dee..44718baae 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -91,6 +91,9 @@ struct AigerWriter
 		} else
 		if (alias_map.count(bit)) {
 			a = bit2aig(alias_map.at(bit));
+		} else
+		if (initstate_bits.count(bit)) {
+			a = initstate_ff;
 		}
 
 		if (bit == State::Sx || bit == State::Sz)
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 9e316a055..c1da4b127 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -1070,7 +1070,12 @@ struct BtorWorker
 					bad_properties.push_back(nid_en_and_not_a);
 				} else {
 					int nid = next_nid++;
-					btorf("%d bad %d\n", nid, nid_en_and_not_a);
+					string infostr = log_id(cell);
+					if (infostr[0] == '$' && cell->attributes.count("\\src")) {
+						infostr = cell->attributes.at("\\src").decode_string().c_str();
+						std::replace(infostr.begin(), infostr.end(), ' ', '_');
+					}
+					btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str());
 				}
 
 				btorf_pop(log_id(cell));
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index bac68ac70..1df996aa7 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -1032,12 +1032,17 @@ class MkVcd:
                 print("$var integer 32 t smt_step $end", file=self.f)
                 print("$var event 1 ! smt_clock $end", file=self.f)
 
+                def vcdescape(n):
+                    if n.startswith("$") or ":" in n:
+                        return "\\" + n
+                    return n
+
                 scope = []
                 for path in sorted(self.nets):
                     key, width = self.nets[path]
 
                     uipath = list(path)
-                    if "." in uipath[-1]:
+                    if "." in uipath[-1] and not uipath[-1].startswith("$"):
                         uipath = uipath[0:-1] + uipath[-1].split(".")
                     for i in range(len(uipath)):
                         uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i])
@@ -1048,15 +1053,13 @@ class MkVcd:
 
                     while uipath[:-1] != scope:
                         scopename = uipath[len(scope)]
-                        if scopename.startswith("$"):
-                            scopename = "\\" + scopename
-                        print("$scope module %s $end" % scopename, file=self.f)
+                        print("$scope module %s $end" % vcdescape(scopename), file=self.f)
                         scope.append(uipath[len(scope)])
 
                     if path in self.clocks and self.clocks[path][1] == "event":
-                        print("$var event 1 %s %s $end" % (key, uipath[-1]), file=self.f)
+                        print("$var event 1 %s %s $end" % (key, vcdescape(uipath[-1])), file=self.f)
                     else:
-                        print("$var wire %d %s %s $end" % (width, key, uipath[-1]), file=self.f)
+                        print("$var wire %d %s %s $end" % (width, key, vcdescape(uipath[-1])), file=self.f)
 
                 for i in range(len(scope)):
                     print("$upscope $end", file=self.f)
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 7b1db4776..54d0f6148 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -33,11 +33,11 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal, siminit;
-int auto_name_counter, auto_name_offset, auto_name_digits;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit;
+int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter;
 std::map<RTLIL::IdString, int> auto_name_map;
 std::set<RTLIL::IdString> reg_wires, reg_ct;
-std::string auto_prefix;
+std::string auto_prefix, extmem_prefix;
 
 RTLIL::Module *active_module;
 dict<RTLIL::SigBit, RTLIL::State> active_initdata;
@@ -371,13 +371,14 @@ void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig)
 	}
 }
 
-void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false, bool as_comment = false)
+void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString, RTLIL::Const> &attributes, char term = '\n', bool modattr = false, bool regattr = false, bool as_comment = false)
 {
 	if (noattr)
 		return;
 	if (attr2comment)
 		as_comment = true;
 	for (auto it = attributes.begin(); it != attributes.end(); ++it) {
+		if (it->first == "\\init" && regattr) continue;
 		f << stringf("%s" "%s %s", indent.c_str(), as_comment ? "/*" : "(*", id(it->first).c_str());
 		f << stringf(" = ");
 		if (modattr && (it->second == State::S0 || it->second == Const(0)))
@@ -392,7 +393,7 @@ void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString,
 
 void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 {
-	dump_attributes(f, indent, wire->attributes);
+	dump_attributes(f, indent, wire->attributes, '\n', /*modattr=*/false, /*regattr=*/reg_wires.count(wire->name));
 #if 0
 	if (wire->port_input && !wire->port_output)
 		f << stringf("%s" "input %s", indent.c_str(), reg_wires.count(wire->name) ? "reg " : "");
@@ -1068,14 +1069,64 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size+offset-1, offset);
 		if (use_init)
 		{
-			f << stringf("%s" "initial begin\n", indent.c_str());
-			for (int i=0; i<size; i++)
+			if (extmem)
+			{
+				std::string extmem_filename = stringf("%s-%d.mem", extmem_prefix.c_str(), extmem_counter++);
+
+				std::string extmem_filename_esc;
+				for (auto c : extmem_filename)
+				{
+					if (c == '\n')
+						extmem_filename_esc += "\\n";
+					else if (c == '\t')
+						extmem_filename_esc += "\\t";
+					else if (c < 32)
+						extmem_filename_esc += stringf("\\%03o", c);
+					else if (c == '"')
+						extmem_filename_esc += "\\\"";
+					else if (c == '\\')
+						extmem_filename_esc += "\\\\";
+					else
+						extmem_filename_esc += c;
+				}
+				f << stringf("%s" "initial $readmemb(\"%s\", %s);\n", indent.c_str(), extmem_filename_esc.c_str(), mem_id.c_str());
+
+				std::ofstream extmem_f(extmem_filename, std::ofstream::trunc);
+				if (extmem_f.fail())
+					log_error("Can't open file `%s' for writing: %s\n", extmem_filename.c_str(), strerror(errno));
+				else
+				{
+					for (int i=0; i<size; i++)
+					{
+						RTLIL::Const element = cell->parameters["\\INIT"].extract(i*width, width);
+						for (int j=0; j<element.size(); j++)
+						{
+							switch (element[element.size()-j-1])
+							{
+								case State::S0: extmem_f << '0'; break;
+								case State::S1: extmem_f << '1'; break;
+								case State::Sx: extmem_f << 'x'; break;
+								case State::Sz: extmem_f << 'z'; break;
+								case State::Sa: extmem_f << '_'; break;
+								case State::Sm: log_error("Found marker state in final netlist.");
+							}
+						}
+						extmem_f << '\n';
+					}
+				}
+
+			}
+			else
 			{
-				f << stringf("%s" "  %s[%d] = ", indent.c_str(), mem_id.c_str(), i);
-				dump_const(f, cell->parameters["\\INIT"].extract(i*width, width));
-				f << stringf(";\n");
+				f << stringf("%s" "initial begin\n", indent.c_str());
+				for (int i=0; i<size; i++)
+				{
+					f << stringf("%s" "  %s[%d] = ", indent.c_str(), mem_id.c_str(), i);
+					dump_const(f, cell->parameters["\\INIT"].extract(i*width, width));
+					f << stringf(";\n");
+				}
+				f << stringf("%s" "end\n", indent.c_str());
 			}
-			f << stringf("%s" "end\n", indent.c_str());
 		}
 
 		// create a map : "edge clk" -> expressions within that clock domain
@@ -1521,7 +1572,7 @@ void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw
 
 	bool got_default = false;
 	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it) {
-		dump_attributes(f, indent + "  ", (*it)->attributes, '\n', /*modattr=*/false, /*as_comment=*/true);
+		dump_attributes(f, indent + "  ", (*it)->attributes, '\n', /*modattr=*/false, /*regattr=*/false, /*as_comment=*/true);
 		if ((*it)->compare.size() == 0) {
 			if (got_default)
 				continue;
@@ -1686,7 +1737,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 		}
 	}
 
-	dump_attributes(f, indent, module->attributes, '\n', /*attr2comment=*/true);
+	dump_attributes(f, indent, module->attributes, '\n', /*modattr=*/true);
 	f << stringf("%s" "module %s(", indent.c_str(), id(module->name, false).c_str());
 	bool keep_running = true;
 	for (int port_id = 1; keep_running; port_id++) {
@@ -1776,8 +1827,16 @@ struct VerilogBackend : public Backend {
 		log("        deactivates this feature and instead will write string constants\n");
 		log("        as binary numbers.\n");
 		log("\n");
+		log("    -extmem\n");
+		log("        instead of initializing memories using assignments to individual\n");
+		log("        elements, use the '$readmemh' function to read initialization data\n");
+		log("        from a file. This data is written to a file named by appending\n");
+		log("        a sequential index to the Verilog filename and replacing the extension\n");
+		log("        with '.mem', e.g. 'write_verilog -extmem foo.v' writes 'foo-1.mem',\n");
+		log("        'foo-2.mem' and so on.\n");
+		log("\n");
 		log("    -defparam\n");
-		log("        Use 'defparam' statements instead of the Verilog-2001 syntax for\n");
+		log("        use 'defparam' statements instead of the Verilog-2001 syntax for\n");
 		log("        cell parameters.\n");
 		log("\n");
 		log("    -blackboxes\n");
@@ -1811,6 +1870,7 @@ struct VerilogBackend : public Backend {
 		nodec = false;
 		nohex = false;
 		nostr = false;
+		extmem = false;
 		defparam = false;
 		decimal = false;
 		siminit = false;
@@ -1884,6 +1944,11 @@ struct VerilogBackend : public Backend {
 				nostr = true;
 				continue;
 			}
+			if (arg == "-extmem") {
+				extmem = true;
+				extmem_counter = 1;
+				continue;
+			}
 			if (arg == "-defparam") {
 				defparam = true;
 				continue;
@@ -1911,6 +1976,12 @@ struct VerilogBackend : public Backend {
 			break;
 		}
 		extra_args(f, filename, args, argidx);
+		if (extmem)
+		{
+			if (filename.empty())
+				log_cmd_error("Option -extmem must be used with a filename.\n");
+			extmem_prefix = filename.substr(0, filename.rfind('.'));
+		}
 
 		design->sort();