YosysHQ / yosys

Yosys Open SYnthesis Suite
https://yosyshq.net/yosys/
ISC License
3.52k stars 894 forks source link

opt pass is optimizing my code away #100

Closed dvc94ch closed 9 years ago

dvc94ch commented 9 years ago

Hi.

The latest yosys from git optimizes my fsm a little too much... :smile:

I'm a total beginner in Verilog so I'm not sure if it's just my code. I uploaded it to github https://github.com/dvc94ch/fsm-verilog/blob/master/fsm.v

Any help would be greatly appreciated.

Below is the output in .blif and the build script that causes it:

read_verilog fsm.v
show -pause
proc
show -pause
opt_clean
check
show -pause
opt
show -pause
# Generated by Yosys 0.5+385 (git sha1 ddf3e2d, clang 3.7.0 -march=x86-64 -mtune=generic -O2 -fstack-protector-strong -fPIC -Os)

.model fsm
.inputs clk a b c
.outputs k m l
.names $false
.names $true
1
.names $undef
.names $false k
1 1
.names $false l
1 1
.names $false m
1 1
.end
cliffordwolf commented 9 years ago

Woho! The 100th opened issue on github! ;)

Regarding your question: I think Yosys is correct to optimize the design away. Afaics, there is no way that either k, l, or m ever output "1", when the whole circuit starts initialized with "x"..

There are two problem with your code:

  1. You are writing to state from two different always blocks. This has undefined behavior in Verilog synthesis.
  2. You use STATE_ML to check if either state == STATE_M or state == STATE_L, but this is not what your code does! Your code actually means state == STATE_ML, and this is never the case. This problem should also have been evident in simulation. (You should always write test benches and simulate your code!)

Here is a corrected version of your verilog module:

module fsm (input clk, input a, b, c, output k, m, l);
  localparam
    STATE_IDLE = 3'b000,
    STATE_K = 3'b001,
    STATE_M = 3'b010,
    STATE_L = 3'b100;

  reg [2:0] state;

  always @(posedge clk) begin
    // next state
    case (state)
      STATE_IDLE: begin
        if (a && b) begin
          state <= STATE_ML;
        end else if (b) begin
          state <= STATE_K;
        end
      end
      STATE_M, STATE_L: begin
        if (a && b && c) begin
          state <= STATE_L;
        end else if (b && c) begin
          state <= STATE_M;
        end
      end
    endcase

    // reset
    if (!a && !b && !c)
      state <= STATE_IDLE;
  end

  // output logic
  assign k = state[0] & ~state[1] & ~state[2];
  assign m = ~state[0] & state[1] & ~state[2];
  assign l = ~state[0] & ~state[1] & state[2];
endmodule
dvc94ch commented 9 years ago

putting it all in a single always block fixed it!! I thought I read somewhere that that was good coding style to split your fsm into 2 or 3 always blocks.

I did write a testbench and it did not show the problem... https://github.com/dvc94ch/fsm-verilog/blob/master/testbench.v

Thank you!

On Fri, Nov 13, 2015 at 10:14 AM, Clifford Wolf notifications@github.com wrote:

Woho! The 100th opened issue on github! ;)

Regarding your question: I think Yosys is correct to optimize the design away. Afaics, there is no way that either k, l, or m ever output "1", when the whole circuit starts initialized with "x"..

There are two problem with your code:

1.

You are writing to state from two different always blocks. This has undefined behavior in Verilog synthesis. 2.

You use STATE_ML to check if either state == STATE_M or state == STATE_L, but this is not what your code does! Your code actually means state == STATE_ML, and this is never the case. This problem should also have been evident in simulation. (You should always write test benches and simulate your code!)

Here is a corrected version of your verilog module:

module fsm (input clk, input a, b, c, output k, m, l); localparam STATE_IDLE = 3'b000, STATE_K = 3'b001, STATE_M = 3'b010, STATE_L = 3'b100;

reg [2:0] state;

always @(posedge clk) begin // next state case (state) STATE_IDLE: begin if (a && b) begin state <= STATE_ML; end else if (b) begin state <= STATE_K; end end STATE_M, STATE_L: begin if (a && b && c) begin state <= STATE_L; end else if (b && c) begin state <= STATE_M; end end endcase

