From b1eeb7de3d1fbe7648ffb9819f16b9b6f552af93 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Wed, 6 Aug 2025 15:21:10 +1200
Subject: [PATCH] Less verbose equiv assumes

both only print on the first step, and equiv_simple only prints if also verbose
---
 passes/equiv/equiv_induct.cc | 10 ++++++----
 passes/equiv/equiv_simple.cc | 10 ++++++----
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index b39d7a785..1995be3cd 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -79,10 +79,12 @@ struct EquivInductWorker
 		}
 
 		if (set_assumes) {
-			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]));
+			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));
 		}
 
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index bdb39172b..1bebf5454 100644
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -243,10 +243,12 @@ struct EquivSimpleWorker
 			}
 
 			if (set_assumes) {
-				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.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
+				if (verbose && step == 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));
 			}