Merge pull request #446 from diffblue/unique_case1

Verilog: grammar for `unique case` and `unique if`
diffblue · Apr 23, 2024 · 6e0ac27 · 6e0ac27
2 parents 1abd38e + 87c8f5a
commit 6e0ac27
Show file tree

Hide file tree

Showing 6 changed files with 73 additions and 13 deletions.
diff --git a/regression/verilog/case/unique_case1.desc 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
@@ -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
@@ -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
@@ -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
@@ -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)

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -2845,27 +2845,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)); }
 	;