loop_generate_construct not supported

[zputrle]

Just to confirm. As far as I can see, the loop_generate_construct (or generate_for) is not supported by EBMC. List [1] indicates that it is (section 27.4).

For example, if I pass the following module to EBMC by using ebmc test_generate_for.v --systemverilog --top test_generate_for --bound 10

module test_generate_for
(
    input   [32-1 : 0] vec_i ,
    output  [32-1 : 0] vec_o
);

genvar i ;
for (i = 0; i < 32; i = i + 1) begin
    assign vec_o[i] = vec_i[i];
end

endmodule

I get the following output

Parsing examples/test_generate_for.v
Converting
Type-checking Verilog::test_generate_for
--- begin invariant violation report ---
Invariant check failed
File: verilog_interfaces.cpp:310 function: interface_module_item
Condition: false
Reason: unexpected module item: generate_for
Backtrace:
[0x53a0c2]
[0x53ae3d]
[0x485592]
[0x7d0eab]
[0x78da13]
[0x8283c2]
[0x78e794]
[0x7551a2]
[0x61be54]
[0x61caaf]
[0x4dd131]
[0x4df1f0]
[0x4a2494]
[0x477c7f]
[0x475e09]
[0x8ee94a]
[0x8f01e7]
[0x4804f5]


--- end invariant violation report ---
./run_test_generate_for.sh: line 7: 12862 Aborted                 (core dumped) ebmc examples/test_generate_for.v --systemverilog --top test_generate_for --bound 10

When checking the convert_module_item function in src/verilog/verilog_typecheck.cpp, which I'm assuming that raises the exception that causes unexpected module item: generate_for to print, there is no ID_generate_for case to handle the generate_for.

Also, for some reason, it seems that EBMC core dumps at the end.

I'm using the latest release (ebmc-5.1).

[1] https://www.cprover.org/ebmc/manual/verilog_language_features/

[kroening]

This will work if you put generate ... endgenerate around the loop.

These became optional with 1364-2005; will fix.

[kroening]

I would be grateful if you could confirm the fix.

[zputrle]

Thank you for the info and for the fast response.

[zputrle]

I confirm that the fix resolves the problem.