Merge pull request #569 from diffblue/avalbval-tc

cast from 2-valued to aval/bval 4-valued vectors

Author: tautschnig

regression/verilog/expressions/equality2.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE broken-smt-backend
 equality2.v
 --bound 0
 ^EXIT=0$

regression/verilog/expressions/equality2.v

@@ -2,15 +2,15 @@ module main;
 
   always assert property01: (10===10)==1;
   always assert property02: (10===20)==0;
-  always assert property03: (10!==10)==1;
-  always assert property04: (10!==20)==0;
+  always assert property03: (10!==10)==0;
+  always assert property04: (10!==20)==1;
   always assert property05: ('bx==='bx)==1;
   always assert property06: ('bz==='bz)==1;
   always assert property07: ('bx==='bz)==0;
   always assert property08: ('bx==='b1)==0;
   always assert property09: ('bz==='b1)==0;
   always assert property10: ('b1==='b01)==1; // zero extension
-  always assert property11: ('b1==='sb11)==0; // zero extension
-  always assert property12: ('sb1==='sb11)==1; // sign extension
+  always assert property11: ('b011==='sb11)==1; // zero extension
+  always assert property12: ('sb011==='sb11)==1; // sign extension
 
 endmodule

src/verilog/aval_bval_encoding.cpp

@@ -146,22 +146,32 @@ combine_aval_bval(const exprt &aval, const exprt &bval, const typet &dest)
 
 exprt aval_bval_conversion(const exprt &src, const typet &dest)
 {
-  PRECONDITION(is_aval_bval(src.type()));
   PRECONDITION(is_aval_bval(dest));
-
-  auto src_width = aval_bval_width(src.type());
   auto dest_width = aval_bval_width(dest);
 
-  if(src_width == dest_width)
+  if(is_aval_bval(src.type()))
   {
-    // same size
-    return typecast_exprt{src, dest};
+    auto src_width = aval_bval_width(src.type());
+
+    if(src_width == dest_width)
+    {
+      // same size
+      return typecast_exprt{src, dest};
+    }
+    else
+    {
+      auto new_aval = adjust_size(aval(src), dest_width);
+      auto new_bval = adjust_size(bval(src), dest_width);
+      return combine_aval_bval(new_aval, new_bval, dest);
+    }
   }
   else
   {
-    auto new_aval = adjust_size(aval(src), dest_width);
-    auto new_bval = adjust_size(bval(src), dest_width);
-    return combine_aval_bval(new_aval, new_bval, dest);
+    const bv_typet bv_type{dest_width};
+    auto aval =
+      typecast_exprt{typecast_exprt{src, aval_bval_underlying(dest)}, bv_type};
+    auto bval = bv_type.all_zeros_expr();
+    return combine_aval_bval(aval, bval, dest);
   }
 }
 

src/verilog/verilog_synthesis.cpp

@@ -268,12 +268,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
         dest_type.id() == ID_verilog_signedbv)
       {
         auto aval_bval_type = lower_to_aval_bval(dest_type);
-
-        if(is_aval_bval(src_type))
-        {
-          // separately convert aval and bval
-          return aval_bval_conversion(typecast_expr.op(), aval_bval_type);
-        }
+        return aval_bval_conversion(typecast_expr.op(), aval_bval_type);
       }
       else if(dest_type.id() == ID_struct)
       {