Verilog: little_endian -> big_endian

Verilog vectors may use indices that either increase or decrease with the
significance of the indexed bit.  The default is to increase, i.e., a bit
with a bigger index has a higher significance.

This flips the type annotation used to distinguish the two cases from
ID_C_little_endian, to signal the increasing case, to ID_C_big_endian.

The benefit is that the common default does not require any annotation.

Author: kroening

regression/verilog/enums/enum2.desc

@@ -1,7 +1,7 @@
 CORE
 enum2.sv
 
-^file .* line 4: assignment to enum requires enum of the same type, but got signed \[0:31\]$
+^file .* line 4: assignment to enum requires enum of the same type, but got signed \[31:0\]$
 ^EXIT=2$
 ^SIGNAL=0$
 --

src/hw_cbmc_irep_ids.h

@@ -46,7 +46,7 @@ IREP_ID_ONE(sva_overlapped_implication)
 IREP_ID_ONE(sva_non_overlapped_implication)
 IREP_ID_ONE(module_instance)
 IREP_ID_TWO(C_offset, #offset)
-IREP_ID_TWO(C_little_endian, #little_endian)
+IREP_ID_TWO(C_big_endian, #big_endian)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)

src/trans-netlist/trans_trace.cpp

@@ -647,7 +647,7 @@ static std::string vcd_suffix(
     left_bound = offset;
     right_bound = left_bound+width-1;
 
-    if(type.get_bool(ID_C_little_endian))
+    if(!type.get_bool(ID_C_big_endian))
       std::swap(left_bound, right_bound);
 
     return "["+integer2string(left_bound)+":"+integer2string(right_bound)+"]";

src/verilog/expr2verilog.cpp

@@ -1361,7 +1361,7 @@ std::string expr2verilogt::convert(const typet &type)
   else if(type.id()==ID_unsignedbv || type.id()==ID_signedbv)
   {
     unsigned width=to_bitvector_type(type).get_width();
-    bool little_endian=type.get_bool(ID_C_little_endian);
+    bool big_endian = type.get_bool(ID_C_big_endian);
     unsigned offset=atoi(type.get(ID_C_offset).c_str());
 
     if(width!=0)
@@ -1373,18 +1373,18 @@ std::string expr2verilogt::convert(const typet &type)
         dest="signed ";
 
       dest+='[';
-      
-      if(little_endian)
+
+      if(big_endian)
       {
-        dest+=std::to_string(offset+width-1);
-        dest+=":";
         dest+=std::to_string(offset);
+        dest += ":";
+        dest += std::to_string(offset + width - 1);
       }
       else
       {
-        dest+=std::to_string(offset);
-        dest+=":";
         dest+=std::to_string(offset+width-1);
+        dest += ":";
+        dest += std::to_string(offset);
       }
 
       dest+="]";

src/verilog/verilog_typecheck_expr.cpp

@@ -483,22 +483,24 @@ constant_exprt verilog_typecheck_exprt::left(const exprt &expr)
       type.id() == ID_bool)
     {
       auto offset = type.get_int(ID_C_offset);
-      if(type.get_bool(ID_C_little_endian))
-        return offset + get_width(type) - 1;
-      else
+      if(type.get_bool(ID_C_big_endian))
         return offset;
+      else
+        return offset + get_width(type) - 1;
     }
     else if(type.id() == ID_array)
     {
       auto offset = numeric_cast_v<mp_integer>(
         to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
-      if(type.get_bool(ID_C_little_endian))
+      if(type.get_bool(ID_C_big_endian))
+        return offset;
+      else
+      {
         return offset +
                numeric_cast_v<mp_integer>(
                  to_constant_expr(to_array_type(type).size())) -
                1;
-      else
-        return offset;
+      }
     }
     else
       return 0;
@@ -531,22 +533,24 @@ constant_exprt verilog_typecheck_exprt::right(const exprt &expr)
       type.id() == ID_bool)
     {
       auto offset = type.get_int(ID_C_offset);
-      if(type.get_bool(ID_C_little_endian))
-        return offset;
-      else
+      if(type.get_bool(ID_C_big_endian))
         return offset + get_width(type) - 1;
+      else
+        return offset;
     }
     else if(type.id() == ID_array)
     {
       auto offset = numeric_cast_v<mp_integer>(
         to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
-      if(type.get_bool(ID_C_little_endian))
-        return offset;
-      else
+      if(type.get_bool(ID_C_big_endian))
+      {
         return offset +
                numeric_cast_v<mp_integer>(
                  to_constant_expr(to_array_type(type).size())) -
                1;
+      }
+      else
+        return offset;
     }
     else
       return 0;
@@ -576,10 +580,10 @@ constant_exprt verilog_typecheck_exprt::increment(const exprt &expr)
       type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv ||
       type.id() == ID_array)
     {
-      if(type.get_bool(ID_C_little_endian))
-        return 1;
-      else
+      if(type.get_bool(ID_C_big_endian))
         return -1;
+      else
+        return 1;
     }
     else
       return -1;
@@ -1330,9 +1334,8 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
       expr.type()=verilog_signedbv_typet(bits);
     else
       expr.type()=verilog_unsignedbv_typet(bits);
-    
+
     expr.set(ID_value, fvalue);
-    expr.set(ID_C_little_endian, true);
   }
   else
   {
@@ -1351,7 +1354,6 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
       expr.type()=unsignedbv_typet(bits);
 
     expr.set(ID_value, integer2bvrep(int_value, bits));
-    expr.set(ID_C_little_endian, true);
   }
 
   return std::move(expr);

src/verilog/verilog_typecheck_type.cpp

@@ -39,20 +39,21 @@ array_typet verilog_typecheck_exprt::convert_unpacked_array_type(
   const exprt &size_expr = static_cast<const exprt &>(src.find(ID_size));
 
   mp_integer size, offset;
-  bool little_endian;
+  bool big_endian;
 
   if(range_expr.is_not_nil())
   {
     // these may be negative
     mp_integer msb, lsb;
     convert_range(range_expr, msb, lsb);
-    little_endian = (lsb <= msb);
-    size = (little_endian ? msb - lsb : lsb - msb) + 1;
-    offset = little_endian ? lsb : msb;
+    big_endian = (lsb > msb);
+    size = (big_endian ? lsb - msb : msb - lsb) + 1;
+    DATA_INVARIANT(size >= 0, "array size must not be negative");
+    offset = big_endian ? msb : lsb;
   }
   else if(size_expr.is_not_nil())
   {
-    little_endian = true;
+    big_endian = false;
     size = convert_integer_constant_expression(size_expr);
     offset = 0;
     if(size < 0)
@@ -73,7 +74,7 @@ array_typet verilog_typecheck_exprt::convert_unpacked_array_type(
   const exprt final_size_expr = from_integer(size, integer_typet());
   auto result = array_typet{element_type, final_size_expr};
   result.set(ID_offset, from_integer(offset, integer_typet()));
-  result.set(ID_C_little_endian, little_endian);
+  result.set(ID_C_big_endian, big_endian);
 
   return result;
 }
@@ -182,11 +183,11 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     mp_integer msb, lsb;
     convert_range(range, msb, lsb);
 
-    bool little_endian=(lsb<=msb);
+    bool big_endian = (lsb > msb);
+
+    mp_integer width = (big_endian ? lsb - msb : msb - lsb) + 1;
+    mp_integer offset = big_endian ? msb : lsb;
 
-    mp_integer width=(little_endian?msb-lsb:lsb-msb)+1;
-    mp_integer offset=little_endian?lsb:msb;
-    
     // let's look at the subtype
     const auto subtype =
       static_cast<const typet &>(src).has_subtype()
@@ -204,7 +205,7 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
 
       dest.add_source_location() = source_location;
       dest.set_width(width.to_ulong());
-      dest.set(ID_C_little_endian, little_endian);
+      dest.set(ID_C_big_endian, big_endian);
       dest.set(ID_C_offset, integer2string(offset));
 
       return std::move(dest).with_source_location(source_location);

src/vhdl/expr2vhdl.cpp

@@ -745,7 +745,7 @@ std::string expr2vhdlt::convert(const typet &type)
   else if(type.id()==ID_unsignedbv || type.id()==ID_signedbv)
   {
     unsigned width=to_bitvector_type(type).get_width();
-    bool little_endian=type.get_bool(ID_C_little_endian);
+    bool little_endian = type.get_bool(ID_C_big_endian);
     unsigned offset=atoi(type.get(ID_C_offset).c_str());
 
     if(width!=0)