From 3d4fa8389e4137e1ca89e06957995442fc90e82e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 13 Nov 2025 13:06:39 -0800 Subject: [PATCH] Verilog: add type parameters to scope Type parameters are now added to the scope, and hence usable as types. --- CHANGELOG | 1 + regression/verilog/modules/type_parameters1.desc | 4 ++-- regression/verilog/modules/type_parameters2.desc | 7 +++++++ regression/verilog/modules/type_parameters2.sv | 9 +++++++++ src/verilog/parser.y | 6 +++++- 5 files changed, 24 insertions(+), 3 deletions(-) create mode 100644 regression/verilog/modules/type_parameters2.desc create mode 100644 regression/verilog/modules/type_parameters2.sv diff --git a/CHANGELOG b/CHANGELOG index 5c276f5ea..cd8ae1f17 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,5 +1,6 @@ # EBMC 5.9 +* SystemVerilog: fix for type parameters * SMV: word constants * SMV: IVAR declarations * SMV: bit selection operator diff --git a/regression/verilog/modules/type_parameters1.desc b/regression/verilog/modules/type_parameters1.desc index c68a2b87d..f27f5d4ec 100644 --- a/regression/verilog/modules/type_parameters1.desc +++ b/regression/verilog/modules/type_parameters1.desc @@ -1,8 +1,8 @@ CORE type_parameters1.sv -^\[main\.p1\] always \$bits\(main\.T1\) == 1: PROVED .*$ -^\[main\.p2\] always \$bits\(main\.T2\) == 32: PROVED .*$ +^\[main\.p1\] always \$bits\(bool\) == 1: PROVED .*$ +^\[main\.p2\] always \$bits\(\[31:0\]\) == 32: PROVED .*$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/type_parameters2.desc b/regression/verilog/modules/type_parameters2.desc new file mode 100644 index 000000000..cc2f80d27 --- /dev/null +++ b/regression/verilog/modules/type_parameters2.desc @@ -0,0 +1,7 @@ +CORE +type_parameters2.sv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/modules/type_parameters2.sv b/regression/verilog/modules/type_parameters2.sv new file mode 100644 index 000000000..7f93bff37 --- /dev/null +++ b/regression/verilog/modules/type_parameters2.sv @@ -0,0 +1,9 @@ +module main; + + parameter type T1 = bit [31:0]; + + T1 some_data; + + initial assert ($bits(some_data) == 32); + +endmodule diff --git a/src/verilog/parser.y b/src/verilog/parser.y index f5b2c444d..b41147b70 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2031,7 +2031,11 @@ type_assignment: param_identifier '=' data_type 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); } + addswap($$, ID_type, $3); + + // add to the scope as a type name + PARSER.scopes.add_name(base_name, "", verilog_scopet::TYPEDEF); + } ; data_type_or_implicit: