Verilog: fix array index direction for descending and ascending ranges

regression/verilog/arrays/array_conversion3.desc

@@ -6,12 +6,12 @@ array_conversion3.sv
 ^\[main\.p13\] main\.array1\[2\] == 3: PROVED .*$
 ^\[main\.p14\] main\.array1\[3\] == 4: PROVED .*$
 ^\[main\.p15\] main\.array1 == 32'h1020304: PROVED .*$
-^\[main\.p21\] main\.array2\[0\] == 4: REFUTED$
-^\[main\.p22\] main\.array2\[1\] == 3: REFUTED$
-^\[main\.p23\] main\.array2\[2\] == 2: REFUTED$
-^\[main\.p24\] main\.array2\[3\] == 1: REFUTED$
+^\[main\.p21\] main\.array2\[0\] == 4: PROVED .*$
+^\[main\.p22\] main\.array2\[1\] == 3: PROVED .*$
+^\[main\.p23\] main\.array2\[2\] == 2: PROVED .*$
+^\[main\.p24\] main\.array2\[3\] == 1: PROVED .*$
 ^\[main\.p25\] main\.array2 == 32'h1020304: PROVED .*$
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 --

regression/verilog/arrays/packed_direction1.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 packed_direction1.sv
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This gives the wrong answer.

regression/verilog/arrays/unpacked_direction1.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 unpacked_direction1.sv
 --module main
+^\[main\.p0\] main\.my_array0\[0\] == 1: PROVED .*$
+^\[main\.p1\] main\.my_array1\[0\] == 1: PROVED .*$
+^\[main\.p2\] main\.my_array2\[0 \+ 5 - 3'b001 - 0\] == 5: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This gives the wrong answer.

regression/verilog/structs/array_in_struct1.sv

@@ -8,17 +8,19 @@ module main;
     bit [3:0] [31:0] array2;
   } s;
 
-  initial s = '{ '{ 1, 2, 3, 4 }, '{ 1, 2, 3, 4 } };
+  initial begin
+    s = '{ '{ 1, 2, 3, 4 }, '{ 1, 2, 3, 4 } };
 
-  // Expected to pass.
-  p0: assert final ($bits(s) == 4 * 32 + 4 * 32);
-  p11: assert property (s.array1[0] == 1);
-  p12: assert property (s.array1[1] == 2);
-  p13: assert property (s.array1[2] == 3);
-  p14: assert property (s.array1[3] == 4);
-  p21: assert property (s.array2[0] == 1);
-  p22: assert property (s.array2[1] == 2);
-  p23: assert property (s.array2[2] == 3);
-  p24: assert property (s.array2[3] == 4);
+    // Expected to pass.
+    p0: assert($bits(s) == 4 * 32 + 4 * 32);
+    p11: assert(s.array1[0] == 1);
+    p12: assert(s.array1[1] == 2);
+    p13: assert(s.array1[2] == 3);
+    p14: assert(s.array1[3] == 4);
+    p21: assert(s.array2[0] == 4);
+    p22: assert(s.array2[1] == 3);
+    p23: assert(s.array2[2] == 2);
+    p24: assert(s.array2[3] == 1);
+  end
 
 endmodule

src/verilog/verilog_elaborate_type.cpp

@@ -173,6 +173,7 @@ typet verilog_typecheck_exprt::convert_packed_array_type(
 
     array_typet result{element_type, size};
     result.set(ID_offset, from_integer(offset, integer_typet()));
+    result.set(ID_C_increasing, range.increasing());
     result.set(ID_C_verilog_type, ID_verilog_packed_array);
 
     return std::move(result).with_source_location(source_location);

src/verilog/verilog_lowering.cpp

@@ -233,7 +233,7 @@ exprt to_bitvector(const exprt &src)
     bool is_packed =
       array_type.get(ID_C_verilog_type) == ID_verilog_packed_array;
 
-    if(is_packed && !array_type.get_bool(ID_C_increasing))
+    if(is_packed && array_type.get_bool(ID_C_increasing))
     {
       for(std::size_t index = 0; index < size_int; index++)
       {

src/verilog/verilog_typecheck_expr.cpp

@@ -231,6 +231,18 @@ void verilog_typecheck_exprt::assignment_conversion(
         assignment_conversion(rhs.operands()[i], element_type);
       }
 
+      // For packed arrays with descending range (e.g., [3:0]),
+      // the assignment pattern lists elements from the left (highest)
+      // index to the right (lowest), but internally index 0 must
+      // correspond to Verilog index 0 (the lowest). Reverse the
+      // operands so that internal[0] = last element = Verilog index 0.
+      if(
+        array_type.get(ID_C_verilog_type) == ID_verilog_packed_array &&
+        !array_type.get_bool(ID_C_increasing))
+      {
+        std::reverse(rhs.operands().begin(), rhs.operands().end());
+      }
+
       // turn into array expression
       rhs.id(ID_array);
       rhs.type() = lhs_type;
@@ -3000,13 +3012,35 @@ exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr)
     typet _index_type = index_type(array_type);
     op1 = typecast_exprt{op1, _index_type};
 
-    if(
-      array_type.get_bool(ID_C_increasing) &&
-      array_type.get(ID_C_verilog_type) == ID_verilog_packed_array)
+    // For unpacked arrays, the internal representation stores
+    // elements starting from the left index of the range.
+    // We need to adjust the Verilog index to the internal index.
+    if(array_type.get(ID_C_verilog_type) == ID_verilog_unpacked_array)
     {
-      expr.op1() = minus_exprt{
-        minus_exprt{typecast_exprt{array_type.size(), _index_type}, expr.op1()},
-        from_integer(1, _index_type)};
+      auto offset_expr = static_cast<const exprt &>(array_type.find(ID_offset));
+
+      if(array_type.get_bool(ID_C_increasing))
+      {
+        // ascending range [l:r] with l<r, e.g., [0:4]
+        // internal index = verilog_index - offset
+        if(!offset_expr.is_zero())
+        {
+          expr.op1() =
+            minus_exprt{expr.op1(), typecast_exprt{offset_expr, _index_type}};
+        }
+      }
+      else
+      {
+        // descending range [l:r] with l>=r, e.g., [4:0]
+        // internal index = (offset + size - 1) - verilog_index
+        expr.op1() = minus_exprt{
+          minus_exprt{
+            plus_exprt{
+              typecast_exprt{offset_expr, _index_type},
+              typecast_exprt{array_type.size(), _index_type}},
+            from_integer(1, _index_type)},
+          expr.op1()};
+      }
     }
 
     expr.type() = array_type.element_type();