From 8d1c1faf82ec085c9756a31010ed9d50d06334d3 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Tue, 3 Feb 2026 17:59:31 +0100
Subject: [PATCH] equiv_simple, equiv_induct: error by default on missing
 model, add -ignore-unknown-cells

---
 passes/equiv/equiv.h         | 8 ++++++++
 passes/equiv/equiv_induct.cc | 2 +-
 passes/equiv/equiv_simple.cc | 2 +-
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h
index b255042ba..8a24b2fcd 100644
--- a/passes/equiv/equiv.h
+++ b/passes/equiv/equiv.h
@@ -33,6 +33,7 @@ struct EquivWorker {
 		bool model_undef = false;
 		int max_seq = 1;
 		bool set_assumes = false;
+		bool ignore_unknown_cells = false;
 
 		bool parse(const std::vector<std::string>& args, size_t& idx) {
 			if (args[idx] == "-undef") {
@@ -47,6 +48,10 @@ struct EquivWorker {
 				set_assumes = true;
 				return true;
 			}
+			if (args[idx] == "-ignore-unknown-cells") {
+				ignore_unknown_cells = true;
+				return true;
+			}
 			return false;
 		}
 		static std::string help(const char* default_seq) {
@@ -59,6 +64,9 @@ struct EquivWorker {
 			"\n"
 			"    -set-assumes\n"
 			"        set all assumptions provided via $assume cells\n"
+			"\n"
+			"    -ignore-unknown-cells\n"
+			"        ignore all cells that can not be matched to a SAT model\n"
 			, default_seq);
 		}
     };
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index c91501719..f7ceb78a3 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -45,7 +45,7 @@ struct EquivInductWorker : public EquivWorker
 
 		for (auto cell : cells) {
 			if (!satgen.importCell(cell, step)) {
-				report_missing_model(true, cell);
+				report_missing_model(cfg.ignore_unknown_cells, cell);
 			}
 			if (cell->type == ID($equiv)) {
 				SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit();
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 0749d18aa..f345e9794 100644
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -336,7 +336,7 @@ struct EquivSimpleWorker : public EquivWorker
 			for (auto cell : problem_cells) {
 				auto key = pair<Cell*, int>(cell, step+1);
 				if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) {
-					report_missing_model(true, cell);
+					report_missing_model(cfg.ignore_unknown_cells, cell);
 				}
 				imported_cells_cache.insert(key);
 			}