Merge branch 'master' of github.com:YosysHQ/yosys

7 files changed, 150 insertions, 62 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 0798fb35d..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)
@@ -777,7 +780,7 @@ struct AigerBackend : public Backend {
 			}
 			break;
 		}
-		extra_args(f, filename, args, argidx);
+		extra_args(f, filename, args, argidx, !ascii_mode);
 
 		Module *top_module = design->top_module();
 
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index fa6ba0aca..46890b071 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -203,7 +203,7 @@ struct XAigerWriter
 		//       box ordering, but not individual AIG cells
 		dict<SigBit, pool<IdString>> bit_drivers, bit_users;
 		TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
-		bool abc_box_seen = false;
+		bool abc9_box_seen = false;
 
 		for (auto cell : module->selected_cells()) {
 			if (cell->type == "$_NOT_")
@@ -242,8 +242,8 @@ struct XAigerWriter
 			log_assert(!holes_mode);
 
 			RTLIL::Module* inst_module = module->design->module(cell->type);
-			if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
-				abc_box_seen = true;
+			if (inst_module && inst_module->attributes.count("\\abc9_box_id")) {
+				abc9_box_seen = true;
 
 				if (!holes_mode) {
 					toposort.node(cell->name);
@@ -291,10 +291,10 @@ struct XAigerWriter
 					if (is_output) {
 						int arrival = 0;
 						if (port_wire) {
-							auto it = port_wire->attributes.find("\\abc_arrival");
+							auto it = port_wire->attributes.find("\\abc9_arrival");
 							if (it != port_wire->attributes.end()) {
 								if (it->second.flags != 0)
-									log_error("Attribute 'abc_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
+									log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
 								arrival = it->second.as_int();
 							}
 						}
@@ -318,7 +318,7 @@ struct XAigerWriter
 			//log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
 		}
 
-		if (abc_box_seen) {
+		if (abc9_box_seen) {
 			for (auto &it : bit_users)
 				if (bit_drivers.count(it.first))
 					for (auto driver_cell : bit_drivers.at(it.first))
@@ -347,9 +347,11 @@ struct XAigerWriter
 				log_assert(cell);
 
 				RTLIL::Module* box_module = module->design->module(cell->type);
-				if (!box_module || !box_module->attributes.count("\\abc_box_id"))
+				if (!box_module || !box_module->attributes.count("\\abc9_box_id"))
 					continue;
 
+				bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */);
+
 				// Fully pad all unused input connections of this box cell with S0
 				// Fully pad all undriven output connections of this box cell with anonymous wires
 				// NB: Assume box_module->ports are sorted alphabetically
@@ -394,7 +396,10 @@ struct XAigerWriter
 							rhs = it->second;
 						}
 						else {
-							rhs = module->addWire(NEW_ID, GetSize(w));
+							Wire *wire = module->addWire(NEW_ID, GetSize(w));
+							if (blackbox)
+								wire->set_bool_attribute(ID(abc9_padding));
+							rhs = wire;
 							cell->setPort(port_name, rhs);
 						}
 
@@ -405,12 +410,7 @@ struct XAigerWriter
 							if (O != b)
 								alias_map[O] = b;
 							undriven_bits.erase(O);
-
-							auto jt = input_bits.find(b);
-							if (jt != input_bits.end()) {
-								log_assert(keep_bits.count(O));
-								input_bits.erase(b);
-							}
+							input_bits.erase(b);
 						}
 					}
 				}
@@ -429,7 +429,7 @@ struct XAigerWriter
 			// inherit existing inout's drivers
 			if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
 					|| keep_bits.count(bit)) {
-				RTLIL::IdString wire_name = wire->name.str() + "$inout.out";
+				RTLIL::IdString wire_name = stringf("$%s$inout.out", wire->name.c_str());
 				RTLIL::Wire *new_wire = module->wire(wire_name);
 				if (!new_wire)
 					new_wire = module->addWire(wire_name, GetSize(wire));
@@ -666,7 +666,7 @@ struct XAigerWriter
 
 				write_h_buffer(box_inputs);
 				write_h_buffer(box_outputs);
-				write_h_buffer(box_module->attributes.at("\\abc_box_id").as_int());
+				write_h_buffer(box_module->attributes.at("\\abc9_box_id").as_int());
 				write_h_buffer(box_count++);
 			}
 
@@ -856,7 +856,7 @@ struct XAigerBackend : public Backend {
 			}
 			break;
 		}
-		extra_args(f, filename, args, argidx);
+		extra_args(f, filename, args, argidx, !ascii_mode);
 
 		Module *top_module = design->top_module();
 
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 4472993d4..c1da4b127 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -569,7 +569,7 @@ struct BtorWorker
 			int nid_init_val = -1;
 
 			if (!initval.is_fully_undef())
-				nid_init_val = get_sig_nid(initval);
+				nid_init_val = get_sig_nid(initval, -1, false, true);
 
 			int sid = get_bv_sid(GetSize(sig_q));
 			int nid = next_nid++;