// reset
if (!a && !b && !c)
  state <= STATE_IDLE;

end

// output logic assign k = state[0] & ~state[1] & ~state[2]; assign m = ~state[0] & state[1] & ~state[2]; assign l = ~state[0] & ~state[1] & state[2]; endmodule

— Reply to this email directly or view it on GitHub https://github.com/cliffordwolf/yosys/issues/100#issuecomment-156371416.

cliffordwolf commented 9 years ago

I thought I read somewhere that that was good coding style to split your fsm into 2 or 3 always blocks.

Yes, but like this:       :)

reg [2:0] next_state;
reg [2:0] state;

always @* begin
    next_state = ...;
end

always @(posedge clk) begin
    state <= next_state;
end

Not by writing to the same signal from multiple blocks. That just has undefined behavior!

I did write a testbench and it did not show the problem...

It must show you that the STATE_ML thing is not working..

The other problem is tricky to spot in simulation, because in simulation the undefined part is simply in which order the always blocks are executed. So it might look ok in one simulator that executes the two always blocks in the order order they appear in the verilog file, but it might fail in another simulator that chooses a different order for evaluating the always block.

In synthesis it is simply a driver-driver conflict. Running something like yosys -p 'proc; check' fsm_orig.v will even tell you that your design contains driver-driver conflicts for the three state bits:

3. Executing CHECK pass (checking for obvious problems).
checking module fsm..
Warning: multiple conflicting drivers for fsm.\state [2]:
    port Q[2] of cell $procdff$44 ($dff)
    port Q[2] of cell $procdff$43 ($dff)
Warning: multiple conflicting drivers for fsm.\state [1]:
    port Q[1] of cell $procdff$44 ($dff)
    port Q[1] of cell $procdff$43 ($dff)
Warning: multiple conflicting drivers for fsm.\state [0]:
    port Q[0] of cell $procdff$44 ($dff)
    port Q[0] of cell $procdff$43 ($dff)
found and reported 3 problems.
cliffordwolf commented 9 years ago

It must show you that the STATE_ML thing is not working..

Oops! Sorry! I misread your code. You are actually assign state <= STATE_ML; and treating it as a separate state. So please forget everything I've said about that. -- The only problem was the driver-driver conflict after all.

dvc94ch commented 9 years ago

I guess my state naming isn't ideal. I missed the check warnings - silly me.

Thank you again and sorry for wasting your time...

On Fri, Nov 13, 2015 at 12:28 PM, Clifford Wolf notifications@github.com wrote:

I thought I read somewhere that that was good coding style to split your fsm into 2 or 3 always blocks.

Yes, but like this: :)

reg [2:0] next_state; reg [2:0] state;

always @* begin next_state = ...; end

always @(posedge clk) begin state <= next_state; end

Not by writing to the same signal from multiple blocks. That just has undefined behavior!

I did write a testbench and it did not show the problem...

It must show you that the STATE_ML thing is not working..

The other problem is tricky to spot in simulation, because in simulation the undefined part is simply in which order the always blocks are executed. So it might look ok in one simulator that executes the two always blocks in the order order they appear in the verilog file, but it might fail in another simulator that chooses a different order for evaluating the always block.

In synthesis it is simply a driver-driver conflict. Running something like yosys -p 'proc; check' fsm_orig.v will even tell you that your design contains driver-driver conflicts for the three state bits:

  1. Executing CHECK pass (checking for obvious problems). checking module fsm.. Warning: multiple conflicting drivers for fsm.\state [2]: port Q[2] of cell $procdff$44 ($dff) port Q[2] of cell $procdff$43 ($dff) Warning: multiple conflicting drivers for fsm.\state [1]: port Q[1] of cell $procdff$44 ($dff) port Q[1] of cell $procdff$43 ($dff) Warning: multiple conflicting drivers for fsm.\state [0]: port Q[0] of cell $procdff$44 ($dff) port Q[0] of cell $procdff$43 ($dff) found and reported 3 problems.

— Reply to this email directly or view it on GitHub https://github.com/cliffordwolf/yosys/issues/100#issuecomment-156403050.