Merge pull request #5233 from YosysHQ/krys/equiv_assume

Assumptions for equiv_*

kernel/satgen.h

@@ -64,7 +64,7 @@ struct ezSatPtr : public std::unique_ptr<ezSAT> {
 struct SatGen
 {
 	ezSAT *ez;
-	SigMap *sigmap;
+	const SigMap *sigmap;
 	std::string prefix;
 	SigPool initial_state;
 	std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en;
@@ -75,12 +75,12 @@ struct SatGen
 	bool model_undef;
 	bool def_formal = false;
 
-	SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
+	SatGen(ezSAT *ez, const SigMap *sigmap, std::string prefix = std::string()) :
 			ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
 	{
 	}
 
-	void setContext(SigMap *sigmap, std::string prefix = std::string())
+	void setContext(const SigMap *sigmap, std::string prefix = std::string())
 	{
 		this->sigmap = sigmap;
 		this->prefix = prefix;

passes/equiv/equiv_induct.cc

@@ -37,14 +37,15 @@ struct EquivInductWorker
 
 	int max_seq;
 	int success_counter;
+	bool set_assumes;
 
 	dict<int, int> ez_step_is_consistent;
 	pool<Cell*> cell_warn_cache;
 	SigPool undriven_signals;
 
-	EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq) : module(module), sigmap(module),
+	EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module),
 			cells(module->selected_cells()), workset(unproven_equiv_cells),
-			satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0)
+			satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes)
 	{
 		satgen.model_undef = model_undef;
 	}
@@ -77,6 +78,16 @@ struct EquivInductWorker
 			}
 		}
 
+		if (set_assumes) {
+			if (step == 1) {
+				RTLIL::SigSpec assumes_a, assumes_en;
+				satgen.getAssumes(assumes_a, assumes_en, step);
+				for (int i = 0; i < GetSize(assumes_a); i++)
+					log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
+			}
+			ez->assume(satgen.importAssumes(step));
+		}
+
 		if (satgen.model_undef) {
 			for (auto bit : undriven_signals.export_all())
 				ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step)));
