Verilog: fix for index on packed arrays that are lsb first

Verilog allows packed arrays (vectors) to arrange the bits in the vector in
order of decreasing significance.

As we internally always use increasing significance, we need to flip the
index around in this case.

Author: kroening

regression/verilog/expressions/bit-extract5.desc

@@ -0,0 +1,11 @@
+CORE
+bit-extract5.sv
+--module main --bound 0
+^\[main\.p0\] always main\.w1\[0\] && !main\.w1\[31\]: PROVED up to bound 0$
+^\[main\.p1\] always main\.w2\[0\] && !main\.w2\[31\]: PROVED up to bound 0$
+^\[main\.p2\] always main\.w3\[0\] && !main\.w3\[31\]: PROVED up to bound 0$
+^\[main\.p3\] always main\.w4\[0\] && !main\.w4\[31\]: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/bit-extract5.sv

@@ -0,0 +1,13 @@
+module main;
+
+  wire [31:0] w1 = 'b1;
+  wire [32:1] w2 = 'b1;
+  wire [0:31] w3 = 'b1;
+  wire [1:32] w4 = 'b1;
+
+  p0: assert property (w1[0] and !w1[31]);
+  p1: assert property (w2[1] and !w2[32]);
+  p2: assert property (w3[31] and !w3[0]);
+  p3: assert property (w4[32] and !w4[1]);
+
+endmodule

regression/verilog/expressions/bit-extract6.desc

@@ -0,0 +1,9 @@
+CORE
+bit-extract6.sv
+--module main --bound 0
+^\[main\.p0\] always \(main\.index == 8 |-> main\.vector\[7 - main\.index - 1\] == 1\): PROVED up to bound 0$
+^\[main\.p1\] always \(main\.index >= 1 \&\& main\.index <= 7 |-> main\.vector\[7 - main\.index - 1\] == 0\): PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/bit-extract6.sv

@@ -0,0 +1,13 @@
+module main;
+
+  wire [1:8] vector = 1;
+  wire [7:0] index;
+
+  // Non-constant index.
+  // Note that index 8 is the least significant bit.
+  p0: assert property (index == 8 |-> vector[index] == 1);
+
+  // Verilog guarantees that any out-of-bounds access is zero.
+  p1: assert property (index >= 1 && index <= 7 |-> vector[index] == 0);
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -1635,26 +1635,46 @@ bool verilog_typecheck_exprt::is_constant_expression(
   exprt tmp(expr);
 
   convert_expr(tmp);
-  ns.follow_macros(tmp);
-
-  simplify(tmp, ns);
 
-  if(tmp.is_true())
-  {
-    value=1;
-    return true;
-  }
-  else if(tmp.is_false())
-  {
-    value=0;
-    return true;
-  }
-  else if(!to_integer_non_constant(tmp, value))
+  auto integer_opt = is_constant_integer_post_convert(tmp);
+  if(integer_opt.has_value())
   {
+    value = integer_opt.value();
     return true;
   }
+  else
+    return false;
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::is_constant_integer_post_convert
+
+  Inputs:
 
-  return false;
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::optional<mp_integer>
+verilog_typecheck_exprt::is_constant_integer_post_convert(const exprt &expr)
+{
+  exprt tmp = expr;
+
+  ns.follow_macros(tmp);
+  tmp = simplify_expr(tmp, ns);
+
+  if(!tmp.is_constant())
+    return {};
+
+  if(tmp.is_true())
+    return 1;
+  else if(tmp.is_false())
+    return 0;
+  else
+    return numeric_cast<mp_integer>(to_constant_expr(tmp));
 }
 
 /*******************************************************************\
@@ -2189,65 +2209,65 @@ exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr)
   // Verilog's bit select expression may map onto an extractbit
   // or an array index expression, depending on the type of the first
   // operand.
-  exprt &op0 = expr.op0();
+  exprt &op0 = expr.op0(), &op1 = expr.op1();
   convert_expr(op0);
+  convert_expr(op1);
 
   if(op0.type().id() == ID_verilog_real)
   {
     throw errort().with_location(op0.source_location())
       << "bit-select of real is not allowed";
   }
 
-  if(op0.type().id()==ID_array)
+  if(op1.type().id() == ID_verilog_real)
   {
-    exprt &op1 = expr.op1();
-    convert_expr(op1);
-    if(op1.type().id() == ID_verilog_real)
-    {
-      throw errort().with_location(op1.source_location())
-        << "real number index is not allowed";
-    }
+    throw errort().with_location(op1.source_location())
+      << "real number index is not allowed";
+  }
 
+  if(op0.type().id() == ID_array)
+  {
     typet _index_type = index_type(to_array_type(op0.type()));
-
-    if(_index_type!=op1.type())
-    {
-      mp_integer i;
-      if(!to_integer_non_constant(op1, i))
-        op1=from_integer(i, _index_type);
-      else if(op1.is_true() || op1.is_false())
-        op1=from_integer(op1.is_true()?1:0, _index_type);
-      else
-        op1 = typecast_exprt{op1, _index_type};
-    }
+    op1 = typecast_exprt{op1, _index_type};
 
     expr.type() = to_array_type(op0.type()).element_type();
     expr.id(ID_index);
   }
   else
   {
     auto width = get_width(op0.type());
-    auto offset = atoi(op0.type().get(ID_C_offset).c_str());
+    auto offset = op0.type().get_int(ID_C_offset);
 
-    mp_integer op1;
+    auto op1_opt = is_constant_integer_post_convert(op1);
 
-    if(is_constant_expression(expr.op1(), op1))
+    if(op1_opt.has_value()) // constant index
     {
       // 1800-2017 sec 11.5.1: out-of-bounds bit-select is
       // x for 4-state and 0 for 2-state values.
-      if(op1 < offset || op1 >= width + offset)
+      auto op1_int = op1_opt.value();
+
+      if(op1_int < offset || op1_int >= width + offset)
         return false_exprt().with_source_location(expr);
 
-      op1 -= offset;
-      expr.op1() = from_integer(op1, natural_typet());
+      op1_int -= offset;
+
+      if(op0.type().get_bool(ID_C_big_endian))
+        op1_int = width - op1_int - 1;
+
+      expr.op1() = from_integer(op1_int, natural_typet());
     }
-    else
+    else // non-constant index
     {
-      convert_expr(expr.op1());
-      if(expr.op1().type().id() == ID_verilog_real)
+      if(offset != 0)
+      {
+        expr.op1() =
+          minus_exprt{expr.op1(), from_integer(offset, expr.op1().type())};
+      }
+
+      if(op0.type().get_bool(ID_C_big_endian))
       {
-        throw errort().with_location(expr.op1().source_location())
-          << "real number index is not allowed";
+        expr.op1() =
+          minus_exprt{from_integer(width - 1, expr.op1().type()), expr.op1()};
       }
     }
 

src/verilog/verilog_typecheck_expr.h

@@ -104,6 +104,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   // elaboration (expansion and folding) of constant expressions and functions
   bool is_constant_expression(const exprt &, mp_integer &value);
+  std::optional<mp_integer> is_constant_integer_post_convert(const exprt &);
   exprt elaborate_constant_expression(exprt);
 
   // To be overridden, requires a Verilog interpreter.