Merge pull request #1303 from diffblue/word-level-smv-array

array types for word-level SMV output

Author: tautschnig

regression/ebmc/smv-word-level/verilog3.desc

@@ -0,0 +1,10 @@
+CORE
+verilog3.sv
+--smv-word-level
+^MODULE main$
+^VAR some_array : array 0\.\.31 of unsigned word\[8\];$
+^TRANS next\(main\.some_array\) = main\.some_array$
+^LTLSPEC G main\.some_array\[resize\(unsigned\(0sd32_0\), 5\)\] = 0ud8_123$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-word-level/verilog3.sv

@@ -0,0 +1,8 @@
+module main(input clk);
+
+  // an array of bytes
+  reg [7:0] some_array [32];
+
+  assert property (@(posedge clk) some_array[0] == 8'd123);
+
+endmodule

src/ebmc/output_smv_word_level.cpp

@@ -45,7 +45,8 @@ operator<<(std::ostream &out, const smv_type_printert &type_printer)
 
   if(
     type.id() == ID_bool || type.id() == ID_signedbv ||
-    type.id() == ID_unsignedbv || type.id() == ID_range)
+    type.id() == ID_unsignedbv || type.id() == ID_range ||
+    type.id() == ID_array)
   {
     return out << type2smv(type, ns);
   }

src/smvlang/expr2smv.cpp

@@ -952,10 +952,15 @@ std::string type2smv(const typet &type, const namespacet &ns)
     return "boolean";
   else if(type.id()==ID_array)
   {
+    auto &array_type = to_array_type(type);
+    auto size_const = to_constant_expr(array_type.size());
+    auto size_int = numeric_cast_v<mp_integer>(size_const);
     std::string code = "array ";
-    code+="..";
+    // The index type cannot be any type, but must be a range low..high
+    code += "0..";
+    code += integer2string(size_int - 1);
     code+=" of ";
-    code += type2smv(to_array_type(type).element_type(), ns);
+    code += type2smv(array_type.element_type(), ns);
     return code;
   }
   else if(type.id() == ID_smv_enumeration)