Tranlation of foreach from Sail to SystemVerilog failing.

[yutakang]

Hi there,

I've identified an issue related to the Sail-to-SystemVerilog translator. The problem arises when translating Sail code that involves the foreach construct.
Simply put, I suspect that the translation of the foreach construct in Sail to if… then… else… in SystemVerilog is not working as expected.
To illustrate this, let's consider the HighestSetBit as an example.

$include <prelude.sail>

val execute : forall 'N, 'N >= 0. bits('N) -> int

function execute x = {
    foreach (i from ('N - 1) to 0 by 1 in dec) {
        if [x[i]] == 0b1 then {
            return(i)
        };
        ()
    };
    return(negate(1))
}

Note that I changed the function name from HighestSetBit to execute to trigger the translator.

  function automatic logic [127:0] execute(sail_bits x);
        logic [127:0] sail_return;
        bit goto_for_start_1 = 1'h0;
        bit goto_then_9 = 1'h0;
        bit goto_endif_10 = 1'h0;
        bit goto_for_end_2 = 1'h0;
        bit goto_end_function_3 = 1'h0;
        logic [63:0] zz42;
        logic [127:0] zz415;
        logic [63:0] zz43;
        logic [63:0] zz44;
        logic [63:0] zz46;
        sail_unit zz47;
        bit zz48;
        logic [0:0] zz411;
        logic zz412;
        logic [127:0] zz414;
        logic [0:0] zz413;
        sail_unit zz49;
        logic [127:0] zz410;
        sail_unit zz45;
        logic [1:0] zz40;
        logic [127:0] zz41;
        zz415 = {120'h000000000000000000000000000000, x.size};
        zz42 = {zz415[64:0] - 65'b00000000000000000000000000000000000000000000000000000000000000001}[63:0];
        zz43 = 64'h0000000000000000;
        zz44 = 64'h0000000000000001;
        zz46 = zz42;
        /* for_start_1 */
        if (signed'(zz46) < signed'(zz43)) begin
            goto_for_end_2 = 1'h1;
        end else begin
            goto_for_end_2 = 1'h0;
        end;
        if (!goto_for_end_2) begin
            zz414 = unsigned'(128'(signed'({zz46})));
            zz412 = sail_vector_access_inc(x, zz414);
            zz413 = 1'b0;
            zz413 = zz412;
            zz411 = zz413;
            zz48 = zz411 == 1'b1;
        end;
        if (!goto_for_end_2) begin
            if (zz48) begin
                goto_then_9 = 1'h1;
            end else begin
                goto_then_9 = 1'h0;
            end;
        end;
        if (!(goto_for_end_2 || goto_then_9)) begin
            zz49 = SAIL_UNIT;
        end;
        if (!(goto_for_end_2 || goto_then_9)) begin
            goto_endif_10 = 1'h1;
        end;

        /* then_9 */
        if (!(goto_endif_10 || goto_for_end_2)) begin
            zz410 = unsigned'(128'(signed'({zz46})));
            sail_return = zz410;
        end;
        if (!(goto_endif_10 || goto_for_end_2)) begin
            goto_end_function_3 = 1'h1;
        end;
        /* endif_10 */
        if (!(goto_end_function_3 || goto_for_end_2)) begin
            zz47 = SAIL_UNIT;
            zz46 = zz46 - zz44;
        end;
        if (!(goto_end_function_3 || goto_for_end_2)) begin
            goto_for_start_1 = 1'h1;
        end;
        /* for_end_2 */
        if (!(goto_end_function_3 || goto_for_start_1)) begin
            zz45 = SAIL_UNIT;
            zz40 = 2'b10 + 2'b01;
            zz41 = (~128'h00000000000000000000000000000001) + 128'h00000000000000000000000000000001;
            sail_return = zz41;
        end;
        /* end_function_3 */
        if (!goto_for_start_1) begin
            return sail_return;
        end;
    endfunction

Even though one can sometimes emulate for-loops using if-then-else constructs and by exploiting SystemVerilog’s intrinsic parallelism, it seems that this translation is not working as expected.

The problem becomes evident in the above example where the if-then-else constructs used to emulate for-loops are located inside a function in SystemVerilog. However, SystemVerilog’s atomic execution model for functions does not allow us to effectively exploit intrinsic parallelism to emulate for-loops.

Furthermore, it seems that we also need to use always constructs to introduce procedural blocks effectively.
As a new user of Sail and SystemVerilog, it appears to me that translating foreach in Sail to for in SystemVerilog is a more straightforward approach.

Are there reasons for using if-then-else constructs to emulate for-loops?

[Timmmm]

See #436. IIRC Alasdair said it simply hasn't been implemented yet. I may have imagined that though.

[yutakang]

Thanks, @Timmmm. I will leave this issue here, as it explains why the current translation of foreach from Sail to SystemVerilog does not work as intended, using a concrete example.

This might be useful for someone at the University of Cambridge who will address this issue.