From 70a5e887d99576dc990c7ced8386a05ebfdf8aff Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 21 Nov 2025 09:32:33 -0800 Subject: [PATCH] Verilog: type of parameter ports The type checker now applies the type given for a parameter port. --- CHANGELOG | 1 + regression/verilog/modules/parameter_ports5.desc | 5 ++--- src/verilog/verilog_elaborate.cpp | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index cd8ae1f17..7d05720c2 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,5 +1,6 @@ # EBMC 5.9 +* Verilog: fix for typed parameter ports * SystemVerilog: fix for type parameters * SMV: word constants * SMV: IVAR declarations diff --git a/regression/verilog/modules/parameter_ports5.desc b/regression/verilog/modules/parameter_ports5.desc index 645cd370c..3775ae6ba 100644 --- a/regression/verilog/modules/parameter_ports5.desc +++ b/regression/verilog/modules/parameter_ports5.desc @@ -1,7 +1,6 @@ -KNOWNBUG -parameter_ports5.v +CORE +parameter_ports5.sv ^EXIT=0$ ^SIGNAL=0$ -- -The type of the parameter is ignored. diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index bf3b9bf37..9c22bf2b8 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -989,7 +989,7 @@ verilog_typecheckt::elaborate(const verilog_module_sourcet &module_source) // At the top level of the module, include the parameter ports. for(auto &declaration : module_source.parameter_port_decls()) for(auto &declarator : declaration.declarators()) - collect_symbols(typet(ID_nil), declarator); + collect_symbols(declaration.type(), declarator); // At the top level of the module, include the non-parameter module port // module items.