Verilog: aval/bval lowering of 4-valued logic

regression/verilog/case/case1.v

@@ -1,20 +1,20 @@
 module main(input clk, x, y);
 
   reg [1:0] cnt1;
-  reg z;
+  reg result;
 
   initial cnt1=0;
-  initial z=0;
+  initial result=0;
 
   always @(posedge clk) cnt1=cnt1+1;
 
   always @(posedge clk)
     casex (cnt1)
       2'b00:;
       2'b01:;
-      2'b1?: z=1;
+      2'b1?: result=1;
     endcase
 
-  always assert p1: z==0;
+  always assert p1: result==0;
 
 endmodule

src/hw_cbmc_irep_ids.h

@@ -148,6 +148,7 @@ IREP_ID_ONE(uwire)
 IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
 IREP_ID_TWO(C_verilog_type, #verilog_type)
+IREP_ID_TWO(C_verilog_aval_bval, #verilog_aval_bval)
 IREP_ID_ONE(verilog_enum)
 IREP_ID_ONE(verilog_packed_array)
 IREP_ID_ONE(verilog_type_reference)

src/verilog/Makefile

@@ -1,4 +1,5 @@
-SRC = expr2verilog.cpp \
+SRC = aval_bval_encoding.cpp \
+      expr2verilog.cpp \
       sva_expr.cpp \
       verilog_elaborate.cpp \
       verilog_expr.cpp \

src/verilog/aval_bval_encoding.cpp

@@ -0,0 +1,154 @@
+/*******************************************************************\
+
+Module: aval/bval encoding
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "aval_bval_encoding.h"
+
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/mathematical_types.h>
+#include <util/std_expr.h>
+
+bv_typet aval_bval_type(std::size_t width, irep_idt source_type)
+{
+  PRECONDITION(!source_type.empty());
+  auto result = bv_typet{width * 2};
+  result.set(ID_C_verilog_aval_bval, source_type);
+  return result;
+}
+
+bv_typet lower_to_aval_bval(const typet &src)
+{
+  PRECONDITION(
+    src.id() == ID_verilog_unsignedbv || src.id() == ID_verilog_signedbv);
+  return aval_bval_type(to_bitvector_type(src).get_width(), src.id());
+}
+
+bool is_aval_bval(const typet &type)
+{
+  return type.id() == ID_bv && !type.get(ID_C_verilog_aval_bval).empty();
+}
+
+std::size_t aval_bval_width(const typet &type)
+{
+  PRECONDITION(is_aval_bval(type));
+  return to_bv_type(type).get_width() / 2;
+}
+
+typet aval_bval_underlying(const typet &src)
+{
+  auto id = src.get(ID_C_verilog_aval_bval);
+  if(id == ID_verilog_unsignedbv)
+    return unsignedbv_typet{aval_bval_width(src)};
+  else if(id == ID_verilog_signedbv)
+    return signedbv_typet{aval_bval_width(src)};
+  else
+    PRECONDITION(false);
+}
+
+constant_exprt lower_to_aval_bval(const constant_exprt &src)
+{
+  PRECONDITION(
+    src.type().id() == ID_verilog_signedbv ||
+    src.type().id() == ID_verilog_unsignedbv);
+
+  auto new_type = lower_to_aval_bval(src.type());
+  auto width = aval_bval_width(new_type);
+  auto &value = id2string(src.get_value());
+
+  auto bv_f = [width, value](const std::size_t dest_index) {
+    bool bval = dest_index >= width;
+    std::size_t src_bit_nr = bval ? dest_index - width : dest_index;
+
+    // bval aval | 4-state Verilog value
+    // ----------|----------------------
+    //   0    0  |   0
+    //   0    1  |   1
+    //   1    0  |   X
+    //   1    1  |   Z
+
+    switch(value[value.size() - 1 - src_bit_nr])
+    {
+    case '0':
+      return bval ? 0 : 0;
+    case '1':
+      return bval ? 0 : 1;
+    case 'x':
+      return bval ? 1 : 0;
+    case '?':
+    case 'z':
+      return bval ? 1 : 1;
+    default:
+      INVARIANT(false, "unexpected Verilog vector bit");
+    }
+  };
+
+  return constant_exprt{make_bvrep(width * 2, bv_f), new_type};
+}
+
+exprt aval(const exprt &src)
+{
+  PRECONDITION(is_aval_bval(src.type()));
+  auto width = aval_bval_width(src.type());
+  return extractbits_exprt{
+    src, from_integer(0, integer_typet()), bv_typet{width}};
+}
+
+exprt bval(const exprt &src)
+{
+  PRECONDITION(is_aval_bval(src.type()));
+  auto width = aval_bval_width(src.type());
+  return extractbits_exprt{
+    src, from_integer(width, integer_typet()), bv_typet{width}};
+}
+
+static exprt adjust_size(const exprt &src, std::size_t dest_width)
+{
+  auto src_width = to_bv_type(src.type()).get_width();
+  if(dest_width > src_width)
+  {
+    auto zeros = from_integer(0, bv_typet{dest_width - src_width});
+    return concatenation_exprt{{zeros, src}, bv_typet{dest_width}};
+  }
+  else if(dest_width < src_width)
+  {
+    return extractbits_exprt{
+      src, from_integer(0, integer_typet{}), bv_typet{dest_width}};
+  }
+  else
+    return src;
+}
+
+static exprt
+combine_aval_bval(const exprt &aval, const exprt &bval, const typet &dest)
+{
+  PRECONDITION(aval.type().id() == ID_bv);
+  PRECONDITION(bval.type().id() == ID_bv);
+  return concatenation_exprt{{bval, aval}, 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)
+  {
+    // 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);
+  }
+}

src/verilog/aval_bval_encoding.h

@@ -0,0 +1,37 @@
+/*******************************************************************\
+
+Module: aval/bval encoding
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_AVAL_BVAL_H
+#define CPROVER_VERILOG_AVAL_BVAL_H
+
+#include <util/bitvector_types.h>
+#include <util/std_expr.h>
+
+// bit-concoding for four-valued types
+//
+// bval aval | 4-state Verilog value
+// ----------|----------------------
+//   0    0  |   0
+//   0    1  |   1
+//   1    0  |   X
+//   1    1  |   Z
+
+bool is_aval_bval(const typet &);
+std::size_t aval_bval_width(const typet &);
+typet aval_bval_underlying(const typet &);
+
+bv_typet lower_to_aval_bval(const typet &);
+constant_exprt lower_to_aval_bval(const constant_exprt &);
+
+// extract a/b vectors
+exprt aval(const exprt &);
+exprt bval(const exprt &);
+
+exprt aval_bval_conversion(const exprt &, const typet &);
+
+#endif

src/verilog/verilog_synthesis.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
+#include "aval_bval_encoding.h"
 #include "expr2verilog.h"
 #include "sva_expr.h"
 #include "verilog_expr.h"
@@ -74,6 +75,18 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
       UNREACHABLE;
     }
   }
+  else if(expr.id() == ID_constant)
+  {
+    // encode into aval/bval
+    if(
+      expr.type().id() == ID_verilog_unsignedbv ||
+      expr.type().id() == ID_verilog_signedbv)
+    {
+      return lower_to_aval_bval(to_constant_expr(expr));
+    }
+
+    return expr;
+  }
   else if(expr.id()==ID_function_call)
   {
     return expand_function_call(to_function_call_expr(expr));
@@ -94,6 +107,19 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
     if(typecast_expr.op().is_constant())
       simplify(expr, ns);
 
+    if(
+      expr.type().id() == ID_verilog_unsignedbv ||
+      expr.type().id() == ID_verilog_signedbv)
+    {
+      auto aval_bval_type = lower_to_aval_bval(expr.type());
+
+      if(is_aval_bval(typecast_expr.op().type()))
+      {
+        // separately convert aval and bval
+        return aval_bval_conversion(typecast_expr.op(), aval_bval_type);
+      }
+    }
+
     return expr;
   }
   else if(expr.id() == ID_verilog_non_indexed_part_select)
@@ -2260,71 +2286,34 @@ exprt verilog_synthesist::case_comparison(
   const exprt &case_operand,
   const exprt &pattern)
 {
-  // we need to take case of ?, x, z in the pattern
+  // the pattern has the max type, not the case operand
   const typet &pattern_type=pattern.type();
-
-  if(pattern_type.id()==ID_verilog_signedbv ||
-     pattern_type.id()==ID_verilog_unsignedbv)
-  {
-    // try to simplify the pattern
-    exprt tmp=pattern;
-
-    simplify(tmp, ns);
-
-    if(tmp.id()!=ID_constant)
-    {
-      warning().source_location=pattern.source_location();
-      warning() << "unexpected case pattern: " << to_string(tmp) << eom;
-    }
-    else
-    {
-      exprt new_case_operand=case_operand;
-
-      // the pattern has the max type
-      unsignedbv_typet new_type(pattern.type().get_int(ID_width));
-      new_case_operand = typecast_exprt{new_case_operand, new_type};
-
-      // we are using masking!
-
-      std::string new_pattern_value=
-        id2string(to_constant_expr(tmp).get_value());
-
-      // ?zx -> 0
-      for(unsigned i=0; i<new_pattern_value.size(); i++)
-        if(new_pattern_value[i]=='?' ||
-           new_pattern_value[i]=='z' ||
-           new_pattern_value[i]=='x')
-          new_pattern_value[i]='0';
-
-      auto new_pattern =
-        from_integer(string2integer(new_pattern_value, 2), new_type);
-
-      std::string new_mask_value=
-        id2string(to_constant_expr(tmp).get_value());
 
-      // ?zx -> 0, 0 -> 1
-      for(unsigned i=0; i<new_mask_value.size(); i++)
-        if(new_mask_value[i]=='?' ||
-           new_mask_value[i]=='z' ||
-           new_mask_value[i]=='x')
-          new_mask_value[i]='0';
-        else
-          new_mask_value[i]='1';
-
-      auto new_mask = from_integer(string2integer(new_mask_value, 2), new_type);
+  // we need to take case of ?, x, z in the pattern
+  if(is_aval_bval(pattern_type))
+  {
+    // We are using masking based on the pattern.
+    // The aval is the comparison value, and the
+    // negation of bval is the mask.
+    auto pattern_aval = ::aval(pattern);
+    auto pattern_bval = ::bval(pattern);
+    auto mask_expr = bitnot_exprt{pattern_bval};
 
-      exprt bitand_expr = bitand_exprt{new_case_operand, new_mask};
+    auto case_operand_casted = typecast_exprt{
+      typecast_exprt::conditional_cast(
+        case_operand, aval_bval_underlying(pattern_type)),
+      mask_expr.type()};
 
-      return equal_exprt{bitand_expr, new_pattern};
-    }
+    return equal_exprt{
+      bitand_exprt{case_operand_casted, mask_expr},
+      bitand_exprt{pattern_aval, mask_expr}};
   }
 
-  if(pattern.type()==case_operand.type())
-    return equal_exprt(case_operand, pattern);
+  // 2-valued comparison
+  exprt case_operand_casted =
+    typecast_exprt::conditional_cast(case_operand, pattern_type);
 
-  // the pattern has the max type
-  exprt tmp_case_operand=typecast_exprt(case_operand, pattern.type());
-  return equal_exprt(tmp_case_operand, pattern);
+  return equal_exprt(case_operand_casted, pattern);
 }
 
 /*******************************************************************\