Merge pull request #725 from diffblue/verilog-increasing

Verilog: big_endian -> increasing

Author: tautschnig

src/hw_cbmc_irep_ids.h

@@ -70,7 +70,7 @@ IREP_ID_ONE(sva_not)
 IREP_ID_ONE(sva_or)
 IREP_ID_ONE(module_instance)
 IREP_ID_TWO(C_offset, #offset)
-IREP_ID_TWO(C_big_endian, #big_endian)
+IREP_ID_TWO(C_increasing, #increasing)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)

src/trans-netlist/trans_trace.cpp

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

src/verilog/expr2verilog.cpp

@@ -1623,7 +1623,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 big_endian = type.get_bool(ID_C_big_endian);
+    bool increasing = type.get_bool(ID_C_increasing);
     unsigned offset=atoi(type.get(ID_C_offset).c_str());
 
     if(width!=0)
@@ -1636,7 +1636,7 @@ std::string expr2verilogt::convert(const typet &type)
 
       dest+='[';
 
-      if(big_endian)
+      if(increasing)
       {
         dest+=std::to_string(offset);
         dest += ":";

src/verilog/verilog_elaborate_type.cpp

@@ -39,19 +39,19 @@ 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 big_endian;
+  bool increasing;
 
   if(range_expr.is_not_nil())
   {
     // these may be negative
     auto range = convert_range(range_expr);
-    big_endian = (range.lsb > range.msb);
+    increasing = range.increasing();
     size = range.length();
     offset = range.smallest_index();
   }
   else if(size_expr.is_not_nil())
   {
-    big_endian = false;
+    increasing = false;
     size = convert_integer_constant_expression(size_expr);
     offset = 0;
     if(size < 0)
@@ -72,7 +72,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_big_endian, big_endian);
+  result.set(ID_C_increasing, increasing);
 
   return result;
 }
@@ -99,8 +99,6 @@ typet verilog_typecheck_exprt::convert_packed_array_type(
 
   auto range = convert_range(range_expr);
 
-  bool big_endian = (range.lsb > range.msb);
-
   mp_integer width = range.length();
   mp_integer offset = range.smallest_index();
 
@@ -122,7 +120,7 @@ typet verilog_typecheck_exprt::convert_packed_array_type(
 
     dest.add_source_location() = source_location;
     dest.set_width(width.to_ulong());
-    dest.set(ID_C_big_endian, big_endian);
+    dest.set(ID_C_increasing, range.increasing());
     dest.set(ID_C_offset, integer2string(offset));
 
     return std::move(dest).with_source_location(source_location);

src/verilog/verilog_typecheck_expr.cpp

@@ -484,7 +484,7 @@ 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_big_endian))
+      if(type.get_bool(ID_C_increasing))
         return offset;
       else
         return offset + get_width(type) - 1;
@@ -493,7 +493,7 @@ constant_exprt verilog_typecheck_exprt::left(const exprt &expr)
     {
       auto offset = numeric_cast_v<mp_integer>(
         to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
-      if(type.get_bool(ID_C_big_endian))
+      if(type.get_bool(ID_C_increasing))
         return offset;
       else
       {
@@ -534,7 +534,7 @@ 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_big_endian))
+      if(type.get_bool(ID_C_increasing))
         return offset + get_width(type) - 1;
       else
         return offset;
@@ -543,7 +543,7 @@ constant_exprt verilog_typecheck_exprt::right(const exprt &expr)
     {
       auto offset = numeric_cast_v<mp_integer>(
         to_constant_expr(static_cast<const exprt &>(type.find(ID_offset))));
-      if(type.get_bool(ID_C_big_endian))
+      if(type.get_bool(ID_C_increasing))
       {
         return offset +
                numeric_cast_v<mp_integer>(
@@ -608,7 +608,7 @@ 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_big_endian))
+      if(type.get_bool(ID_C_increasing))
         return -1;
       else
         return 1;
@@ -2516,7 +2516,7 @@ exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr)
 
       op1_int -= offset;
 
-      if(op0.type().get_bool(ID_C_big_endian))
+      if(op0.type().get_bool(ID_C_increasing))
         op1_int = width - op1_int - 1;
 
       expr.op1() = from_integer(op1_int, natural_typet());
@@ -2529,7 +2529,7 @@ exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr)
           minus_exprt{expr.op1(), from_integer(offset, expr.op1().type())};
       }
 
-      if(op0.type().get_bool(ID_C_big_endian))
+      if(op0.type().get_bool(ID_C_increasing))
       {
         expr.op1() =
           minus_exprt{from_integer(width - 1, expr.op1().type()), expr.op1()};

src/verilog/verilog_typecheck_expr.h

@@ -79,13 +79,19 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
     mp_integer msb, lsb;
 
-    /// return true iff the bit with the higest index
-    /// is the most significant bit
-    bool highest_index_is_msb() const
+    /// Return true iff the bit with the higest index
+    /// is the most significant bit, i.e., the vector
+    /// is indexed left-to-right with decreasing indices.
+    bool decreasing() const
     {
       return msb >= lsb;
     }
 
+    bool increasing() const
+    {
+      return !decreasing();
+    }
+
     mp_integer length() const
     {
       if(msb >= lsb)

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_big_endian);
+    bool increasing = type.get_bool(ID_C_increasing);
     unsigned offset=atoi(type.get(ID_C_offset).c_str());
 
     if(width!=0)
@@ -757,8 +757,8 @@ std::string expr2vhdlt::convert(const typet &type)
         dest="signed bv";
 
       dest+='[';
-      
-      if(little_endian)
+
+      if(!increasing)
       {
         dest+=std::to_string(offset+width-1);
         dest+=":";