From 0b3de4e373d24d8d691a78b7c3077102c56b258d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 29 Jul 2025 16:16:00 -0700 Subject: [PATCH 1/2] KNOWNBUG test for named property --- regression/verilog/property/named_property3.desc | 9 +++++++++ regression/verilog/property/named_property3.sv | 11 +++++++++++ 2 files changed, 20 insertions(+) create mode 100644 regression/verilog/property/named_property3.desc create mode 100644 regression/verilog/property/named_property3.sv diff --git a/regression/verilog/property/named_property3.desc b/regression/verilog/property/named_property3.desc new file mode 100644 index 000000000..4689e950b --- /dev/null +++ b/regression/verilog/property/named_property3.desc @@ -0,0 +1,9 @@ +KNOWNBUG +named_property3.sv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +The expression in the named property is not lowered. diff --git a/regression/verilog/property/named_property3.sv b/regression/verilog/property/named_property3.sv new file mode 100644 index 000000000..d22d4437b --- /dev/null +++ b/regression/verilog/property/named_property3.sv @@ -0,0 +1,11 @@ +module main; + + wire [31:0] x = 'b10010001; + + property with_index; + x[7:4] == 'b1001 + endproperty + + assert property (with_index); + +endmodule From 98249d4d9d4aadefe0ee13ca68df977dbf19b202 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 29 Jul 2025 17:06:30 -0700 Subject: [PATCH 2/2] Fix for lowering for expressions given as named properties This adds the missing lowering for expressions given as named properties. --- regression/verilog/property/named_property3.desc | 3 +-- regression/verilog/property/named_property3.sv | 1 + src/verilog/verilog_synthesis.cpp | 5 ++++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/regression/verilog/property/named_property3.desc b/regression/verilog/property/named_property3.desc index 4689e950b..de8fdbf2e 100644 --- a/regression/verilog/property/named_property3.desc +++ b/regression/verilog/property/named_property3.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE named_property3.sv ^EXIT=0$ @@ -6,4 +6,3 @@ named_property3.sv -- ^warning: ignoring -- -The expression in the named property is not lowered. diff --git a/regression/verilog/property/named_property3.sv b/regression/verilog/property/named_property3.sv index d22d4437b..384172f38 100644 --- a/regression/verilog/property/named_property3.sv +++ b/regression/verilog/property/named_property3.sv @@ -3,6 +3,7 @@ module main; wire [31:0] x = 'b10010001; property with_index; + // the index expression requires lowering x[7:4] == 'b1001 endproperty diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 5eaf9e5cf..eec00e874 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -90,8 +90,11 @@ exprt verilog_synthesist::synth_expr_rec(exprt expr, symbol_statet symbol_state) // substitute assert(symbol.value.is_not_nil()); + // These aren't lowered yet + auto lowered = verilog_lowering(symbol.value); + // recursive call - return synth_expr_rec(symbol.value, symbol_state); + return synth_expr_rec(lowered, symbol_state); } else {