From 3deb8f313e3351206dc4d3f86fdc4ac10b6ee2f9 Mon Sep 17 00:00:00 2001
From: nick <nickrallison1@gmail.com>
Date: Tue, 1 Sep 2026 14:34:28 -0600
Subject: [PATCH] fix 6151 - adding error cases to formal backends / also
 adding test cases

---
 backends/btor/btor.cc                         |  9 +++++++
 backends/smt2/smt2.cc                         |  3 +++
 tests/various/btor_allconst.ys                | 13 ++++++++++
 tests/various/btor_allseq.ys                  | 13 ++++++++++
 ...heck_cells_btor.ys => btor_check_cells.ys} |  0
 tests/various/btor_equiv_cells.ys             | 26 +++++++++++++++++++
 tests/various/btor_fair_cells.ys              | 11 ++++++++
 tests/various/btor_live_cells.ys              | 11 ++++++++
 ...heck_cells_smt2.ys => smt2_check_cells.ys} |  0
 tests/various/smt2_equiv_cells.ys             | 26 +++++++++++++++++++
 tests/various/smt2_fair_cells.ys              | 11 ++++++++
 tests/various/smt2_live_cells.ys              | 11 ++++++++
 12 files changed, 134 insertions(+)
 create mode 100644 tests/various/btor_allconst.ys
 create mode 100644 tests/various/btor_allseq.ys
 rename tests/various/{check_cells_btor.ys => btor_check_cells.ys} (100%)
 create mode 100644 tests/various/btor_equiv_cells.ys
 create mode 100644 tests/various/btor_fair_cells.ys
 create mode 100644 tests/various/btor_live_cells.ys
 rename tests/various/{check_cells_smt2.ys => smt2_check_cells.ys} (100%)
 create mode 100644 tests/various/smt2_equiv_cells.ys
 create mode 100644 tests/various/smt2_fair_cells.ys
 create mode 100644 tests/various/smt2_live_cells.ys

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index d9d23ad7b..51f28afcd 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -745,6 +745,11 @@ struct BtorWorker
 			goto okay;
 		}
 
+		if (cell->type.in(ID($allconst), ID($allseq)))
+			log_error("Unsupported cell type %s for cell %s.%s",
+					cell->type.unescape(), module, cell);
+
+
 		if (cell->type.in(ID($anyconst), ID($anyseq)))
 		{
 			SigSpec sig_y = sigmap(cell->getPort(ID::Y));
@@ -1270,6 +1275,10 @@ struct BtorWorker
 				log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync` or `clk2fflogic` before `write_btor`.\n",
 						cell->type.unescape(), module, cell);
 
+			if (cell->type.in(ID($live), ID($fair), ID($equiv)))
+				log_error("Unsupported cell type %s for cell %s.%s",
+						cell->type.unescape(), module, cell);
+
 			if (cell->type == ID($assume))
 			{
 				btorf_push(cell->name.unescape());
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 88044359f..40587edae 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1110,6 +1110,9 @@ struct Smt2Worker
 			if (cell->type == ID($check))
 				log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync` or `clk2fflogic` before `write_smt2`.\n",
 						cell->type.unescape(), module, cell);
