Verilog: fix array index direction for descending and ascending ranges

Arrays declared with descending ranges (e.g., [4:0]) or ascending ranges
with non-zero offsets were not correctly mapping Verilog indices to
internal array indices. This affected both packed and unpacked arrays.

For unpacked arrays, the Verilog index is now adjusted to the internal
index based on the range direction and offset. For packed arrays, the
assignment pattern operands are reversed for descending ranges so that
internal index 0 corresponds to Verilog index 0, and the bitvector
lowering is updated to match.

Per IEEE 1800-2017 section 10.9.1, assignment patterns assign elements
left-to-right starting from the left index of the range.

Author: kroening

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

@@ -16,9 +16,9 @@ module main;
   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);
+  p21: assert property (s.array2[0] == 4);
+  p22: assert property (s.array2[1] == 3);
+  p23: assert property (s.array2[2] == 2);
+  p24: assert property (s.array2[3] == 1);
 
 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();