From a2c1b268d9fa664fcd08723cdb673ce9ea87e786 Mon Sep 17 00:00:00 2001 From: Ethan Mahintorabi Date: Wed, 8 May 2024 01:00:06 +0000 Subject: [PATCH 1/3] 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 --- 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]; From c039da2ec167e2ef825357b09e6f7713c4a476df Mon Sep 17 00:00:00 2001 From: Ethan Mahintorabi Date: Wed, 8 May 2024 01:09:52 +0000 Subject: [PATCH 2/3] renames variables for more code clairty Signed-off-by: Ethan Mahintorabi --- frontends/verific/verific.cc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 6203013bf68..a18f9fc877b 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2156,15 +2156,15 @@ 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(); - int msb = pr->GetPort()->Bus()->LeftIndex(); - int lsb = pr->GetPort()->Bus()->RightIndex(); + int msb_index = pr->GetPort()->Bus()->LeftIndex(); + int lsb_index = pr->GetPort()->Bus()->RightIndex(); int index_of_port = pr->GetPort()->Bus()->IndexOf(pr->GetPort()); - port_offset = index_of_port - min(msb, lsb); + port_offset = index_of_port - min(msb_index, lsb_index); // 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); + if (lsb_index > msb_index) { + port_offset = abs(port_offset - lsb_index); } } IdString port_name_id = RTLIL::escape_id(port_name); From 82a4a87c97e8755e915bade43cf4f8010787ac42 Mon Sep 17 00:00:00 2001 From: Ethan Mahintorabi Date: Wed, 8 May 2024 20:28:37 +0000 Subject: [PATCH 3/3] Fixes error with vector indicies of the form [2:7] [-12:7] Make sure that we correctly adjust the value to align it to a zero indexed list with lsb = 0 Signed-off-by: Ethan Mahintorabi --- frontends/verific/verific.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index a18f9fc877b..b4b0664d341 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2164,7 +2164,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma // that the indicies match LSB = 0 order to match the std::vector // to SigSpec LSB = 0 precondition. if (lsb_index > msb_index) { - port_offset = abs(port_offset - lsb_index); + port_offset = abs(port_offset - (lsb_index - min(msb_index, lsb_index))); } } IdString port_name_id = RTLIL::escape_id(port_name);