diff --git a/regression/verilog/modules/type_parameters1.desc b/regression/verilog/modules/type_parameters1.desc new file mode 100644 index 000000000..2fd0d7490 --- /dev/null +++ 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 new file mode 100644 index 000000000..ac179c9ef --- /dev/null +++ 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 index d7fdc63ce..b7a2a75b2 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1040,6 +1040,10 @@ 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: @@ -1047,6 +1051,10 @@ parameter_declaration: { 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: @@ -1572,6 +1580,13 @@ list_of_param_assignments: { $$=$1; mto($$, $3); } ; +list_of_type_assignments: + type_assignment + { init($$); mto($$, $1); } + | list_of_type_assignments ',' type_assignment + { $$=$1; mto($$, $3); } + ; + param_assignment: param_identifier '=' const_expression { init($$, ID_parameter); auto base_name = stack_expr($1).id(); @@ -1580,6 +1595,14 @@ param_assignment: param_identifier '=' const_expression addswap($$, ID_value, $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 index 73a0259f8..35bcaf7a2 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -75,22 +75,43 @@ 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); + 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.is_type = 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 index b5db46e1d..aba11cd3f 100644 --- 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)