diff --git a/regression/verilog/property/named_property3.desc b/regression/verilog/property/named_property3.desc new file mode 100644 index 000000000..de8fdbf2e --- /dev/null +++ b/regression/verilog/property/named_property3.desc @@ -0,0 +1,8 @@ +CORE +named_property3.sv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/property/named_property3.sv b/regression/verilog/property/named_property3.sv new file mode 100644 index 000000000..384172f38 --- /dev/null +++ b/regression/verilog/property/named_property3.sv @@ -0,0 +1,12 @@ +module main; + + wire [31:0] x = 'b10010001; + + property with_index; + // the index expression requires lowering + x[7:4] == 'b1001 + endproperty + + assert property (with_index); + +endmodule 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 {