Merge pull request #464 from diffblue/type_parameters1

SystemVerilog: type parameters
diffblue · Apr 30, 2024 · bf6629f · bf6629f
2 parents 68409ac + b741269
commit bf6629f
Show file tree

Hide file tree

Showing 5 changed files with 77 additions and 12 deletions.
diff --git a/regression/verilog/modules/type_parameters1.desc b/regression/verilog/modules/type_parameters1.desc
@@ -0,0 +1,9 @@
+CORE
+type_parameters1.sv
+--bound 0
+^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$
+^\[main\.property\.p2\] always 32 == 32: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/modules/type_parameters1.sv b/regression/verilog/modules/type_parameters1.sv
@@ -0,0 +1,9 @@
+module main;
+
+  parameter type T1 = bit;
+  localparam type T2 = bit [31:0];
+
+  p1: assert property ($bits(T1) == 1);
+  p2: assert property ($bits(T2) == 32);
+
+endmodule
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -1040,13 +1040,21 @@ local_parameter_declaration:
 		{ init($$, ID_local_parameter_decl);
 		  stack_expr($$).type() = std::move(stack_type($2));
 		  swapop($$, $3); }
+        | TOK_LOCALPARAM TOK_TYPE list_of_type_assignments
+		{ init($$, ID_local_parameter_decl);
+		  stack_expr($$).type() = typet(ID_type);
+		  swapop($$, $3); }
 	;
 
 parameter_declaration:
           TOK_PARAMETER data_type_or_implicit list_of_param_assignments
 		{ init($$, ID_parameter_decl);
 		  stack_expr($$).type() = std::move(stack_type($2));
 		  swapop($$, $3); }
+        | TOK_PARAMETER TOK_TYPE list_of_type_assignments
+		{ init($$, ID_parameter_decl);
+		  stack_expr($$).type() = typet(ID_type);
+		  swapop($$, $3); }
 	;
 
 specparam_declaration:
@@ -1585,6 +1593,21 @@ param_assignment: param_identifier '=' constant_param_expression
 		  addswap($$, ID_value, $3); }
         ;
 
+list_of_type_assignments:
+	  type_assignment
+		{ init($$); mto($$, $1); }
+	| list_of_type_assignments ',' type_assignment
+		{ $$=$1;    mto($$, $3); }
+	;
+
+type_assignment: param_identifier '=' data_type
+		{ init($$, ID_parameter);
+		  auto base_name = stack_expr($1).id();
+		  stack_expr($$).set(ID_identifier, base_name);
+		  stack_expr($$).set(ID_base_name, base_name);
+		  addswap($$, ID_type, $3); }
+        ;
+
 data_type_or_implicit:
            data_type
         |  implicit_data_type

diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp
@@ -75,22 +75,42 @@ void verilog_typecheckt::collect_symbols(
 
   auto full_identifier = hierarchical_identifier(base_name);
 
-  // If there's no type, parameters take the type of the
-  // value. We signal this using the special type "derive_from_value".
+  // Is this a type or a value parameter?
+  if(type.id() == ID_type)
+  {
+    // much like a typedef
+    auto symbol_type = to_be_elaborated_typet{declarator.type()};
 
-  auto symbol_type =
-    to_be_elaborated_typet(type.is_nil() ? derive_from_value_typet() : type);
+    type_symbolt symbol{full_identifier, symbol_type, mode};
 
-  symbolt symbol{full_identifier, symbol_type, mode};
+    symbol.module = module_identifier;
+    symbol.base_name = base_name;
+    symbol.pretty_name = strip_verilog_prefix(symbol.name);
+    symbol.is_macro = true;
+    symbol.value = nil_exprt{};
+    symbol.location = declarator.source_location();
+
+    add_symbol(std::move(symbol));
+  }
+  else // It's a value parameter.
+  {
+    // If there's no type, parameters take the type of the
+    // value. We signal this using the special type "derive_from_value".
 
-  symbol.module = module_identifier;
-  symbol.base_name = base_name;
-  symbol.pretty_name = strip_verilog_prefix(symbol.name);
-  symbol.is_macro = true;
-  symbol.value = declarator.value();
-  symbol.location = declarator.source_location();
+    auto symbol_type =
+      to_be_elaborated_typet(type.is_nil() ? derive_from_value_typet() : type);
 
-  add_symbol(std::move(symbol));
+    symbolt symbol{full_identifier, symbol_type, mode};
+
+    symbol.module = module_identifier;
+    symbol.base_name = base_name;
+    symbol.pretty_name = strip_verilog_prefix(symbol.name);
+    symbol.is_macro = true;
+    symbol.value = declarator.value();
+    symbol.location = declarator.source_location();
+
+    add_symbol(std::move(symbol));
+  }
 }
 
 void verilog_typecheckt::collect_symbols(const typet &type)

diff --git a/src/verilog/verilog_typecheck_type.cpp b/src/verilog/verilog_typecheck_type.cpp
@@ -292,6 +292,10 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     return struct_union_typet{src.id(), std::move(components)}
       .with_source_location(src.source_location());
   }
+  else if(src.id() == ID_type)
+  {
+    return src;
+  }
   else
   {
     throw errort().with_location(source_location)