Wrong synthesis result when `signed` signal is used for bit indexing

[gergoerdi]

With the following Verilog input, targeting the Nexys A7-50T dev board with a xc7a50tcsg324-1 FPGA, the four LEDs should cycle between different single LED lighting up at roughly 1 Hz. With Vivado, the result is exactly that. With SymbiFlow, however, only the first LED is every on; so instead of cycling ooo*, oo*o, o*oo, *ooo, it cycles ooo*, oooo, oooo, oooo.

module Top(
           input        CLK100MHZ,
           output [3:0] LED
           );

   reg [26:0]           cnt = 0;
   reg [1:0]            i = 0;
   wire signed [3:0]   idx = $signed(i);
   reg [3:0]            result;

   always @(posedge CLK100MHZ) begin : cnt_register
      begin
         cnt <= cnt + 1;
      end
   end

   always @(posedge CLK100MHZ) begin : i_register
      if (cnt == 0) begin
         i <= i + 1;
      end
   end

   always @(*) begin
      result = 4'b0000;
      result[idx] = 1'b1;
   end

   assign LED = result;

endmodule

[gergoerdi]

Unfortunately, fasm2bels fails on the resulting .fasm file, as reported here.

[tcal-x]

Does it work if you change the assignment to

assign LED[3:0] = result[3:0];

?

I'm puzzled a little by the use of idx -- does it sequence through 0000, 0001, 1110, 1111 (after the sign extension from the 2-bit i)? This is hitting some Verilog situations I don't often see :)

[gergoerdi]

Yes, the example crucially depends on the convoluted way of one-hot-encoding i into result.

The code is simplified from Clash output. It could be that the Verilog is wonky, but then I'd need to be told that authoritatively.

[tcal-x]

I used an independent simulator, and the Verilog appears to be incorrect in terms of what you want it to do. This is what I get:

i: 00, 01, 10, 11, repeat idx: 0000, 0001, 1110, 1111, repeat result: 0001, 0010, 0000, 0000, repeat

If you completely eliminate 'idx', and replace result[idx] = 1'b1 with result[i] = 1'b1, then on the simulator it works as you expect ('result' getting 0001, 0010, 0100, 1000, repeat). I did not test that with Symbiflow.

I read one version of the spec where an invalid index into an array gives indeterminate results, so it is legal both for Vivado to give you the result you expected, and for SymbiFlow to give you something different.

[gergoerdi]

I'm not sure why idx goes from 0001 to 1110 instead of 0010, can you elaborate on that?

Nevertheless, I'm afraid I might have simplified the code beyond relevance, if the root cause turns out to be Clash mis-generating Verilog. The real code generated by Clash takes care to explicitly bit-extend i into idx as:

   wire signed [63:0]   idx = $signed({{(64-2) {1'b0}},i});

Can you say if that one still isn't correct, so that I can go back to Clash with it?

[tcal-x]

The 1110 and 1111 came from sign extension; but the actual code explicitly adds 0s, so that seems ok.

So we're back to another thing to check that I mentioned earlier --- if in the code that doesn't work, you replace assign LED = result; with assign LED[3:0] = result[3:0];, does it then work?

[mithro]

At a high level -- if the result works in Vivado, then it should probably also work in SymbiFlow. If Vivado's behaviour is different to the standard then we might be a "act in the same broken manner as vivado" type flag (for example LLVM has flags which make it match GCC's behaviour even when GCC's behaviour is non-spec compliant).

[tcal-x]

I reproduced the unexpected behavior in SymbiFlow even with the explicit zero-extension:

wire signed [3:0]    idx = {2'b00,i};

If I instead use the following, I see the expected behavior (sequencing through the 4 LEDs):

wire        [3:0]    idx = {2'b00,i};

This does seem to be a bug, in Yosys I suppose.