From a2c1b268d9fa664fcd08723cdb673ce9ea87e786 Mon Sep 17 00:00:00 2001
From: Ethan Mahintorabi <ethanmoon@google.com>
Date: Wed, 8 May 2024 01:00:06 +0000
Subject: [PATCH] frontend: Fixes verific import around range order

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>
---
 frontends/verific/verific.cc | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 81e79f7497f..6203013bf68 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -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];