SystemVerilog: set membership operator

kroening · kroening · commit 42e80b010f3f · 2024-11-14T17:21:37.000Z
This adds the set membership operator, 1800-2017 11.4.13.
diff --git a/CHANGELOG b/CHANGELOG
@@ -4,6 +4,7 @@
 * BMC: iterative constraint strengthening is now default;
   use --bmc-with-assumptions to re-enable the previous algorithm.
 * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
+* SystemVerilog: set membership operator
 
 # EBMC 5.3
 
diff --git a/regression/verilog/expressions/inside1.desc b/regression/verilog/expressions/inside1.desc
@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+inside1.sv
+--bound 0
+^\[.*\] always 2 inside \{1, 2, 3\}: PROVED up to bound 0$
+^\[.*\] always 2 inside \{3'b0\?0\}: PROVED up to bound 0$
+^\[.*\] always !\(2 inside \{3'b0\?1\}\): PROVED up to bound 0$
+^\[.*\] always 2 inside \{\[1:3\], \[6:8\]\}: PROVED up to bound 0$
+^\[.*\] always !\(4 inside \{\[1:3\], \[6:8\]\}\): PROVED up to bound 0$
+^\[.*\] always \(1 && 1\) inside \{1, 2, 3\}: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/verilog/expressions/inside1.sv b/regression/verilog/expressions/inside1.sv
@@ -0,0 +1,10 @@
+module main;
+
+  assert final (2 inside {1, 2, 3});
+  assert final (2 inside {3'b0?0});
+  assert final (!(2 inside {3'b0?1}));
+  assert final (2 inside {[1:3], [6:8]});
+  assert final (!(4 inside {[1:3], [6:8]}));
+  assert final ((1&&1) inside {1, 2, 3});
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -84,6 +84,7 @@ IREP_ID_ONE(verilog_wildcard_inequality)
 IREP_ID_ONE(verilog_explicit_cast)
 IREP_ID_ONE(verilog_size_cast)
 IREP_ID_ONE(verilog_implicit_typecast)
+IREP_ID_ONE(verilog_inside)
 IREP_ID_ONE(verilog_unique)
 IREP_ID_ONE(verilog_unique0)
 IREP_ID_ONE(verilog_priority)
@@ -93,6 +94,7 @@ IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)
 IREP_ID_ONE(verilog_past)
 IREP_ID_ONE(verilog_property_declaration)
+IREP_ID_ONE(verilog_value_range)
 IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
 IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
 IREP_ID_ONE(chandle)
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
@@ -1210,6 +1210,68 @@ expr2verilogt::resultt expr2verilogt::convert_streaming_concatenation(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_inside
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt
+expr2verilogt::convert_inside(const verilog_inside_exprt &src)
+{
+  std::string dest;
+  auto precedence = verilog_precedencet::RELATION;
+
+  auto op = convert_rec(src.op());
+
+  if(precedence > op.p)
+    dest += '(';
+  dest += op.s;
+  if(precedence > op.p)
+    dest += ')';
+
+  dest += " inside {";
+  bool first = true;
+  for(auto &op : src.range_list())
+  {
+    if(first)
+      first = false;
+    else
+      dest += ", ";
+    dest += convert_rec(op).s;
+  }
+  dest += "}";
+
+  return {precedence, dest};
+}
+
+/*******************************************************************\
+
+Function: expr2verilogt::convert_value_range
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt
+expr2verilogt::convert_value_range(const verilog_value_range_exprt &src)
+{
+  std::string dest =
+    '[' + convert_rec(src.lhs()).s + ':' + convert_rec(src.rhs()).s + ']';
+
+  return {verilog_precedencet::MEMBER, dest};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_rec
 
   Inputs:
@@ -1701,6 +1763,12 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_streaming_concatenation(
       "<<", to_verilog_streaming_concatenation_expr(src));
 
+  else if(src.id() == ID_verilog_inside)
+    return convert_inside(to_verilog_inside_expr(src));
+
+  else if(src.id() == ID_verilog_value_range)
+    return convert_value_range(to_verilog_value_range_expr(src));
+
   // no VERILOG language expression for internal representation 
   return convert_norep(src, precedence);
 }
diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h
@@ -30,7 +30,7 @@ enum class verilog_precedencet
   MULT = 15,     //  *  /  %
   ADD = 14,      //  + -
   SHIFT = 13,    //  <<  >>  <<<  >>>
-  RELATION = 12, //  >  >=  <  <=
+  RELATION = 12, //  >  >=  <  <= inside dist
   EQUALITY = 11, //  ==  !=  ===  !==  ==?  !=?
   BITAND = 10,   //  &
   XOR = 9,       //  ^  ~^  ^~ (binary)
@@ -159,6 +159,10 @@ class expr2verilogt
     const std::string &name,
     const class verilog_streaming_concatenation_exprt &);
 
+  resultt convert_inside(const class verilog_inside_exprt &);
+
+  resultt convert_value_range(const class verilog_value_range_exprt &);
+
 protected:
   const namespacet &ns;
 };
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -3360,6 +3360,15 @@ case_item:
                   mto($$, $2); }
 	;
 
+open_range_list:
+	  open_value_range
+		{ init($$); mto($$, $1); }
+	| open_range_list ',' open_value_range
+		{ $$=$1; mto($$, $3); }
+	;
+
+open_value_range: value_range;
+
 // System Verilog standard 1800-2017
 // A.6.7.1 Patterns
 
@@ -3854,11 +3863,18 @@ expression:
 		{ init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
 	| TOK_QSTRING
 		{ init($$, ID_constant); stack_expr($$).type()=typet(ID_string); addswap($$, ID_value, $1); }
+	| inside_expression
+	;
+
+inside_expression:
+	  expression TOK_INSIDE '{' open_range_list '}'
+		{ init($$, ID_verilog_inside); mto($$, $1); mto($$, $4); }
 	;
 
 value_range:
 	  expression
 	| '[' expression TOK_COLON expression ']'
+		{ init($$, ID_verilog_value_range); mto($$, $2); mto($$, $4); }
 	;
 
 indexed_range:
diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp
@@ -15,6 +15,18 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/prefix.h>
 
 #include "verilog_typecheck_base.h"
+#include "verilog_types.h"
+
+verilog_wildcard_equality_exprt::verilog_wildcard_equality_exprt(
+  exprt lhs,
+  exprt rhs)
+  : binary_exprt(
+      std::move(lhs),
+      ID_verilog_wildcard_equality,
+      std::move(rhs),
+      verilog_unsignedbv_typet{1})
+{
+}
 
 typet verilog_declaratort::merged_type(const typet &declaration_type) const
 {
@@ -340,3 +352,42 @@ exprt verilog_streaming_concatenation_exprt::lower() const
   else
     PRECONDITION(false);
 }
+
+exprt verilog_inside_exprt::lower() const
+{
+  exprt::operandst disjuncts;
+
+  for(auto &range : range_list())
+  {
+    if(range.id() == ID_verilog_value_range)
+    {
+      auto &range_expr = to_verilog_value_range_expr(range);
+      DATA_INVARIANT(
+        op().type() == range_expr.lhs().type(),
+        "inside_exprt type consistency");
+      DATA_INVARIANT(
+        op().type() == range_expr.rhs().type(),
+        "inside_exprt type consistency");
+      disjuncts.push_back(and_exprt{
+        binary_relation_exprt{op(), ID_ge, range_expr.lhs()},
+        binary_relation_exprt{op(), ID_le, range_expr.rhs()}});
+    }
+    else
+    {
+      DATA_INVARIANT(
+        op().type() == range.type(), "inside_exprt type consistency");
+      auto &range_type = range.type();
+      if(
+        range_type.id() == ID_verilog_unsignedbv ||
+        range_type.id() == ID_verilog_signedbv)
+      {
+        disjuncts.push_back(typecast_exprt{
+          verilog_wildcard_equality_exprt{op(), range}, bool_typet()});
+      }
+      else
+        disjuncts.push_back(equal_exprt{op(), range});
+    }
+  }
+
+  return disjunction(disjuncts);
+}
diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h
@@ -109,9 +109,10 @@ to_verilog_logical_inequality_expr(exprt &expr)
 }
 
 /// ==?
-class verilog_wildcard_equality_exprt : public equal_exprt
+class verilog_wildcard_equality_exprt : public binary_exprt
 {
 public:
+  verilog_wildcard_equality_exprt(exprt, exprt);
 };
 
 inline const verilog_wildcard_equality_exprt &
@@ -2511,4 +2512,70 @@ to_verilog_streaming_concatenation_expr(exprt &expr)
   return static_cast<verilog_streaming_concatenation_exprt &>(expr);
 }
 
+class verilog_inside_exprt : public binary_exprt
+{
+public:
+  verilog_inside_exprt(exprt _op, exprt::operandst _range_list)
+    : binary_exprt(
+        std::move(_op),
+        ID_verilog_inside,
+        exprt{irep_idt{}, typet{}, std::move(_range_list)})
+  {
+  }
+
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  const exprt::operandst &range_list() const
+  {
+    return op1().operands();
+  }
+
+  // lower to ==, ==?, >=, <=
+  exprt lower() const;
+};
+
+inline const verilog_inside_exprt &to_verilog_inside_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_inside);
+  verilog_inside_exprt::check(expr);
+  return static_cast<const verilog_inside_exprt &>(expr);
+}
+
+inline verilog_inside_exprt &to_verilog_inside_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_inside);
+  verilog_inside_exprt::check(expr);
+  return static_cast<verilog_inside_exprt &>(expr);
+}
+
+class verilog_value_range_exprt : public binary_exprt
+{
+public:
+  verilog_value_range_exprt(exprt from, exprt to)
+    : binary_exprt(std::move(from), ID_verilog_value_range, std::move(to))
+  {
+  }
+
+  // lower to >=, <=
+  exprt lower() const;
+};
+
+inline const verilog_value_range_exprt &
+to_verilog_value_range_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_value_range);
+  verilog_value_range_exprt::check(expr);
+  return static_cast<const verilog_value_range_exprt &>(expr);
+}
+
+inline verilog_value_range_exprt &to_verilog_value_range_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_value_range);
+  verilog_value_range_exprt::check(expr);
+  return static_cast<verilog_value_range_exprt &>(expr);
+}
+
 #endif
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
@@ -208,6 +208,12 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
       to_hierarchical_identifier_expr(expr), symbol_state);
     return expr;
   }
+  else if(expr.id() == ID_verilog_inside)
+  {
+    // The lowering uses wildcard equality, which needs to be further lowered
+    auto &inside = to_verilog_inside_expr(expr);
+    expr = inside.lower();
+  }
 
   // Do the operands recursively
   for(auto &op : expr.operands())
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -3179,6 +3179,24 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_verilog_inside)
+  {
+    convert_expr(expr.op0());
+    for(auto &op : expr.op1().operands())
+    {
+      convert_expr(op);
+      if(op.id() == ID_verilog_value_range)
+      {
+        auto &value_range = to_verilog_value_range_expr(op);
+        tc_binary_expr(expr, value_range.lhs(), op);
+        tc_binary_expr(expr, value_range.rhs(), op);
+      }
+      else
+        tc_binary_expr(expr, expr.op0(), op);
+    }
+    expr.type() = bool_typet{};
+    return std::move(expr);
+  }
   else
   {
     // type is guessed for now
