Same registers created by "write_smt2" could be wires with "write_verilog"

[zilongwang123]

I use write_verilog to get the design and write_smt2 to get the smt file. Then run the "yosys-smtbmc" to get the test bench. Then I run the 'iverilog' to get the counterexample using the design and test bench.
The problem is that some registers created by "write_smt2" could be wires with "write_verilog".

An example could be:

module test ( input clk, input s2, output [1:0] s1,); reg [1:0] s1 ; always @ (posedge clk) begin s1[0] <= s2; end endmodule

the script

read_verilog -sv test.v proc opt write_verilog test1.v write_smt2 test1.smt

The "write_verilog" will generate a register \s1_reg[0] for the $dff and s1 will be a two bits wire. But "write_smt2" will generate a two bits bitvec for s1. So when run the 'iverilog' there will be an error since the test bench trys to initial the s1.

How should I fix this gap?

[whitequark]

I can't reproduce this. This is what write_verilog gives me on your file:

module test(clk, s2, s1);
  reg \$auto$verilog_backend.cc:2334:dump_module$2  = 0;
  (* src = "x.v:1.70-1.115" *)
  reg _0_;
  (* src = "x.v:1.21-1.24" *)
  input clk;
  wire clk;
  (* src = "x.v:1.49-1.51" *)
  output [1:0] s1;
  reg [1:0] s1;
  (* src = "x.v:1.32-1.34" *)
  input s2;
  wire s2;
  always @* begin
    if (\$auto$verilog_backend.cc:2334:dump_module$2 ) begin end
    _0_ = s2;
  end
  always @(posedge clk) begin
      s1[0] <= _0_;
  end
endmodule

[zilongwang123]

Did you run 'proc' before 'write_verilog'? BTW, the Yosys version I use is 0.37+83.