Merge pull request #1156 from YosysHQ/eddie/fix_abc9_unknown_cell

write_xaiger to treat unknown cell connections as keep-s

backends/aiger/xaiger.cc

@@ -138,6 +138,7 @@ struct XAigerWriter
 	{
 		pool<SigBit> undriven_bits;
 		pool<SigBit> unused_bits;
+		pool<SigBit> keep_bits;
 
 		// promote public wires
 		for (auto wire : module->wires())
@@ -168,6 +169,9 @@ struct XAigerWriter
 					unused_bits.insert(bit);
 				}
 
+				if (keep)
+					keep_bits.insert(bit);
+
 				if (wire->port_input || keep) {
 					if (bit != wirebit)
 						alias_map[bit] = wirebit;
@@ -235,7 +239,7 @@ 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")) {
+			if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
 				abc_box_seen = true;
 
 				if (!holes_mode) {
@@ -255,10 +259,11 @@ struct XAigerWriter
 				}
 			}
 			else {
+				bool cell_known = cell->known();
 				for (const auto &c : cell->connections()) {
 					if (c.second.is_fully_const()) continue;
-					auto is_input = cell->input(c.first);
-					auto is_output = cell->output(c.first);
+					auto is_input = !cell_known || cell->input(c.first);
+					auto is_output = !cell_known || cell->output(c.first);
 					if (!is_input && !is_output)
 						log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
 
@@ -266,12 +271,15 @@ struct XAigerWriter
 						for (auto b : c.second.bits()) {
 							Wire *w = b.wire;
 							if (!w) continue;
-							if (!w->port_output) {
+							if (!w->port_output || !cell_known) {
 								SigBit I = sigmap(b);
 								if (I != b)
 									alias_map[b] = I;
 								output_bits.insert(b);
 								unused_bits.erase(b);
+
+								if (!cell_known)
+									keep_bits.insert(b);
 							}
 						}
 					}
@@ -424,7 +432,7 @@ struct XAigerWriter
 
 							auto jt = input_bits.find(b);
 							if (jt != input_bits.end()) {
-								log_assert(b.wire->attributes.count("\\keep"));
+								log_assert(keep_bits.count(O));
 								input_bits.erase(b);
 							}
 						}
@@ -444,7 +452,7 @@ struct XAigerWriter
 			// with $inout.out suffix, make it a PO driven by the existing inout, and
 			// inherit existing inout's drivers
 			if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
-					|| wire->attributes.count("\\keep")) {
+					|| keep_bits.count(bit)) {
 				RTLIL::IdString wire_name = wire->name.str() + "$inout.out";
 				RTLIL::Wire *new_wire = module->wire(wire_name);
 				if (!new_wire)

tests/various/abc9.v

@@ -3,3 +3,7 @@ initial o = 1'b0;
 always @*
     o <= ~o;
 endmodule
+
+module abc9_test028(input i, output o);
+unknown u(~i, o);
+endmodule

tests/various/abc9.ys

@@ -1,4 +1,6 @@
 read_verilog abc9.v
+design -save read
+hierarchy -top abc9_test027
 proc
 design -save gold
 
@@ -12,3 +14,11 @@ design -import gate -as gate
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -show-ports miter
 
+design -load read
+hierarchy -top abc9_test028
+proc
+
+abc9 -lut 4
+select -assert-count 1 t:$lut r:LUT=1 r:WIDTH=1 %i %i
+select -assert-count 1 t:unknown
+select -assert-none t:$lut t:unknown %% t: %D