From cf0e68b06cefb58241ad84ce7deb543f0f0deb93 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 6 Feb 2025 12:10:45 +0000 Subject: [PATCH] Verilog: KNOWNBUG for declarations inside a named block inside a function Replicates #966. --- regression/verilog/functioncall/named_block1.desc | 8 ++++++++ regression/verilog/functioncall/named_block1.sv | 13 +++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 regression/verilog/functioncall/named_block1.desc create mode 100644 regression/verilog/functioncall/named_block1.sv diff --git a/regression/verilog/functioncall/named_block1.desc b/regression/verilog/functioncall/named_block1.desc new file mode 100644 index 00000000..883cc6df --- /dev/null +++ b/regression/verilog/functioncall/named_block1.desc @@ -0,0 +1,8 @@ +KNOWNBUG +named_block1.sv + +^\[.*\] always main\.foo\(\) == 123: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/functioncall/named_block1.sv b/regression/verilog/functioncall/named_block1.sv new file mode 100644 index 00000000..c7eba52c --- /dev/null +++ b/regression/verilog/functioncall/named_block1.sv @@ -0,0 +1,13 @@ +module main; + + function [31:0] foo; + begin : block_name + reg [31:0] x; + x = 123; + foo = x; + end + endfunction; + + assert final (foo() == 123); + +endmodule