Merge 6bf9fc1817 into 967b47d984

passes/equiv/equiv_make.cc

@@ -34,6 +34,7 @@ struct EquivMakeWorker
 	vector<string> blacklists;
 	vector<string> encfiles;
 	bool make_assert;
+	bool nocells;
 
 	pool<IdString> blacklist_names;
 	dict<IdString, dict<Const, Const>> encdata;
@@ -419,7 +420,8 @@ struct EquivMakeWorker
 		copy_to_equiv();
 		find_undriven_nets(false);
 		find_same_wires();
-		find_same_cells();
+		if (!nocells)
+			find_same_cells();
 		find_undriven_nets(true);
 	}
 };
@@ -450,6 +452,9 @@ struct EquivMakePass : public Pass {
 		log("        Check equivalence with $assert cells instead of $equiv.\n");
 		log("        $eqx (===) is used to compare signals.");
 		log("\n");
+		log("    -nocells\n");
+		log("        Do not check for equivalent cells, just wires.\n");
+		log("\n");
 		log("Note: The circuit created by this command is not a miter (with something like\n");
 		log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
 		log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
@@ -461,6 +466,7 @@ struct EquivMakePass : public Pass {
 		worker.ct.setup(design);
 		worker.inames = false;
 		worker.make_assert = false;
+		worker.nocells = false;
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
@@ -481,6 +487,10 @@ struct EquivMakePass : public Pass {
 				worker.make_assert = true;
 				continue;
 			}
+			if (args[argidx] == "-nocells") {
+				worker.nocells = true;
+				continue;
+			}
 			break;
 		}
 

passes/equiv/equiv_opt.cc

@@ -60,6 +60,9 @@ struct EquivOptPass:public ScriptPass
 		log("    -undef\n");
 		log("        enable modelling of undef states during equiv_induct.\n");
 		log("\n");
+		log("    -nocells\n");
+		log("        Do not check for equivalent cells, just wires.\n");
+		log("\n");
 		log("    -nocheck\n");
 		log("        disable running check before and after the command under test.\n");
 		log("\n");
@@ -126,6 +129,10 @@ struct EquivOptPass:public ScriptPass
 				async2sync = true;
 				continue;
 			}
+			if (args[argidx] == "-nocells") {
+				make_opts += " -nocells";
+				continue;
+			}
 			break;
 		}
 

tests/various/equiv_nocells.ys

@@ -0,0 +1,13 @@
+read_verilog <<EOT
+module gold(input a, input b, output y);
+    assign y = a & b;
+endmodule
+
+module gate(input a, input b, output y);
+    assign y = a & b;
+endmodule
+EOT
+
+equiv_make -nocells gold gate equiv
+equiv_simple equiv
+equiv_status -assert equiv