mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 04:57:53 +00:00
Code Activity

frontend: Fixes verific import around range order

Browse source 
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
```

Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
This commit is contained in:
Ethan Mahintorabi 2024-05-08 01:00:06 +00:00
parent 2631c7e918
commit a2c1b268d9
No known key found for this signature in database
GPG key ID: 824E41B920BEA252
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
frontends/verific/verific.cc
View file

@ -2156,8 +2156,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
int port_offset = 0;
if (pr->GetPort()->Bus()) {
port_name = pr->GetPort()->Bus()->Name();
port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
int msb = pr->GetPort()->Bus()->LeftIndex();
int lsb = pr->GetPort()->Bus()->RightIndex();
int index_of_port = pr->GetPort()->Bus()->IndexOf(pr->GetPort());
port_offset = index_of_port - min(msb, lsb);
// In cases where the msb order is flipped we need to make sure
// that the indicies match LSB = 0 order to match the std::vector
// to SigSpec LSB = 0 precondition.
if (lsb > msb) {
port_offset = abs(port_offset - lsb);
}
}
IdString port_name_id = RTLIL::escape_id(port_name);
auto &sigvec = cell_port_conns[port_name_id];