Verilog: strong typing for enums

The SystemVerilog 1800-2017 standard requires that enums are strongly typed,
i.e., that automatic conversion to an enum type is prohibited.

Author: kroening

regression/verilog/data-types/enum2.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 enum2.sv
 
-^EXIT=10$
+^file .* line 4: assignment to enum requires enum of the same type$
+^EXIT=2$
 ^SIGNAL=0$
 --
---
-enum constants must be strongly typed.

regression/verilog/data-types/enum4.desc

@@ -1,9 +1,7 @@
-KNOWNBUG
+CORE
 enum4.sv
 --bound 0
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.p1\] always main\.my_light != 0 \+ 1 \+ 1 \+ 1: PROVED up to bound 0$
+^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$
 --
---
-Type conversion not working

regression/verilog/data-types/enum_base_type1.desc

@@ -0,0 +1,7 @@
+CORE
+enum_base_type1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[.*\] always 8 == 8: PROVED up to bound 0$
+--

regression/verilog/data-types/enum_base_type1.sv

@@ -0,0 +1,8 @@
+module main;
+
+  typedef enum bit [7:0] { A } enum_t;
+
+  // expected to pass
+  p1: assert property ($bits(A) == 8);
+
+endmodule

regression/verilog/data-types/enum_cast1.desc

@@ -0,0 +1,8 @@
+CORE
+enum_cast1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$
+^\[main\.property\.p2\] always 2 == 2: PROVED up to bound 0$
+--

regression/verilog/data-types/enum_cast1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  typedef enum { A = 1, B = 2 } enum_t;
+
+  // expected to pass
+  p1: assert property (A == enum_t'(1));
+  p2: assert property (B == enum_t'(2));
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -106,6 +106,7 @@ IREP_ID_ONE(uwire)
 IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
 IREP_ID_ONE(verilog_enum)
+IREP_ID_TWO(C_verilog_type, #verilog_type)
 IREP_ID_ONE(verilog_type_reference)
 IREP_ID_ONE(enum_names)
 IREP_ID_ONE(var)

src/verilog/parser.y

@@ -1253,6 +1253,11 @@ data_type:
 	          init($$, ID_verilog_enum);
 	          stack_type($$).add_subtype() = std::move(stack_type($2));
 	          stack_type($$).set(ID_enum_names, stack_type($4));
+
+	          // We attach a dummy id to distinguish two syntactically
+	          // identical enum types.
+	          auto id = PARSER.current_scope->prefix + "enum-" + PARSER.get_next_id();
+	          stack_expr($$).set(ID_identifier, id);
 	        }
 	| TOK_STRING
 	        { init($$, ID_string); }
@@ -1328,7 +1333,9 @@ enum_base_type_opt:
 		{ init($$, ID_nil); }
 	| integer_atom_type signing_opt
 	| integer_vector_type signing_opt packed_dimension_opt
+		{ $$ = $3; add_as_subtype(stack_type($$), stack_type($1)); }
 	| type_identifier packed_dimension_opt
+		{ $$ = $2; add_as_subtype(stack_type($$), stack_type($1)); }
 	;
 
 non_integer_type:
@@ -2125,7 +2132,7 @@ gate_instance:
 
 name_of_gate_instance_opt:
 	  /* Optional */ 
-	        { init($$, "$_&#ANON" + PARSER.get_dummy_id()); }
+	        { init($$, "$_&#ANON" + PARSER.get_next_id()); }
 	| name_of_gate_instance
 	;
 
@@ -2192,7 +2199,7 @@ module_instance:
 	;
 
 name_of_instance:
-	  { init($$, "$_&#ANON" + PARSER.get_dummy_id());}
+	  { init($$, "$_&#ANON" + PARSER.get_next_id());}
 	| TOK_NON_TYPE_IDENTIFIER
 	;
 

src/verilog/verilog_elaborate.cpp

@@ -102,9 +102,8 @@ void verilog_typecheckt::collect_symbols(const typet &type)
     if(enum_type.has_base_type())
       collect_symbols(enum_type.base_type());
 
-    // The default base type is 'int'.
-    auto base_type =
-      enum_type.has_base_type() ? enum_type.base_type() : signedbv_typet(32);
+    // convert the type now
+    auto converted_type = convert_type(enum_type);
 
     // Add the enum names to the symbol table for subsequent elaboration.
     // Values are given, or the previous plus one, starting with value '0'.
@@ -113,13 +112,17 @@ void verilog_typecheckt::collect_symbols(const typet &type)
     for(auto &enum_name : enum_type.enum_names())
     {
       if(enum_name.value().is_not_nil())
-        initializer = enum_name.value();
+      {
+        exprt tmp = enum_name.value();
+        convert_expr(tmp);
+        initializer = std::move(tmp);
+      }
 
-      exprt value = typecast_exprt(initializer, base_type);
+      exprt value = typecast_exprt(initializer, converted_type);
 
       const auto base_name = enum_name.base_name();
       const auto identifier = hierarchical_identifier(base_name);
-      symbolt enum_name_symbol(identifier, base_type, mode);
+      symbolt enum_name_symbol(identifier, converted_type, mode);
       enum_name_symbol.module = module_identifier;
       enum_name_symbol.base_name = base_name;
       enum_name_symbol.value = std::move(value);
@@ -128,8 +131,8 @@ void verilog_typecheckt::collect_symbols(const typet &type)
       add_symbol(std::move(enum_name_symbol));
 
       initializer = plus_exprt(
-        typecast_exprt(initializer, base_type),
-        typecast_exprt(from_integer(1, integer_typet()), base_type));
+        typecast_exprt(initializer, converted_type),
+        typecast_exprt(from_integer(1, integer_typet()), converted_type));
     }
   }
 }

src/verilog/verilog_parser.h

@@ -46,7 +46,6 @@ class verilog_parsert:public parsert
 
   verilog_parsert():mode(VIS_VERILOG)
   {
-    dummy_id=0;
   }
 
   // parser scopes and identifiers
@@ -118,12 +117,14 @@ class verilog_parsert:public parsert
     return scope_ptr == nullptr ? false : scope_ptr->is_type;
   }
 
-  unsigned dummy_id;
+  // These are used for anonymous gate instances
+  // and to create a unique identifier for enum types.
+  std::size_t next_id_counter = 0;
 
-  std::string get_dummy_id()
+  std::string get_next_id()
   {
-    dummy_id++;
-    return integer2string(dummy_id-1);
+    next_id_counter++;
+    return integer2string(next_id_counter - 1);
   }
 };