+			if (cell->type.in(ID($live), ID($fair), ID($equiv)))
+				log_error("Unsupported cell type %s for cell %s.%s",
+						cell->type.unescape(), module, cell);
 
 			if (cell->type.in(ID($assert), ID($assume), ID($cover)))
 			{
diff --git a/tests/various/btor_allconst.ys b/tests/various/btor_allconst.ys
new file mode 100644
index 000000000..ff52a498e
--- /dev/null
+++ b/tests/various/btor_allconst.ys
@@ -0,0 +1,13 @@
+
+read_verilog -formal <<EOT
+module top (input clk, input req, output reg ack);
+	(* allconst *) reg test;
+    always @(posedge clk) ack <= req;
+    always @(posedge clk) assert(ack & test);
+endmodule
+EOT
+prep -top top
+async2sync
+dffunmap
+logger -expect error "Unsupported cell type .allconst..*" 1
+write_btor /dev/null
diff --git a/tests/various/btor_allseq.ys b/tests/various/btor_allseq.ys
new file mode 100644
index 000000000..15f86701f
--- /dev/null
+++ b/tests/various/btor_allseq.ys
@@ -0,0 +1,13 @@
+
+read_verilog -formal <<EOT
+module top (input clk, input req, output reg ack);
+	(* allseq *) reg test;
+    always @(posedge clk) ack <= req;
+    always @(posedge clk) assert(ack & test);
+endmodule
+EOT
+prep -top top
+async2sync
+dffunmap
+logger -expect error "Unsupported cell type .allseq..*" 1
+write_btor /dev/null
diff --git a/tests/various/check_cells_btor.ys b/tests/various/btor_check_cells.ys
similarity index 100%
rename from tests/various/check_cells_btor.ys
rename to tests/various/btor_check_cells.ys
diff --git a/tests/various/btor_equiv_cells.ys b/tests/various/btor_equiv_cells.ys
new file mode 100644
index 000000000..9d68c8737
--- /dev/null
+++ b/tests/various/btor_equiv_cells.ys
@@ -0,0 +1,26 @@
+read_verilog -formal <<EOT
+module gold (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+endmodule
+EOT
+prep -top gold
+async2sync
+dffunmap
+design -save gold
+
+read_verilog -formal <<EOT
+module gate (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+endmodule
+EOT
+prep -top gate
+async2sync
+dffunmap
+design -save gate
+
+design -copy-from gold -as gold gold
+design -copy-from gate -as gate gate
+
+equiv_make gold gate equiv
+logger -expect error "Unsupported cell type .equiv..*" 1
+write_btor /dev/null
diff --git a/tests/various/btor_fair_cells.ys b/tests/various/btor_fair_cells.ys
new file mode 100644
index 000000000..5933cc0e4
--- /dev/null
+++ b/tests/various/btor_fair_cells.ys
@@ -0,0 +1,11 @@
+read_verilog -formal <<EOT
+module top (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+    always @(posedge clk) assume property (s_eventually ack);
+endmodule
+EOT
+prep -top top
+async2sync
+dffunmap
+logger -expect error "Unsupported cell type .fair..*" 1
+write_btor /dev/null
diff --git a/tests/various/btor_live_cells.ys b/tests/various/btor_live_cells.ys
new file mode 100644
index 000000000..4995c9f98
--- /dev/null
+++ b/tests/various/btor_live_cells.ys
@@ -0,0 +1,11 @@
+read_verilog -formal <<EOT
+module top (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+    always @(posedge clk) assert property (s_eventually ack);
+endmodule
+EOT
+prep -top top
+async2sync
+dffunmap
+logger -expect error "Unsupported cell type .live..*" 1
+write_btor /dev/null
diff --git a/tests/various/check_cells_smt2.ys b/tests/various/smt2_check_cells.ys
similarity index 100%
rename from tests/various/check_cells_smt2.ys
rename to tests/various/smt2_check_cells.ys
diff --git a/tests/various/smt2_equiv_cells.ys b/tests/various/smt2_equiv_cells.ys
new file mode 100644
index 000000000..ba1a9d80d
--- /dev/null
+++ b/tests/various/smt2_equiv_cells.ys
@@ -0,0 +1,26 @@
+read_verilog -formal <<EOT
+module gold (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+endmodule
+EOT
+prep -top gold
+async2sync
+dffunmap
+design -save gold
+
+read_verilog -formal <<EOT
+module gate (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+endmodule
+EOT
+prep -top gate
+async2sync
+dffunmap
+design -save gate
+
+design -copy-from gold -as gold gold
+design -copy-from gate -as gate gate
+
+equiv_make gold gate equiv
+logger -expect error "Unsupported cell type .equiv..*" 1
+write_smt2 /dev/null
diff --git a/tests/various/smt2_fair_cells.ys b/tests/various/smt2_fair_cells.ys
new file mode 100644
index 000000000..e3ab29ed1
--- /dev/null
+++ b/tests/various/smt2_fair_cells.ys
@@ -0,0 +1,11 @@
+read_verilog -formal <<EOT
+module top (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+    always @(posedge clk) assume property (s_eventually ack);
+endmodule
+EOT
+prep -top top
+async2sync
+dffunmap
+logger -expect error "Unsupported cell type .fair..*" 1
+write_smt2 /dev/null
diff --git a/tests/various/smt2_live_cells.ys b/tests/various/smt2_live_cells.ys
new file mode 100644
index 000000000..0504a8b70
--- /dev/null
+++ b/tests/various/smt2_live_cells.ys
@@ -0,0 +1,11 @@
+read_verilog -formal <<EOT
+module top (input clk, input req, output reg ack);
+    always @(posedge clk) ack <= req;
+    always @(posedge clk) assert property (s_eventually ack);
+endmodule
+EOT
+prep -top top
+async2sync
+dffunmap
+logger -expect error "Unsupported cell type .live..*" 1
+write_smt2 /dev/null