From 45d654e2d7baf332b33e7b7bd00c81019c7606ac Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Wed, 17 Dec 2025 20:25:24 +0100
Subject: [PATCH] avoid merging formal properties

---
 frontends/ast/genrtlil.cc         |  1 +
 frontends/verific/verificsva.cc   |  5 ++++-
 passes/opt/opt_merge.cc           |  5 +++++
 tests/opt/opt_merge_properties.ys | 16 ++++++++++++++++
 4 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 tests/opt/opt_merge_properties.ys

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index c26750c98..86ea70b51 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -844,6 +844,7 @@ struct AST_INTERNAL::ProcessGenerator
 
 				RTLIL::Cell *cell = current_module->addCell(cellname, ID($check));
 				set_src_attr(cell, ast);
+				cell->set_bool_attribute(ID(keep));
 				for (auto &attr : ast->attributes) {
 					if (attr.second->type != AST_CONSTANT)
 						log_file_error(*ast->location.begin.filename, ast->location.begin.line, "Attribute `%s' with non-constant value!\n", attr.first);
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index dffe6e8e0..c2cfe7e75 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1846,7 +1846,10 @@ struct VerificSvaImporter
 				if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q);
 				if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q);
 
-				if (c) importer->import_attributes(c->attributes, root);
+				if (c) {
+					c->set_bool_attribute(ID(keep));
+					importer->import_attributes(c->attributes, root);
+				}
 			}
 		}
 		catch (ParserErrorException)
diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc
index 6cdcbc822..307c2bcd3 100644
--- a/passes/opt/opt_merge.cc
+++ b/passes/opt/opt_merge.cc
@@ -227,6 +227,11 @@ struct OptMergeWorker
 		ct.cell_types.erase(ID($anyconst));
 		ct.cell_types.erase(ID($allseq));
 		ct.cell_types.erase(ID($allconst));
+		ct.cell_types.erase(ID($check));
+		ct.cell_types.erase(ID($assert));
+		ct.cell_types.erase(ID($assume));
+		ct.cell_types.erase(ID($live));
+		ct.cell_types.erase(ID($cover));
 
 		log("Finding identical cells in module `%s'.\n", module->name);
 		assign_map.set(module);
diff --git a/tests/opt/opt_merge_properties.ys b/tests/opt/opt_merge_properties.ys
new file mode 100644
index 000000000..dddc13bfb
--- /dev/null
+++ b/tests/opt/opt_merge_properties.ys
@@ -0,0 +1,16 @@
+read_verilog -sv <<EOF
+module top ();
+    always_comb begin
+        label1: cover(0);
+        label2: cover(0);
+    end
+endmodule
+EOF
+
+hierarchy -top top
+proc
+chformal -lower
+clean
+opt_merge
+select -assert-count 2 t:$cover
+