flip-flop loaded into yosys becomes always block which feeds into itself, preventing gate-level simulation

Steps to reproduce the issue

Use the folowing yosys script on the following .sv file:

read_verilog -sv synth_out.sv
write_verilog 0.v

Where synth_out.sv is

module synth_out(
    input clk,
    input rst,
    input a,
    output reg out
);
    reg next_out;

    always @(*) begin
        next_out = 0;

        if(a) begin
            next_out = 1;
        end
    end

    always @(posedge clk, posedge rst) begin
        if(rst) begin
            out <= 0;
        end else begin
            out <= next_out;
        end
    end
endmodule

Examine 0.v, it contains an always block that feeds into itself:

  always @* begin
    if (\$auto$verilog_backend.cc:2083:dump_module$3 ) begin end
    _0_ = _2_;
    (* src = "prot/synth_out.sv:12.9-14.12" *)
    casez (a)
      /* src = "prot/synth_out.sv:12.12-12.13" */
      1'h1:
          _2_ = 1'h1;
      default:
          _2_ = 1'h0;
    endcase
  end

You can see that _2_ is both an input into the block, modifying the value of _0_, and also an output, according to the value of a. This means that if the value of a changs, this block needs to be scheduled twice, but it will only be scheduled once, since the write to 2 won't retrigger the block, since it's being modified by the block itself. Thus gate-level simulation of this code fails.

You can test this code using the following driver code:

module synth_out_test();
    reg clk;
    reg out;
    reg rst;
    reg a;

    synth_out synth_out1(
        .clk(clk),
        .out(out),
        .rst(rst),
        .a(a)
    );

    initial begin
        clk = 1;
        forever begin
            #5 clk = ~clk;
        end
    end

    initial begin
        $monitor("clk=%0b rst=%0b out=%0b a=%0b", clk, rst, out, a);
        rst = 1;
        a = 0;
        #10
        rst = 0;
        #10

        assert(~out);

        #10
        assert(~out);
        a = 1;

        #10
        assert(out);

        #10
        assert(out);

        #10;
        $display("done");

        #100 $finish;
    end
endmodule

This works fine on the original .sv file, but fails on the .v file written by yosys. eg using iverilog:

iverilog -g2012 prot/synth_out.sv prot/synth_out_test.sv && ./a.out

iverilog -g2012 0.v prot/synth_out_test.sv && ./a.out

Expected behavior

behavior when using the original verilog file, and the yosys loaded verilog file should be identical
yosys should not create an always block that updates itself, so taht a needed second run of the block is never triggered
this would allow me to run gate-level simulation

Actual behavior

yosys creates an always block that updates itself, and requires a second evaluation, but is never scheduled, since a simulator will not schedule blocks that are only triggered by themselves
gate-level simulation, eg using iverilog, of synthesized code from yosys does not match the behavior of the original files, nor match the intentions of the original code.

Ok. So, big nuance. It looks like if I go all the way throuhg synthesis, and then test the synthesized verilog in later stages it works ok in fact :) (I just have to make sure to run my asserts not exactly on the clock edge, but slightly after it, which makes total sense).

i.e. using the following yosys script:

write_verilog build/netlist/0.v
flatten
write_verilog build/netlist/1.v
synth
write_verilog build/netlist/2.v
techmap;
write_verilog build/netlist/3.v
dfflibmap -liberty {args.cell_lib}
write_verilog build/netlist/4.v
abc -liberty {args.cell_lib}
write_verilog build/netlist/5.v
clean
write_verilog build/netlist/6.v

write_rtlil build/rtlil.rtl
write_verilog build/netlist.v
ltp
sta
stat

... then 2.v, 3.v, 4.v, 5.v, and 6.v all work ok, as long as, as stated, I offset my tests slightly so tah the asserts dont land exactly on the clock edge, which makes total sense realy, in retrospect.

Nearly all passes in yosys only work on designs that have had hierarchy and proc called on them. Those two passes are kind of "the back end of the frontend", and only after that is the in-memory design actually an elaborated netlist. At that point it can be safely exported to verilog.

The following script:

read_verilog -sv synth_out.sv
hierarchy -top synth_out
proc
write_verilog 0.v

results in this file:

/* Generated by Yosys 0.15+40 (git sha1 305f94a28, clang 11.0.3 -fPIC -Os) */

(* top =  1  *)
(* src = "issue3234.sv:1.1-24.10" *)
module synth_out(clk, rst, a, out);
  (* src = "issue3234.sv:9.5-15.8" *)
  wire _0_;
  (* src = "issue3234.sv:17.5-23.8" *)
  wire _1_;
  (* src = "issue3234.sv:9.5-15.8" *)
  wire _2_;
  wire _3_;
  wire _4_;
  (* src = "issue3234.sv:4.11-4.12" *)
  input a;
  wire a;
  (* src = "issue3234.sv:2.11-2.14" *)
  input clk;
  wire clk;
  (* src = "issue3234.sv:7.9-7.17" *)
  wire next_out;
  (* src = "issue3234.sv:5.16-5.19" *)
  output out;
  reg out;
  (* src = "issue3234.sv:3.11-3.14" *)
  input rst;
  wire rst;
  (* src = "issue3234.sv:17.5-23.8" *)
  always @(posedge clk, posedge rst)
    if (rst) out <= 1'h0;
    else out <= _3_;
  assign _3_ = _4_ ? (* full_case = 32'd1 *) (* src = "issue3234.sv:12.12-12.13|issue3234.sv:12.9-14.12" *) 1'h1 : 1'h0;
  assign _0_ = _2_;
  assign _1_ = next_out;
  assign _4_ = a;
  assign _2_ = _3_;
  assign next_out = _3_;
endmodule

which looks like the correct behavior.

So, from a practical point of view, yes, I simply skip the first couple of lowered outputs, and start from 2.v, in my script.

That said, I would point out that the manual that Clifford/Claire wrote contains the following, which suggests that the 'front-end' only comprises lexing and parsing:

I feel that the doc could perhap be updated at some point, to state that running simulation on the first couple of lowered outputs are not supported, prior to running proc, but I'll go ahead and close this issue. Thanks! :)

YosysHQ / yosys