From d3ed44fb32f01831619ecac46661740a76be33c1 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 20 Apr 2024 15:22:02 -0700
Subject: [PATCH] Verilog: grammar for unique case and unique if

This adds the Verilog grammar rules for unique case and unique if.
---
 regression/verilog/case/unique_case1.desc |  8 +++++
 regression/verilog/case/unique_case1.sv   | 15 +++++++++
 regression/verilog/if/unique_if1.desc     |  8 +++++
 regression/verilog/if/unique_if1.sv       | 15 +++++++++
 src/hw_cbmc_irep_ids.h                    |  3 ++
 src/verilog/parser.y                      | 37 +++++++++++++++--------
 6 files changed, 73 insertions(+), 13 deletions(-)
 create mode 100644 regression/verilog/case/unique_case1.desc
 create mode 100644 regression/verilog/case/unique_case1.sv
 create mode 100644 regression/verilog/if/unique_if1.desc
 create mode 100644 regression/verilog/if/unique_if1.sv

diff --git a/regression/verilog/case/unique_case1.desc b/regression/verilog/case/unique_case1.desc
new file mode 100644
index 000000000..bf323b857
--- /dev/null
+++ b/regression/verilog/case/unique_case1.desc
@@ -0,0 +1,8 @@
+CORE
+unique_case1.sv
+
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/case/unique_case1.sv b/regression/verilog/case/unique_case1.sv
new file mode 100644
index 000000000..6421cc191
--- /dev/null
+++ b/regression/verilog/case/unique_case1.sv
@@ -0,0 +1,15 @@
+module main(input x);
+
+  always_comb // unique
+    unique casex (x)
+      0:;
+      1:;
+    endcase
+    
+  always_comb // not unique
+    unique casex (x)
+      0:;
+      'b1?:;
+    endcase
+    
+endmodule
diff --git a/regression/verilog/if/unique_if1.desc b/regression/verilog/if/unique_if1.desc
new file mode 100644
index 000000000..b0f43a2cd
--- /dev/null
+++ b/regression/verilog/if/unique_if1.desc
@@ -0,0 +1,8 @@
+CORE
+unique_if1.sv
+
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/if/unique_if1.sv b/regression/verilog/if/unique_if1.sv
new file mode 100644
index 000000000..ceb435f93
--- /dev/null
+++ b/regression/verilog/if/unique_if1.sv
@@ -0,0 +1,15 @@
+module main(input x);
+
+  always_comb // unique
+    unique if (x == 0)
+      ;
+    else if(x == 1)
+      ;
+    
+  always_comb // not unique
+    unique if (x == 0)
+      ;
+    else if(x&'b10 == 1)
+      ;
+    
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index f7a3ff5a6..71e914c03 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -35,6 +35,9 @@ IREP_ID_TWO(C_little_endian, #little_endian)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
+IREP_ID_ONE(verilog_unique)
+IREP_ID_ONE(verilog_unique0)
+IREP_ID_ONE(verilog_priority)
 IREP_ID_ONE(verilog_non_indexed_part_select)
 IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index cced4ddb1..519253a69 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -2755,27 +2755,38 @@ disable_statement: TOK_DISABLE hierarchical_task_or_block_identifier ';'
 // A.6.6 Conditional statements
 
 conditional_statement:
-	  TOK_IF '(' expression ')' statement_or_null %prec LT_TOK_ELSE
-		{ init($$, ID_if); mto($$, $3); mto($$, $5); }
-	| TOK_IF '(' expression ')' statement_or_null TOK_ELSE statement_or_null
-		{ init($$, ID_if); mto($$, $3); mto($$, $5); mto($$, $7); }
+	  unique_priority_opt TOK_IF '(' expression ')' statement_or_null %prec LT_TOK_ELSE
+		{ init($$, ID_if); mto($$, $4); mto($$, $6); }
+	| unique_priority_opt TOK_IF '(' expression ')' statement_or_null TOK_ELSE statement_or_null
+		{ init($$, ID_if); mto($$, $4); mto($$, $6); mto($$, $8); }
+	;
+
+unique_priority_opt:
+	  /* Optional */
+		{ init($$); }
+	| TOK_UNIQUE
+		{ init($$, ID_verilog_unique); }
+	| TOK_UNIQUE0
+		{ init($$, ID_verilog_unique0); }
+	| TOK_PRIORITY
+		{ init($$, ID_verilog_priority); }
 	;
 
 // System Verilog standard 1800-2017
 // A.6.7 Case statements
 
 case_statement:
-	  TOK_CASE '(' expression ')' case_item_brace TOK_ENDCASE
-		{ init($$, ID_case);  mto($$, $3);
-                  Forall_operands(it, stack_expr($5))
+	  unique_priority_opt TOK_CASE '(' expression ')' case_item_brace TOK_ENDCASE
+		{ init($$, ID_case);  mto($$, $4);
+                  Forall_operands(it, stack_expr($6))
                     stack_expr($$).add_to_operands(std::move(*it)); }
-	| TOK_CASEX '(' expression ')' case_item_brace TOK_ENDCASE
-		{ init($$, ID_casex); mto($$, $3);
-                  Forall_operands(it, stack_expr($5))
+	| unique_priority_opt TOK_CASEX '(' expression ')' case_item_brace TOK_ENDCASE
+		{ init($$, ID_casex); mto($$, $4);
+                  Forall_operands(it, stack_expr($6))
                     stack_expr($$).add_to_operands(std::move(*it)); }
-	| TOK_CASEZ '(' expression ')' case_item_brace TOK_ENDCASE
-		{ init($$, ID_casez); mto($$, $3);
-                  Forall_operands(it, stack_expr($5))
+	| unique_priority_opt TOK_CASEZ '(' expression ')' case_item_brace TOK_ENDCASE
+		{ init($$, ID_casez); mto($$, $4);
+                  Forall_operands(it, stack_expr($6))
                     stack_expr($$).add_to_operands(std::move(*it)); }
 	;