@@ -184,6 +195,9 @@ struct EquivInductPass : public Pass {
 		log("    -seq <N>\n");
 		log("        the max. number of time steps to be considered (default = 4)\n");
 		log("\n");
+		log("    -set-assumes\n");
+		log("        set all assumptions provided via $assume cells\n");
+		log("\n");
 		log("This command is very effective in proving complex sequential circuits, when\n");
 		log("the internal state of the circuit quickly propagates to $equiv cells.\n");
 		log("\n");
@@ -200,7 +214,7 @@ struct EquivInductPass : public Pass {
 	void execute(std::vector<std::string> args, Design *design) override
 	{
 		int success_counter = 0;
-		bool model_undef = false;
+		bool model_undef = false, set_assumes = false;
 		int max_seq = 4;
 
 		log_header(design, "Executing EQUIV_INDUCT pass.\n");
@@ -215,6 +229,10 @@ struct EquivInductPass : public Pass {
 				max_seq = atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (args[argidx] == "-set-assumes") {
+				set_assumes = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -222,6 +240,7 @@ struct EquivInductPass : public Pass {
 		for (auto module : design->selected_modules())
 		{
 			pool<Cell*> unproven_equiv_cells;
+			vector<Cell*> assume_cells;
 
 			for (auto cell : module->selected_cells())
 				if (cell->type == ID($equiv)) {
@@ -234,7 +253,7 @@ struct EquivInductPass : public Pass {
 				continue;
 			}
 
-			EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq);
+			EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes);
 			worker.run();
 			success_counter += worker.success_counter;
 		}

passes/equiv/equiv_simple.cc

@@ -27,215 +27,345 @@ struct EquivSimpleWorker
 {
 	Module *module;
 	const vector<Cell*> &equiv_cells;
-	Cell *equiv_cell;
+	const vector<Cell*> &assume_cells;
+	struct Cone {
+		pool<Cell*> cells;
+		pool<SigBit> bits;
+		void clear() {
+			cells.clear();
+			bits.clear();
+		}
+	};
 
-	SigMap &sigmap;
+	struct DesignModel {
-	dict<SigBit, Cell*> &bit2driver;
+		const SigMap &sigmap;
+		dict<SigBit, Cell*> &bit2driver;
+	};
+	DesignModel model;
 
 	ezSatPtr ez;
 	SatGen satgen;
-	int max_seq;
+
-	bool short_cones;
+	struct Config {
-	bool verbose;
+		bool verbose = false;
+		bool short_cones = false;
+		bool model_undef = false;
+		bool nogroup = false;
+		bool set_assumes = false;
+		int max_seq = 1;
+	};
+	Config cfg;
 
 	pool<pair<Cell*, int>> imported_cells_cache;
 
-	EquivSimpleWorker(const vector<Cell*> &equiv_cells, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq, bool short_cones, bool verbose, bool model_undef) :
+	EquivSimpleWorker(const vector<Cell*> &equiv_cells, const vector<Cell*> &assume_cells, DesignModel model, Config cfg) :
-			module(equiv_cells.front()->module), equiv_cells(equiv_cells), equiv_cell(nullptr),
+			module(equiv_cells.front()->module), equiv_cells(equiv_cells), assume_cells(assume_cells),
-			sigmap(sigmap), bit2driver(bit2driver), satgen(ez.get(), &sigmap), max_seq(max_seq), short_cones(short_cones), verbose(verbose)
+			model(model), satgen(ez.get(), &model.sigmap), cfg(cfg)
 	{
-		satgen.model_undef = model_undef;
+		satgen.model_undef = cfg.model_undef;
 	}
 
-	bool find_input_cone(pool<SigBit> &next_seed, pool<Cell*> &cells_cone, pool<SigBit> &bits_cone, const pool<Cell*> &cells_stop, const pool<SigBit> &bits_stop, pool<SigBit> *input_bits, Cell *cell)
+	struct ConeFinder {
-	{
+		DesignModel model;
-		if (cells_cone.count(cell))
+		// Bits we should also analyze in a later iteration (flop inputs)
+		pool<SigBit> &next_seed;
+		// Cells and bits we've seen so far while traversing
+		Cone& cone;
+		// We're not allowed to traverse past cells and bits in `stop`
+		const Cone& stop;
+		// Input bits are bits that no longer can be traversed
+		// Tracking these is optional
+		pool<SigBit>* input_bits;
+
+		// Recursively traverses backwards from a cell to find all cells in its input cone
+		// Adds cell to cone.cells, stops at cells in 'stop' set
+		// Returns true if stopped on a stop cell
+		bool find_input_cone(Cell *cell)
+		{
+			if (cone.cells.count(cell))
+				return false;
+
+			cone.cells.insert(cell);
+
+			if (stop.cells.count(cell))
+				return true;
+
+			for (auto &conn : cell->connections())
+				if (yosys_celltypes.cell_input(cell->type, conn.first))
+					for (auto bit : model.sigmap(conn.second)) {
+						if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+							if (!conn.first.in(ID::CLK, ID::C))
+								next_seed.insert(bit);
+						} else
+							find_input_cone(bit);
+					}
 			return false;
+		}
+		void find_input_cone(SigBit bit)
+		{
+			if (cone.bits.count(bit))
+				return;
 
-		cells_cone.insert(cell);
+			cone.bits.insert(bit);
 
-		if (cells_stop.count(cell))
+			if (stop.bits.count(bit)) {
-			return true;
+				if (input_bits != nullptr) input_bits->insert(bit);
+				return;
+			}
 
-		for (auto &conn : cell->connections())
+			if (!model.bit2driver.count(bit))
-			if (yosys_celltypes.cell_input(cell->type, conn.first))
+				return;
-				for (auto bit : sigmap(conn.second)) {
-					if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
-						if (!conn.first.in(ID::CLK, ID::C))
-							next_seed.insert(bit);
-					} else
-						find_input_cone(next_seed, cells_cone, bits_cone, cells_stop, bits_stop, input_bits, bit);
-				}
-		return false;
-	}
 
-	void find_input_cone(pool<SigBit> &next_seed, pool<Cell*> &cells_cone, pool<SigBit> &bits_cone, const pool<Cell*> &cells_stop, const pool<SigBit> &bits_stop, pool<SigBit> *input_bits, SigBit bit)
+			// If the input cone of the driver cell reaches a stop bit,
+			// then `bit` is an "input bit"
+			if (find_input_cone(model.bit2driver.at(bit)))
+				if (input_bits != nullptr) input_bits->insert(bit);
+		}
+		void find_input_cone(pool<SigBit> bits)
+		{
+			for (auto bit : bits)
+				find_input_cone(bit);
+		}
+	};
+
+	// Builds (full or short) input cones from the seeds
+	// Creates full cones (no stops) and optionally short cones (stop at other side's cone)
+	// Updates seed_a/seed_b with next iteration's FF inputs
+	// Returns input bits and cone structures for SAT problem construction
+	std::tuple<pool<SigBit>, Cone, Cone> init_iter(pool<SigBit>& seed_a, pool<SigBit>& seed_b) const
 	{
-		if (bits_cone.count(bit))
+		// Empty, never inserted to, to traverse full cones
-			return;
+		const Cone no_stop;
+		Cone full_cone_a, full_cone_b;
 
-		bits_cone.insert(bit);
+		// Values of seed_* for the next iteration
+		pool<SigBit> next_seed_a, next_seed_b;
 
-		if (bits_stop.count(bit)) {
+		{
-			if (input_bits != nullptr) input_bits->insert(bit);
+			ConeFinder finder_a {model, next_seed_a, full_cone_a, no_stop, nullptr};
-			return;
+			finder_a.find_input_cone(seed_a);
+
+			ConeFinder finder_b {model, next_seed_b, full_cone_b, no_stop, nullptr};
+			finder_b.find_input_cone(seed_b);
 		}
 
-		if (!bit2driver.count(bit))
+		Cone short_cone_a, short_cone_b;
-			return;
+		pool<SigBit> input_bits;
 
-		if (find_input_cone(next_seed, cells_cone, bits_cone, cells_stop, bits_stop, input_bits, bit2driver.at(bit)))
+		if (cfg.short_cones)
-			if (input_bits != nullptr) input_bits->insert(bit);
+		{
+			// Rebuild cones with the knowledge of the full cones.
+			// Avoids stuffing overlaps in input cones into the solver
+			// e.g. for A by using the full B cone as stops
+			next_seed_a.clear();
+			ConeFinder short_finder_a = {model, next_seed_a, short_cone_a, short_cone_b, &input_bits};
+			short_finder_a.find_input_cone(seed_a);
+			next_seed_a.swap(seed_a);
+
+			next_seed_b.clear();
+			ConeFinder short_finder_b = {model, next_seed_b, short_cone_b, short_cone_a, &input_bits};
+			short_finder_b.find_input_cone(seed_b);
+			next_seed_b.swap(seed_b);
+		}
+		else
+		{
+			short_cone_a = full_cone_a;
+			next_seed_a.swap(seed_a);
+
+			short_cone_b = full_cone_b;
+			next_seed_b.swap(seed_b);
+		}
+		return std::make_tuple(input_bits, short_cone_a, short_cone_b);
 	}
 
-	bool run_cell()
+	void report_new_cells(const pool<Cell*>& cells, const Cone& cone_a, const Cone& cone_b) const
 	{
-		SigBit bit_a = sigmap(equiv_cell->getPort(ID::A)).as_bit();
+		log("    Adding %d new cells to the problem (%d A, %d B, %d shared).\n",
-		SigBit bit_b = sigmap(equiv_cell->getPort(ID::B)).as_bit();
+					GetSize(cells), GetSize(cone_a.cells), GetSize(cone_b.cells),
-		int ez_context = ez->frozen_literal();
+					(GetSize(cone_a.cells) + GetSize(cone_b.cells)) - GetSize(cells));
+		#if 0
+			for (auto cell : short_cells_cone_a)
+				log("      A-side cell: %s\n", log_id(cell));
 
+			for (auto cell : short_cells_cone_b)
+				log("      B-side cell: %s\n", log_id(cell));
+		#endif
+	}
+	void report_new_assume_cells(const pool<Cell*>& extra_problem_cells, int old_size, const pool<Cell*>& problem_cells) const
+	{
+		if (cfg.verbose) {
+			log("    Adding %d new cells to check assumptions (and reusing %d).\n",
+				GetSize(problem_cells) - old_size,
+				old_size - (GetSize(problem_cells) - GetSize(extra_problem_cells)));
+		#if 0
+			for (auto cell : extra_problem_cells)
+				log("      cell: %s\n", log_id(cell));
+		#endif
+		}
+	}
+
+	// Ensure the input cones of $assume cells get modelled by the problem
+	pool<Cell*> add_assumes_to_problem(const Cone& cone_a, const Cone& cone_b) const
+	{
+		pool<Cell*> extra_problem_cells;
+		for (auto assume : assume_cells) {
+			pool<SigBit> assume_seed, dummy_next_seed, overlap_bits;
+			assume_seed.insert(model.sigmap(assume->getPort(ID::A)).as_bit());
+			assume_seed.insert(model.sigmap(assume->getPort(ID::EN)).as_bit());
+
+			for (auto& cone : {cone_a, cone_b}) {
+				Cone assume_cone;
+				ConeFinder{model, dummy_next_seed, assume_cone, cone, &overlap_bits}
+					.find_input_cone(assume_seed);
+				if (GetSize(overlap_bits)) {
+					extra_problem_cells.insert(assume);
+					extra_problem_cells.insert(assume_cone.cells.begin(), assume_cone.cells.end());
+					overlap_bits.clear();
+				}
+				assume_cone.clear();
+				dummy_next_seed.clear();
+			}
+		}
+		return extra_problem_cells;
+	}
+
+	static void report_missing_model(Cell* cell)
+	{
+		if (RTLIL::builtin_ff_cell_types().count(cell->type))
+			log_cmd_error("No SAT model available for async FF cell %s (%s).  Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
+		else
+			log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
+	}
+
+	void prepare_ezsat(int ez_context, SigBit bit_a, SigBit bit_b)
+	{
 		if (satgen.model_undef)
 		{
-			int ez_a = satgen.importSigBit(bit_a, max_seq+1);
+			int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1);
-			int ez_b = satgen.importDefSigBit(bit_b, max_seq+1);
+			int ez_b = satgen.importDefSigBit(bit_b, cfg.max_seq+1);
-			int ez_undef_a = satgen.importUndefSigBit(bit_a, max_seq+1);
+			int ez_undef_a = satgen.importUndefSigBit(bit_a, cfg.max_seq+1);
 
 			ez->assume(ez->XOR(ez_a, ez_b), ez_context);
 			ez->assume(ez->NOT(ez_undef_a), ez_context);
 		}
 		else
 		{
-			int ez_a = satgen.importSigBit(bit_a, max_seq+1);
+			int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1);
-			int ez_b = satgen.importSigBit(bit_b, max_seq+1);
+			int ez_b = satgen.importSigBit(bit_b, cfg.max_seq+1);
 			ez->assume(ez->XOR(ez_a, ez_b), ez_context);
 		}
+	}
+	void construct_ezsat(const pool<SigBit>& input_bits, int step)
+	{
+		if (cfg.set_assumes) {
+			if (cfg.verbose && step == cfg.max_seq) {
+				RTLIL::SigSpec assumes_a, assumes_en;
+				satgen.getAssumes(assumes_a, assumes_en, step+1);
+				for (int i = 0; i < GetSize(assumes_a); i++)
+					log("    Import constraint from assume cell: %s when %s (%d).\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]), step);
+			}
+			ez->assume(satgen.importAssumes(step+1));
+		}
 
+		if (satgen.model_undef) {
+			for (auto bit : input_bits)
+				ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step+1)));
+		}
+
+		if (cfg.verbose)
+			log("    Problem size at t=%d: %d literals, %d clauses\n", step, ez->numCnfVariables(), ez->numCnfClauses());
+	}
+
+	bool prove_equiv_cell(Cell* cell)
+	{
+		SigBit bit_a = model.sigmap(cell->getPort(ID::A)).as_bit();
+		SigBit bit_b = model.sigmap(cell->getPort(ID::B)).as_bit();
+		int ez_context = ez->frozen_literal();
+
+		prepare_ezsat(ez_context, bit_a, bit_b);
+
+		// Two bits, bit_a, and bit_b, have been marked equivalent in the design
+		// We will be traversing the input cones for each of them
+		// In the first iteration, we will using those as starting points
 		pool<SigBit> seed_a = { bit_a };
 		pool<SigBit> seed_b = { bit_b };
 
-		if (verbose) {
+		if (cfg.verbose) {
-			log("  Trying to prove $equiv cell %s:\n", log_id(equiv_cell));
+			log("  Trying to prove $equiv cell %s:\n", log_id(cell));
-			log("    A = %s, B = %s, Y = %s\n", log_signal(bit_a), log_signal(bit_b), log_signal(equiv_cell->getPort(ID::Y)));
+			log("    A = %s, B = %s, Y = %s\n", log_signal(bit_a), log_signal(bit_b), log_signal(cell->getPort(ID::Y)));
 		} else {
-			log("  Trying to prove $equiv for %s:", log_signal(equiv_cell->getPort(ID::Y)));
+			log("  Trying to prove $equiv for %s:", log_signal(cell->getPort(ID::Y)));
 		}
 
-		int step = max_seq;
+		int step = cfg.max_seq;
 		while (1)
 		{
-			pool<Cell*> no_stop_cells;
+			// Traverse input cones of seed_a and seed_b, potentially finding new seeds
-			pool<SigBit> no_stop_bits;
+			auto [input_bits, cone_a, cone_b] = init_iter(seed_a, seed_b);
-
-			pool<Cell*> full_cells_cone_a, full_cells_cone_b;
-			pool<SigBit> full_bits_cone_a, full_bits_cone_b;
-
-			pool<SigBit> next_seed_a, next_seed_b;
-
-			for (auto bit_a : seed_a)
-				find_input_cone(next_seed_a, full_cells_cone_a, full_bits_cone_a, no_stop_cells, no_stop_bits, nullptr, bit_a);
-
-			for (auto bit_b : seed_b)
-				find_input_cone(next_seed_b, full_cells_cone_b, full_bits_cone_b, no_stop_cells, no_stop_bits, nullptr, bit_b);
-
-			pool<Cell*> short_cells_cone_a, short_cells_cone_b;
-			pool<SigBit> short_bits_cone_a, short_bits_cone_b;
-			pool<SigBit> input_bits;
-
-			if (short_cones)
-			{
-				next_seed_a.clear();
-				for (auto bit_a : seed_a)
-					find_input_cone(next_seed_a, short_cells_cone_a, short_bits_cone_a, full_cells_cone_b, full_bits_cone_b, &input_bits, bit_a);
-				next_seed_a.swap(seed_a);
-
-				next_seed_b.clear();
-				for (auto bit_b : seed_b)
-					find_input_cone(next_seed_b, short_cells_cone_b, short_bits_cone_b, full_cells_cone_a, full_bits_cone_a, &input_bits, bit_b);
-				next_seed_b.swap(seed_b);
-			}
-			else
-			{
-				short_cells_cone_a = full_cells_cone_a;
-				short_bits_cone_a = full_bits_cone_a;
-				next_seed_a.swap(seed_a);
-
-				short_cells_cone_b = full_cells_cone_b;
-				short_bits_cone_b = full_bits_cone_b;
-				next_seed_b.swap(seed_b);
-			}
 
+			// Cells to model in SAT solver
 			pool<Cell*> problem_cells;
-			problem_cells.insert(short_cells_cone_a.begin(), short_cells_cone_a.end());
+			problem_cells.insert(cone_a.cells.begin(), cone_a.cells.end());
-			problem_cells.insert(short_cells_cone_b.begin(), short_cells_cone_b.end());
+			problem_cells.insert(cone_b.cells.begin(), cone_b.cells.end());
 
-			if (verbose)
+			if (cfg.verbose)
-			{
+				report_new_cells(problem_cells, cone_a, cone_b);
-				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));
-			#if 0
-				for (auto cell : short_cells_cone_a)
-					log("      A-side cell: %s\n", log_id(cell));
 
-				for (auto cell : short_cells_cone_b)
+			if (cfg.set_assumes) {
-					log("      B-side cell: %s\n", log_id(cell));
+				auto extras = add_assumes_to_problem(cone_a, cone_b);
-			#endif
+				if (GetSize(extras)) {
+					auto old_size = GetSize(problem_cells);
+					problem_cells.insert(extras.begin(), extras.end());
+					report_new_assume_cells(extras, old_size, problem_cells);
+				}
 			}
 
 			for (auto cell : problem_cells) {
 				auto key = pair<Cell*, int>(cell, step+1);
 				if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) {
-					if (RTLIL::builtin_ff_cell_types().count(cell->type))
+					report_missing_model(cell);
-						log_cmd_error("No SAT model available for async FF cell %s (%s).  Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
-					else
-						log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
 				}
 				imported_cells_cache.insert(key);
 			}
 
-			if (satgen.model_undef) {
+			construct_ezsat(input_bits, step);
-				for (auto bit : input_bits)
-					ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step+1)));
-			}
-
-			if (verbose)
-				log("    Problem size at t=%d: %d literals, %d clauses\n", step, ez->numCnfVariables(), ez->numCnfClauses());
 
 			if (!ez->solve(ez_context)) {
-				log(verbose ? "    Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n");
+				log(cfg.verbose ? "    Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n");
-				equiv_cell->setPort(ID::B, equiv_cell->getPort(ID::A));
+				// Replace $equiv cell with a short
+				cell->setPort(ID::B, cell->getPort(ID::A));
 				ez->assume(ez->NOT(ez_context));
 				return true;
 			}
 
-			if (verbose)
+			if (cfg.verbose)
-				log("    Failed to prove equivalence with sequence length %d.\n", max_seq - step);
+				log("    Failed to prove equivalence with sequence length %d.\n", cfg.max_seq - step);
 
 			if (--step < 0) {
-				if (verbose)
+				if (cfg.verbose)
 					log("    Reached sequence limit.\n");
 				break;
 			}
 
 			if (seed_a.empty() && seed_b.empty()) {
-				if (verbose)
+				if (cfg.verbose)
 					log("    No nets to continue in previous time step.\n");
 				break;
 			}
 
 			if (seed_a.empty()) {
-				if (verbose)
+				if (cfg.verbose)
 					log("    No nets on A-side to continue in previous time step.\n");
 				break;
 			}
 
 			if (seed_b.empty()) {
-				if (verbose)
+				if (cfg.verbose)
 					log("    No nets on B-side to continue in previous time step.\n");
 				break;
 			}
 
-			if (verbose) {
+			if (cfg.verbose) {
 			#if 0
 				log("    Continuing analysis in previous time step with the following nets:\n");
 				for (auto bit : seed_a)
@@ -248,7 +378,7 @@ struct EquivSimpleWorker
 			}
 		}
 
-		if (!verbose)
+		if (!cfg.verbose)
 			log(" failed.\n");
 
 		ez->assume(ez->NOT(ez_context));
@@ -260,14 +390,13 @@ struct EquivSimpleWorker
 		if (GetSize(equiv_cells) > 1) {
 			SigSpec sig;
 			for (auto c : equiv_cells)
-				sig.append(sigmap(c->getPort(ID::Y)));
+				sig.append(model.sigmap(c->getPort(ID::Y)));
 			log(" Grouping SAT models for %s:\n", log_signal(sig));
 		}
 
 		int counter = 0;
 		for (auto c : equiv_cells) {
-			equiv_cell = c;
+			if (prove_equiv_cell(c))
-			if (run_cell())
 				counter++;
 		}
 		return counter;
@@ -301,35 +430,41 @@ struct EquivSimplePass : public Pass {
 		log("    -seq <N>\n");
 		log("        the max. number of time steps to be considered (default = 1)\n");
 		log("\n");
+		log("    -set-assumes\n");
+		log("        set all assumptions provided via $assume cells\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, Design *design) override
 	{
-		bool verbose = false, short_cones = false, model_undef = false, nogroup = false;
+		EquivSimpleWorker::Config cfg = {};
 		int success_counter = 0;
-		int max_seq = 1;
 
 		log_header(design, "Executing EQUIV_SIMPLE pass.\n");
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
 			if (args[argidx] == "-v") {
-				verbose = true;
+				cfg.verbose = true;
 				continue;
 			}
 			if (args[argidx] == "-short") {
-				short_cones = true;
+				cfg.short_cones = true;
 				continue;
 			}
 			if (args[argidx] == "-undef") {
-				model_undef = true;
+				cfg.model_undef = true;
 				continue;
 			}
 			if (args[argidx] == "-nogroup") {
-				nogroup = true;
+				cfg.nogroup = true;
 				continue;
 			}
 			if (args[argidx] == "-seq" && argidx+1 < args.size()) {
-				max_seq = atoi(args[++argidx].c_str());
+				cfg.max_seq = atoi(args[++argidx].c_str());
+				continue;
+			}
+			if (args[argidx] == "-set-assumes") {
+				cfg.set_assumes = true;
 				continue;
 			}
 			break;
@@ -347,17 +482,21 @@ struct EquivSimplePass : public Pass {
 			SigMap sigmap(module);
 			dict<SigBit, Cell*> bit2driver;
 			dict<SigBit, dict<SigBit, Cell*>> unproven_equiv_cells;
+			vector<Cell*> assumes;
 			int unproven_cells_counter = 0;
 
-			for (auto cell : module->selected_cells())
+			for (auto cell : module->selected_cells()) {
 				if (cell->type == ID($equiv) && cell->getPort(ID::A) != cell->getPort(ID::B)) {
 					auto bit = sigmap(cell->getPort(ID::Y).as_bit());
 					auto bit_group = bit;
-					if (!nogroup && bit_group.wire)
+					if (!cfg.nogroup && bit_group.wire)
 						bit_group.offset = 0;
 					unproven_equiv_cells[bit_group][bit] = cell;
 					unproven_cells_counter++;
+				} else if (cell->type == ID($assume)) {
+					assumes.push_back(cell);
 				}
+			}
 
 			if (unproven_equiv_cells.empty())
 				continue;
@@ -375,15 +514,16 @@ struct EquivSimplePass : public Pass {
 			}
 
 			unproven_equiv_cells.sort();
-			for (auto it : unproven_equiv_cells)
+			for (auto [_, d] : unproven_equiv_cells)
 			{
-				it.second.sort();
+				d.sort();
 
 				vector<Cell*> cells;
-				for (auto it2 : it.second)
+				for (auto [_, cell] : d)
-					cells.push_back(it2.second);
+					cells.push_back(cell);
 
-				EquivSimpleWorker worker(cells, sigmap, bit2driver, max_seq, short_cones, verbose, model_undef);
+				EquivSimpleWorker::DesignModel model {sigmap, bit2driver};
+				EquivSimpleWorker worker(cells, assumes, model, cfg);
 				success_counter += worker.run();
 			}
 		}

tests/various/equiv_assume.ys

@@ -0,0 +1,141 @@
+read_verilog -sv <<EOT
+module gold (input D, output Q);
+assign Q = '0;
+endmodule
+
+module gate (input D, output Q);
+assume property (D == '0);
+assign Q = D;
+endmodule
+EOT
+
+chformal -lower
+async2sync
+design -stash input
+
+# using $assert cells in sat verifies
+design -load input
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts -verify
+# this fails
+# sat -prove-asserts -verify
+
+# so should $equiv
+## in equiv_simple
+design -load input
+equiv_make gold gate equiv
+equiv_simple -set-assumes equiv
+equiv_status -assert equiv
+
+## and equiv_induct
+delete equiv
+equiv_make gold gate equiv
+equiv_induct -set-assumes equiv
+equiv_status -assert equiv
+
+# and it works through cells
+design -reset
+read_verilog -sv <<EOT
+module gold (input [1:0] D, output [1:0] Q);
+assign Q = !D;
+endmodule
+
+module gate (input [1:0] D, output [1:0] Q);
+assume property (D == 2'b11);
+wire [1:0] G = ~D;
+assign Q = G;
+endmodule
+EOT
+
+chformal -lower
+async2sync
+design -stash input2
+
+design -load input2
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts -verify
+
+design -load input2
+equiv_make gold gate equiv
+equiv_simple -set-assumes equiv
+equiv_status -assert equiv
+
+delete equiv
+equiv_make gold gate equiv
+equiv_induct -set-assumes equiv
+equiv_status -assert equiv
+
+# and registers
+design -reset
+read_verilog -sv <<EOT
+module gold (input clk, input [1:0] D, output [1:0] Q);
+assign Q = '0;
+endmodule
+
+module gate (input clk, input [1:0] D, output [1:0] Q);
+reg [1:0] Dreg;
+assume property (Dreg == 2'b11);
+always @(clk) begin
+    Dreg <= D;
+end
+assign Q = ~Dreg;
+endmodule
+EOT
+
+proc
+chformal -lower
+async2sync
+design -stash input3
+
+design -load input3
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts -verify
+
+design -load input3
+equiv_make gold gate equiv
+equiv_simple -set-assumes equiv
+equiv_status -assert equiv
+
+delete equiv
+equiv_make gold gate equiv
+equiv_induct -set-assumes equiv
+equiv_status -assert equiv
+
+# so long as the assumption doesn't end up after the equiv
+design -reset
+read_verilog -sv <<EOT
+module gold (input [1:0] D, output [1:0] Q);
+assign Q = !D;
+endmodule
+
+module gate (input [1:0] D, output [1:0] Q);
+assume property (G == 2'b00);
+wire [1:0] G = ~D;
+assign Q = G;
+endmodule
+EOT
+
+chformal -lower
+async2sync
+design -stash input4
+
+logger -expect log "model found: FAIL!" 1
+logger -expect log "Found a total of 2 unproven .equiv cells." 2
+
+design -load input4
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts
+
+design -load input4
+equiv_make gold gate equiv
+equiv_simple -set-assumes equiv
+equiv_status equiv
+
+delete equiv
+equiv_make gold gate equiv
+equiv_induct -set-assumes equiv
+equiv_status equiv