Merge pull request #6164 from YosysHQ/nick/fix-6151

Adding error cases to formal backends for invalid formal cells

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());

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)))
 			{

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

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

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

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

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

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

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

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