f4pga-arch-defs
f4pga-arch-defs copied to clipboard
Wrong synthesis result when `signed` signal is used for bit indexing
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
Unfortunately, fasm2bels
fails on the resulting .fasm
file, as reported here.
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 :)
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.
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.
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?
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?
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).
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.