aval/bval for bitwise not

This adds an aval/bval encoding for 4-valued bitwise NOT expressions.

Author: kroening

regression/verilog/expressions/bitwise_not1.desc

@@ -0,0 +1,7 @@
+CORE
+bitwise_not1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/bitwise_not1.sv

@@ -0,0 +1,12 @@
+module main;
+
+  assert final (~0 === 'hffff_ffff);
+  assert final (~1 === 'hffff_fffe);
+  assert final (~(-('sd1)) === 0);
+  assert final (~3'b101 === 3'b010);
+  assert final (~3'bxxx === 3'bxxx);
+  assert final (~3'bzzz === 3'bxxx);
+  assert final (~3'b10x === 3'b01x);
+  assert final (~3'b10z === 3'b01x);
+
+endmodule

src/verilog/aval_bval_encoding.cpp

@@ -180,6 +180,7 @@ combine_aval_bval(const exprt &aval, const exprt &bval, const typet &dest)
 {
   PRECONDITION(aval.type().id() == ID_bv);
   PRECONDITION(bval.type().id() == ID_bv);
+  PRECONDITION(dest.id() == ID_bv);
   return concatenation_exprt{{bval, aval}, dest};
 }
 
@@ -336,6 +337,24 @@ exprt aval_bval(const not_exprt &expr)
   return if_exprt{has_xz, x, aval_bval_conversion(not_expr, x.type())};
 }
 
+exprt aval_bval(const bitnot_exprt &expr)
+{
+  auto &type = expr.type();
+  PRECONDITION(is_four_valued(type));
+  PRECONDITION(is_aval_bval(expr.op()));
+
+  // x/z is done bit-wise.
+  // ~z is x.
+  auto op_aval = aval(expr.op());
+  auto op_bval = bval(expr.op());
+
+  exprt aval = bitor_exprt{
+    bitand_exprt{bitnot_exprt{op_bval}, op_bval},                // x/z case
+    bitand_exprt{bitnot_exprt{op_aval}, bitnot_exprt{op_bval}}}; // 0/1 case
+
+  return combine_aval_bval(aval, op_bval, lower_to_aval_bval(expr.type()));
+}
+
 exprt aval_bval(const power_exprt &expr)
 {
   PRECONDITION(is_four_valued(expr.type()));

src/verilog/aval_bval_encoding.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_VERILOG_AVAL_BVAL_H
 #define CPROVER_VERILOG_AVAL_BVAL_H
 
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/mathematical_expr.h>
 
@@ -46,6 +47,8 @@ exprt aval_bval(const verilog_logical_inequality_exprt &);
 
 /// lowering for !
 exprt aval_bval(const not_exprt &);
+/// lowering for ~
+exprt aval_bval(const bitnot_exprt &);
 /// lowering for ==?
 exprt aval_bval(const verilog_wildcard_equality_exprt &);
 /// lowering for !=?

src/verilog/verilog_lowering.cpp

@@ -503,6 +503,16 @@ exprt verilog_lowering(exprt expr)
     else
       return expr; // leave as is
   }
+  else if(expr.id() == ID_bitnot)
+  {
+    auto &bitnot_expr = to_bitnot_expr(expr);
+
+    // encode into aval/bval
+    if(is_four_valued(expr.type()))
+      return aval_bval(bitnot_expr);
+    else
+      return expr; // leave as is
+  }
   else if(expr.id() == ID_verilog_iff)
   {
     auto &iff = to_verilog_iff_expr(expr);