Assignment to struct fields in different blocks are not supported

[bbawj]

From the latest main:

6.0 (ebmc-6.0-227-gb11cd715)

Here is a minimal example

typedef struct {
  logic field1;
  logic field2;
} structure_t;

module debug (
    input wire clk,
    input wire rst
);
  structure_t s;
  always @(posedge clk) begin
    s.field1 <= 0;
  end
  always @(posedge clk) begin
    s.field2 <= 0;
  end

  initial assert (s.field1 == 0);
endmodule

Output:

EBMC version 6.10.0 (7483d0de) 64-bit x86_64 linux
Converting
Type-checking Verilog::debug
Synthesis Verilog::debug
file debug.sv line 15: conflict with previous assignment
CONVERSION ERROR

If i change the assert to the following property instead:

 property p;
    @(posedge clk) rst |=> ##1 s.field2 == 0;
  endproperty
  assert property (p);

Output:

EBMC version 6.10.0 (7483d0de) 64-bit x86_64 linux
Converting
Type-checking Verilog::debug
file debug.sv line 19: unknown identifier field1
CONVERSION ERROR

[kroening]

The first example (fields of a struct assigned in different always constructs) is fixed by #2119, which replaces synthesis by a conversion from the RTL representation (#2117); the fields are disjoint slices there. A regression test is included.

The second example fails during type checking (unknown identifier field2 when the field is referenced inside a named property declaration), independently of synthesis, and remains open.

[kroening]

The second example is fixed by #2121: the member select in a named property declaration is no longer resolved when the declaration is converted, but once the type of the lhs of the . is known.