Foreach with multiple loop variables doesn't emit skipped indexes

[mglb]

Skipped indexes are missing in VPI AST. According to [1] skipped index variable should be represented as vpiOperation with vpiOpType = vpiNullOp. [1]: IEEE Std 1800-2021 "IEEE Standard for SystemVerilog", 37 VPI object model diagrams, 37.73. Do-while, foreach, Detail 2.

Example (https://github.com/zachjs/sv2v/blob/master/test/core/foreach.sv):

module top;
    logic [1:0] foo [4] = {2'b10,2'b01,2'b11,2'b00};
    initial
        foreach (foo [ x ])
            $display(x, foo[x]);

    // from the SystemVerilog-2017 specification
    int A [2][3][4];
    bit [3:0][2:1] B [5:1][4];
    initial begin
        A = 0;
        B = 0;
        foreach( A [ i, j, k ] )
            $display(i, j, k);
        foreach( B [ q, r, , s ] )
            $display(q, r, s);
    end
endmodule

VPI AST fragment for the foreach over B:

\_foreach_stmt: (work@top), line:15:9, endln:15:16
  |vpiParent:
  \_begin: (work@top), line:10:13, endln:17:8
  |vpiFullName:work@top
  |vpiVariables:
  \_ref_var: (work@top.B), line:15:18, endln:15:19
    |vpiParent:
    \_foreach_stmt: (work@top), line:15:9, endln:15:16
    |vpiTypespec:
    \_array_typespec:
    |vpiName:B
    |vpiFullName:work@top.B
  |vpiLoopVars:
  \_bit_var: (q), line:15:22, endln:15:23
    |vpiTypespec:
    \_bit_typespec: , line:9:5, endln:9:19
      |vpiRange:
      ...
    |vpiName:q
  |vpiLoopVars:
  \_bit_var: (r), line:15:25, endln:15:26
    |vpiTypespec:
    \_bit_typespec: , line:9:5, endln:9:19
      |vpiRange:
      \_range: , line:9:9, endln:9:14
      ...
    |vpiName:r
  ╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴┨ Missing vpiOperation
  |vpiLoopVars:
  \_bit_var: (s), line:15:30, endln:15:31
    |vpiTypespec:
    \_bit_typespec: , line:9:5, endln:9:19
      |vpiRange:
      ...
    |vpiName:s
...

[alaindargelas]

Please provide a synthesizable example we can formally verify

[mglb]

This one should be syntesizable:

module top(input clk);
    bit [1:0][3:0] B [3:0][2];
    always @(posedge clk) begin
        foreach(B[q, r, , s]) begin
            B[q][r][0][s] = r;
            B[q][r][1][s] = 0;
        end
    end
endmodule

Relevant fragments of UHDM tree (command: surelog -parse -d uhdm):

...
|vpiStmt:
\_foreach_stmt: (work@top), line:4:9, endln:4:16
  |vpiParent:
  \_begin: (work@top), line:3:27, endln:8:8
  |vpiFullName:work@top
  |vpiVariables:
  \_ref_var: (work@top.B), line:4:17, endln:4:18
    |vpiParent:
    \_foreach_stmt: (work@top), line:4:9, endln:4:16
    |vpiTypespec:
    \_array_typespec:
    |vpiName:B
    |vpiFullName:work@top.B
  |vpiLoopVars:
  \_bit_var: (q), line:4:19, endln:4:20
    |vpiTypespec:
    \_bit_typespec: , line:2:5, endln:2:19
      |vpiRange:
      \_range: , line:2:9, endln:2:14
        |vpiLeftRange:
        \_constant: , line:2:10, endln:2:11
          |vpiParent:
          \_range: , line:2:9, endln:2:14
          |vpiDecompile:1
          |vpiSize:64
          |UINT:1
          |vpiConstType:9
        |vpiRightRange:
        \_constant: , line:2:12, endln:2:13
          |vpiParent:
          \_range: , line:2:9, endln:2:14
          |vpiDecompile:0
          |vpiSize:64
          |UINT:0
          |vpiConstType:9
      |vpiRange:
      \_range: , line:2:14, endln:2:19
        |vpiLeftRange:
        \_constant: , line:2:15, endln:2:16
          |vpiParent:
          \_range: , line:2:14, endln:2:19
          |vpiDecompile:3
          |vpiSize:64
          |UINT:3
          |vpiConstType:9
        |vpiRightRange:
        \_constant: , line:2:17, endln:2:18
          |vpiParent:
          \_range: , line:2:14, endln:2:19
          |vpiDecompile:0
          |vpiSize:64
          |UINT:0
          |vpiConstType:9
    |vpiName:q
  |vpiLoopVars:
  \_bit_var: (r), line:4:22, endln:4:23
    |vpiTypespec:
    \_bit_typespec: , line:2:5, endln:2:19
      |vpiRange:
      ...
    |vpiName:r
  ╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴╴┨ Missing vpiLoopVars/vpiOperation
  |vpiLoopVars:
  \_bit_var: (s), line:4:27, endln:4:28
    |vpiTypespec:
    \_bit_typespec: , line:2:5, endln:2:19
      |vpiRange:
      ...
    |vpiName:s
  |vpiStmt:
  ...

[alaindargelas]

By synthesizable, I also mean that we can observe in the synthesis output if we are dealing with the design correctly end-to-end. The example you provided is not Observable, there is no output, the Synthesis optimizes everything out so no matter how badly we model the design the formal verification or simulation will say "Good job". We need to create designs that are synthesizable and observable. So we don't have false negatives.

The modified design below fits the description above:

module top(input clk, output bit [1:0][3:0] B [3:0][2]);
    always @(posedge clk) begin
        foreach(B[q, r, , s]) begin
            B[q][r][0][s] = r;
            B[q][r][1][s] = 0;
        end
    end
endmodule

That design will generate a netlist that can be simulated of run through formal verification.

[alaindargelas]

Fixed by #3241.

@mglb, please add this testcase to https://github.com/chipsalliance/UHDM-integration-tests/tree/8dc491bb51384418a41a7d2f9c30ac8e576f4619/tests

and make sure we reach formal equivalence with Yosys parser.

module top(input clk, output bit [1:0][3:0] B [3:0][2]);
    always @(posedge clk) begin
        foreach(B[q, r, , s]) begin
            B[q][r][0][s] = r;
            B[q][r][1][s] = 0;
        end
    end
endmodule