YosysHQ / yosys

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

frontend: Fixes verific import around range order #4379

Closed QuantamHD closed 1 month ago

QuantamHD commented 1 month ago

Test Case

module packed_dimensions_range_ordering (
    input  wire [0:4-1] in,
    output wire [4-1:0] out
);
  assign out = in;
endmodule : packed_dimensions_range_ordering

module instanciates_packed_dimensions_range_ordering (
    input  wire [4-1:0] in,
    output wire [4-1:0] out
);
  packed_dimensions_range_ordering U0 (
      .in (in),
      .out(out)
  );
endmodule : instanciates_packed_dimensions_range_ordering
// with verific, does not pass formal
module instanciates_packed_dimensions_range_ordering(in, out);
  input [3:0] in;
  wire [3:0] in;
  output [3:0] out;
  wire [3:0] out;

  assign out = { in[0], in[1], in[2], in[3] };
endmodule

// with surelog, passes formal
module instanciates_packed_dimensions_range_ordering(in, out);
  input [3:0] in;
  wire [3:0] in;
  output [3:0] out;
  wire [3:0] out;

  assign out = in;
endmodule

Script

verific -sv test.sv
verific -import -vv instanciates_packed_dimensions_range_ordering
hierarchy -top instanciates_packed_dimensions_range_ordering
flatten
opt
clean -purge
write_verilog -simple-lhs -noattr -noexpr result3.v
QuantamHD commented 1 month ago

@mmicko I found another set of bugs where the index of the list is of the form [2:7] and [-12:7]. I had to add another term to the equation to make sure the indexes weren't offset from 0

mmicko commented 1 month ago

Thanks @QuantamHD managed to reproduce issue and this indeed covers it