@@ -681,7 +681,7 @@ struct BtorWorker
 				{
 					if (verbose)
 						btorf("; initval = %s\n", log_signal(firstword));
-					nid_init_val = get_sig_nid(firstword);
+					nid_init_val = get_sig_nid(firstword, -1, false, true);
 				}
 				else
 				{
@@ -693,8 +693,8 @@ struct BtorWorker
 						if (thisword.is_fully_undef())
 							continue;
 						Const thisaddr(i, abits);
-						int nid_thisword = get_sig_nid(thisword);
-						int nid_thisaddr = get_sig_nid(thisaddr);
+						int nid_thisword = get_sig_nid(thisword, -1, false, true);
+						int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true);
 						int last_nid_init_val = nid_init_val;
 						nid_init_val = next_nid++;
 						if (verbose)
@@ -792,7 +792,7 @@ struct BtorWorker
 		cell_recursion_guard.erase(cell);
 	}
 
-	int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
+	int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
 	{
 		int nid = -1;
 		sigmap.apply(sig);
@@ -823,7 +823,10 @@ struct BtorWorker
 				int sid = get_bv_sid(GetSize(sig));
 
 				int nid_input = next_nid++;
-				btorf("%d input %d\n", nid_input, sid);
+				if (is_init)
+					btorf("%d state %d\n", nid_input, sid);
+				else
+					btorf("%d input %d\n", nid_input, sid);
 
 				int nid_masked_input;
 				if (sig_mask_undef.is_fully_ones()) {
@@ -897,9 +900,12 @@ struct BtorWorker
 
 							int sid = get_bv_sid(GetSize(s));
 							int nid = next_nid++;
-							btorf("%d input %d %s\n", nid, sid);
+							btorf("%d input %d\n", nid, sid);
 							nid_width[nid] = GetSize(s);
 
+							for (int j = 0; j < GetSize(s); j++)
+								nidbits.push_back(make_pair(nid, j));
+
 							i += GetSize(s)-1;
 							continue;
 						}
@@ -1064,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/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
index fff110bb0..671686173 100644
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@@ -266,7 +266,7 @@ struct ProtobufBackend : public Backend {
 			}
 			break;
 		}
-		extra_args(f, filename, args, argidx);
+		extra_args(f, filename, args, argidx, !text_mode);
 
 		log_header(design, "Executing Protobuf backend.\n");
 
@@ -338,7 +338,7 @@ struct ProtobufPass : public Pass {
 		if (!filename.empty()) {
 			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
-			ff->open(filename.c_str(), std::ofstream::trunc);
+			ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary));
 			if (ff->fail()) {
 				delete ff;
 				log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 445a42e0d..3d6d3e1b3 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1256,7 +1256,7 @@ def smt_check_sat():
     return smt.check_sat()
 
 if tempind:
-    retstatus = False
+    retstatus = "FAILED"
     skip_counter = step_size
     for step in range(num_steps, -1, -1):
         if smt.forall:
@@ -1303,7 +1303,7 @@ if tempind:
 
         else:
             print_msg("Temporal induction successful.")
-            retstatus = True
+            retstatus = "PASSED"
             break
 
 elif covermode:
@@ -1321,7 +1321,7 @@ elif covermode:
     smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
 
     step = 0
-    retstatus = False
+    retstatus = "FAILED"
     found_failed_assert = False
 
     assert step_size == 1
@@ -1365,7 +1365,7 @@ elif covermode:
                 if smt_check_sat() == "unsat":
                     print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
                     found_failed_assert = True
-                    retstatus = False
+                    retstatus = "FAILED"
                     break
 
             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
@@ -1400,7 +1400,7 @@ elif covermode:
             break
 
         if "1" not in cover_mask:
-            retstatus = True
+            retstatus = "PASSED"
             break
 
         step += 1
@@ -1412,7 +1412,7 @@ elif covermode:
 
 else:  # not tempind, covermode
     step = 0
-    retstatus = True
+    retstatus = "PASSED"
     while step < num_steps:
         smt_state(step)
         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
@@ -1459,8 +1459,8 @@ else:  # not tempind, covermode
                     print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
 
                 if smt_check_sat() == "unsat":
-                    print("%s Warmup failed!" % smt.timestamp())
-                    retstatus = False
+                    print("%s Assumptions are unsatisfiable!" % smt.timestamp())
+                    retstatus = "PREUNSAT"
                     break
 
             if not final_only:
@@ -1487,13 +1487,13 @@ else:  # not tempind, covermode
                         print_msg("Re-solving with appended steps..")
                         if smt_check_sat() == "unsat":
                             print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
-                            retstatus = False
+                            retstatus = "FAILED"
                             break
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
                     write_trace(0, last_check_step+1+append_steps, '%')
-                    retstatus = False
+                    retstatus = "FAILED"
                     break
 
                 smt_pop()
@@ -1519,7 +1519,7 @@ else:  # not tempind, covermode
                         print_anyconsts(i)
                         print_failed_asserts(i, final=True)
                         write_trace(0, i+1, '%')
-                        retstatus = False
+                        retstatus = "FAILED"
                         break
 
                     smt_pop()
@@ -1534,7 +1534,7 @@ else:  # not tempind, covermode
             print_msg("Solving for step %d.." % (last_check_step))
             if smt_check_sat() != "sat":
                 print("%s No solution found!" % smt.timestamp())
-                retstatus = False
+                retstatus = "FAILED"
                 break
 
             elif dumpall:
@@ -1551,5 +1551,5 @@ else:  # not tempind, covermode
 smt.write("(exit)")
 smt.wait()
 
-print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)"))
-sys.exit(0 if retstatus else 1)
+print_msg("Status: %s" % retstatus)
+sys.exit(0 if retstatus == "PASSED" else 1)
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();