mirror of https://github.com/YosysHQ/yosys.git
simplify: regression test for AST_CELLARRAY simplification issue
This commit is contained in:
parent
dd8b412833
commit
cf3570abde
|
@ -0,0 +1,45 @@
|
|||
# Regression test for #3467
|
||||
read_verilog <<EOT
|
||||
|
||||
module bit_buf (
|
||||
input wire bit_in,
|
||||
output wire bit_out
|
||||
);
|
||||
assign bit_out = bit_in;
|
||||
endmodule
|
||||
|
||||
module top (
|
||||
input wire [3:0] data_in,
|
||||
output wire [3:0] data_out
|
||||
);
|
||||
|
||||
wire [3:0] data [0:4];
|
||||
|
||||
assign data[0] = data_in;
|
||||
assign data_out = data[4];
|
||||
|
||||
genvar i;
|
||||
generate
|
||||
for (i=0; i<=3; i=i+1) begin
|
||||
bit_buf bit_buf_instance[3:0] (
|
||||
.bit_in(data[i]),
|
||||
.bit_out(data[i + 1])
|
||||
);
|
||||
end
|
||||
endgenerate
|
||||
endmodule
|
||||
|
||||
module top2 (
|
||||
input wire [3:0] data_in,
|
||||
output wire [3:0] data_out
|
||||
);
|
||||
assign data_out = data_in;
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
hierarchy
|
||||
proc
|
||||
|
||||
miter -equiv -make_assert -flatten top top2 miter
|
||||
sat -prove-asserts -verify miter
|
Loading…
Reference in New Issue