Various equiv_simple improvements

kernel/satgen.h

@@ -1163,6 +1163,25 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$_BUF_" || cell->type == "$equiv")
+		{
+			std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
+			std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
+			extendSignalWidthUnary(a, y, cell);
+
+			std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+			ez->assume(ez->vec_eq(a, yy));
+
+			if (model_undef) {
+				std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
+				std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
+				extendSignalWidthUnary(undef_a, undef_y, cell, false);
+				ez->assume(ez->vec_eq(undef_a, undef_y));
+				undefGating(y, yy, undef_y);
+			}
+			return true;
+		}
+
 		if (cell->type == "$assert")
 		{
 			std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));

passes/equiv/equiv_simple.cc

@@ -34,10 +34,11 @@ struct EquivSimpleWorker
 	ezDefaultSAT ez;
 	SatGen satgen;
 	int max_seq;
+	bool verbose;
 
-	EquivSimpleWorker(Cell *equiv_cell, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq) :
+	EquivSimpleWorker(Cell *equiv_cell, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq, bool verbose) :
 			module(equiv_cell->module), equiv_cell(equiv_cell), sigmap(sigmap),
-			bit2driver(bit2driver), satgen(&ez, &sigmap), max_seq(max_seq)
+			bit2driver(bit2driver), satgen(&ez, &sigmap), max_seq(max_seq), verbose(verbose)
 	{
 	}
 
@@ -90,8 +91,12 @@ struct EquivSimpleWorker
 		pool<SigBit> seed_a = { bit_a };
 		pool<SigBit> seed_b = { bit_b };
 
+		if (verbose) {
 			log("  Trying to prove $equiv cell %s:\n", log_id(equiv_cell));
 			log("    A = %s, B = %s, Y = %s\n", log_signal(bit_a), log_signal(bit_b), log_signal(equiv_cell->getPort("\\Y")));
+		} else {
+			log("  Trying to prove $equiv for %s:", log_signal(equiv_cell->getPort("\\Y")));
+		}
 
 		int step = max_seq;
 		while (1)
@@ -127,43 +132,52 @@ struct EquivSimpleWorker
 			problem_cells.insert(short_cells_cone_a.begin(), short_cells_cone_a.end());
 			problem_cells.insert(short_cells_cone_b.begin(), short_cells_cone_b.end());
 
+			if (verbose)
 				log("    Adding %d new cells to the problem (%d A, %d B, %d shared).\n",
 						GetSize(problem_cells), GetSize(short_cells_cone_a), GetSize(short_cells_cone_b),
 						(GetSize(short_cells_cone_a) + GetSize(short_cells_cone_b)) - GetSize(problem_cells));
 
 			for (auto cell : problem_cells)
-				satgen.importCell(cell, step+1);
+				if (!satgen.importCell(cell, step+1))
+					log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
 
+			if (verbose)
 				log("    Problem size at t=%d: %d literals, %d clauses\n", step, ez.numCnfVariables(), ez.numCnfClauses());
 
 			if (!ez.solve()) {
-				log("    Proved equivalence! Marking $equiv cell as proven.\n");
+				log(verbose ? "    Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n");
 				equiv_cell->setPort("\\B", equiv_cell->getPort("\\A"));
 				return true;
 			}
 
+			if (verbose)
 				log("    Failed to prove equivalence with sequence length %d.\n", max_seq - step);
 
 			if (--step < 0) {
+				if (verbose)
 					log("    Reached sequence limit.\n");
 				break;
 			}
 
 			if (seed_a.empty() && seed_b.empty()) {
+				if (verbose)
 					log("    No nets to continue in previous time step.\n");
 				break;
 			}
 
 			if (seed_a.empty()) {
+				if (verbose)
 					log("    No nets on A-side to continue in previous time step.\n");
 				break;
 			}
 
 			if (seed_b.empty()) {
+				if (verbose)
 					log("    No nets on B-side to continue in previous time step.\n");
 				break;
 			}
 
+			if (verbose) {
 			#if 0
 				log("    Continuing analysis in previous time step with the following nets:\n");
 				for (auto bit : seed_a)
@@ -174,7 +188,10 @@ struct EquivSimpleWorker
 				log("    Continuing analysis in previous time step with %d A- and %d B-nets.\n", GetSize(seed_a), GetSize(seed_b));
 			#endif
 			}
+		}
 
+		if (!verbose)
+			log(" failed.\n");
 		return false;
 	}
 };
@@ -189,12 +206,16 @@ struct EquivSimplePass : public Pass {
 		log("\n");
 		log("This command tries to prove $equiv cells using a simple direct SAT approach.\n");
 		log("\n");
+		log("    -v\n");
+		log("        verbose output\n");
+		log("\n");
 		log("    -seq <N>\n");
 		log("        the max. number of time steps to be considered (default = 1)\n");
 		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, Design *design)
 	{
+		bool verbose = false;
 		int success_counter = 0;
 		int max_seq = 1;
 
@@ -202,6 +223,10 @@ struct EquivSimplePass : public Pass {
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-v") {
+				verbose = true;
+				continue;
+			}
 			if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 				max_seq = atoi(args[++argidx].c_str());
 				continue;
@@ -240,7 +265,7 @@ struct EquivSimplePass : public Pass {
 			}
 
 			for (auto cell : unproven_equiv_cells) {
-				EquivSimpleWorker worker(cell, sigmap, bit2driver, max_seq);
+				EquivSimpleWorker worker(cell, sigmap, bit2driver, max_seq, verbose);
 				if (worker.run())
 					success_counter++;
 			}