Verilog: aval/bval lowering of 4-valued logic

This introduces the standard aval/bval lowering of Verilog's 4-valued logic
into bit vectors.

Author: kroening

lib/cbmc

@@ -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/hw_cbmc_irep_ids.h

@@ -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/Makefile

@@ -0,0 +1,77 @@
+/*******************************************************************\
+
+Module: aval/bval encoding
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "aval_bval_encoding.h"
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/std_expr.h>
+
+bv_typet aval_bval_type(std::size_t width)
+{
+  auto result = bv_typet{width * 2};
+  result.set(ID_C_verilog_aval_bval, true);
+  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());
+}
+
+bool is_aval_bval(const typet &type)
+{
+  return type.id() == ID_bv && type.get_bool(ID_C_verilog_aval_bval);
+}
+
+std::size_t aval_bval_width(const typet &type)
+{
+  PRECONDITION(is_aval_bval(type));
+  return to_bv_type(type).get_width() / 2;
+}
+
+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_index = 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[src_index])
+    {
+    case '0':
+      return bval ? 0 : 0;
+    case '1':
+      return bval ? 0 : 1;
+    case 'z':
+      return bval ? 1 : 1;
+    case 'x':
+      return bval ? 1 : 0;
+    default:
+      INVARIANT(false, "unexpected Verilog vector bit");
+    }
+  };
+
+  return constant_exprt{make_bvrep(width * 2, bv_f), new_type};
+}

src/verilog/aval_bval_encoding.cpp

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+Module: aval/bval encoding
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_AVAL_BVAL_H
+#define CPROVER_VERILOG_AVAL_BVAL_H
+
+#include <util/expr.h>
+
+class bv_typet;
+class constant_exprt;
+
+// 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 &);
+
+bv_typet lower_to_aval_bval(const typet &);
+constant_exprt lower_to_aval_bval(const constant_exprt &);
+
+// extract a/b vectors
+exprt aval_bval_a(const exprt &);
+exprt aval_bval_b(const exprt &);
+
+#endif

src/verilog/aval_bval_encoding.h

@@ -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));
@@ -2262,15 +2275,14 @@ exprt verilog_synthesist::case_comparison(
 {
   // we need to take case of ?, x, z in the pattern
   const typet &pattern_type=pattern.type();
-  
-  if(pattern_type.id()==ID_verilog_signedbv ||
-     pattern_type.id()==ID_verilog_unsignedbv)
+
+  if(is_aval_bval(pattern_type))
   {
     // try to simplify the pattern
     exprt tmp=pattern;
 
     simplify(tmp, ns);
-    
+
     if(tmp.id()!=ID_constant)
     {
       warning().source_location=pattern.source_location();
@@ -2279,43 +2291,39 @@ exprt verilog_synthesist::case_comparison(
     else
     {
       exprt new_case_operand=case_operand;
+      auto width = aval_bval_width(pattern_type);
 
       // 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';
+      bv_typet comparison_type{width};
+      new_case_operand = typecast_exprt{new_case_operand, comparison_type};
 
-      auto new_pattern =
-        from_integer(string2integer(new_pattern_value, 2), new_type);
+      auto &pattern_value = id2string(to_constant_expr(tmp).get_value());
 
-      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);
-
-      exprt bitand_expr = bitand_exprt{new_case_operand, new_mask};
-
-      return equal_exprt{bitand_expr, new_pattern};
+      // we are using masking!
+      auto value_bvrep =
+        make_bvrep(width, [pattern_value](const std::size_t index) {
+          // 0?zx -> 0
+          // 1    -> 1
+          DATA_INVARIANT(
+            index < pattern_value.size(), "index within pattern_value");
+          return pattern_value[index] == '1';
+        });
+
+      auto mask_bvrep =
+        make_bvrep(width, [pattern_value](const std::size_t index) {
+          // ?zx -> 0
+          // 01  -> 1
+          DATA_INVARIANT(
+            index < pattern_value.size(), "index within pattern_value");
+          return pattern_value[index] == '0' || pattern_value[index] == '1';
+        });
+
+      auto value_expr = constant_exprt{value_bvrep, comparison_type};
+      auto mask_expr = constant_exprt{mask_bvrep, comparison_type};
+
+      exprt bitand_expr = bitand_exprt{new_case_operand, mask_expr};
+
+      return equal_exprt{bitand_expr, value_expr};
     }
   }
 

src/verilog/verilog_synthesis.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_VERILOG_SYNTHESIS_CLASS_H
 #define CPROVER_VERILOG_SYNTHESIS_CLASS_H
 
+#include <util/bitvector_types.h>
 #include <util/mathematical_expr.h>
 #include <util/mp_arith.h>
 #include <util/options.h>
@@ -326,6 +327,17 @@ class verilog_synthesist:
   void function_locality(const symbolt &);
 
   unsigned temporary_counter;
+
+  static bool is_aval_bval(const typet &type)
+  {
+    return type.id() == ID_bv && type.get_bool(ID_C_verilog_aval_bval);
+  }
+
+  static std::size_t aval_bval_width(const typet &type)
+  {
+    PRECONDITION(is_aval_bval(type));
+    return to_bv_type(type).get_width() / 2;
+  }
 };
 
 #endif