Verilog: grammar for unique case and unique if

This adds the Verilog grammar rules for unique case and unique if.

Author: kroening

regression/verilog/case/unique_case1.desc

@@ -0,0 +1,8 @@
+CORE
+unique_case1.sv
+
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

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

regression/verilog/if/unique_if1.desc

@@ -0,0 +1,8 @@
+CORE
+unique_if1.sv
+
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

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

src/hw_cbmc_irep_ids.h

@@ -37,6 +37,9 @@ IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
 IREP_ID_ONE(verilog_explicit_cast)
 IREP_ID_ONE(verilog_implicit_typecast)
+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)

src/verilog/parser.y

@@ -2785,27 +2785,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)); }
 	;