From e47f5369fd897dab4c3c8da2143986dd7d040411 Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Wed, 9 Jul 2025 15:58:35 +0200
Subject: [PATCH] verificsva: check -L value is small enough for code to work

---
 frontends/verific/verific.cc    | 3 +++
 frontends/verific/verificsva.cc | 8 ++++----
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index d83db3410..241b2db30 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -4124,6 +4124,9 @@ struct VerificPass : public Pass {
 			if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
 				cmd_error(args, argidx, "unknown option");
 
+			if ((unsigned long)verific_sva_fsm_limit >= sizeof(1ull)*8)
+				log_cmd_error("-L %d: limit too large; maximum allowed value is %zu.\n", verific_sva_fsm_limit, sizeof(1ull)*8-1);
+
 			std::set<std::string> top_mod_names;
 
 			if (mode_all)
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 7652f8130..6e87bd267 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -479,14 +479,14 @@ struct SvaFsm
 					GetSize(dnode.ctrl), verific_sva_fsm_limit);
 		}
 
-		for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
+		for (unsigned long long i = 0; i < (1ull << GetSize(dnode.ctrl)); i++)
 		{
 			Const ctrl_val(i, GetSize(dnode.ctrl));
 			pool<SigBit> ctrl_bits;
 
-			for (int i = 0; i < GetSize(dnode.ctrl); i++)
-				if (ctrl_val[i] == State::S1)
-					ctrl_bits.insert(dnode.ctrl[i]);
+			for (int j = 0; j < GetSize(dnode.ctrl); j++)
+				if (ctrl_val[j] == State::S1)
+					ctrl_bits.insert(dnode.ctrl[j]);
 
 			vector<int> new_state;
 			bool accept = false, cond = false;