Same registers created by "write_smt2" could be wires with "write_verilog" #4205
Unanswered
zilongwang123
asked this question in
Q&A
Replies: 1 comment 1 reply
-
I can't reproduce this. This is what 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 |
Beta Was this translation helpful? Give feedback.
1 reply
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
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?
Beta Was this translation helpful? Give feedback.
All reactions