SystemVerilog: wildcard equality and inequality

regression/verilog/expressions/wildcard_equality1.desc

@@ -1,7 +1,17 @@
-KNOWNBUG
+CORE broken-smt-backend
 wildcard_equality1.sv
 --bound 0
-^EXIT=0$
+^\[main\.property01\] always 10 ==\? 10 === 1: PROVED up to bound 0$
+^\[main\.property02\] always 10 ==\? 20 === 0: PROVED up to bound 0$
+^\[main\.property03\] always 10 !=\? 20 === 1: PROVED up to bound 0$
+^\[main\.property04\] always 10 ==\? 20 === 0: PROVED up to bound 0$
+^\[main\.property05\] always 2'b00 ==\? 2'b0x === 1: PROVED up to bound 0$
+^\[main\.property06\] always 2'b10 ==\? 2'b0x === 0: PROVED up to bound 0$
+^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED up to bound 0$
+^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED up to bound 0$
+^\[main\.property09\] always 2'b11 ==\? 2'b11 === 0: REFUTED$
+^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED up to bound 0$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/hw_cbmc_irep_ids.h

@@ -66,6 +66,8 @@ IREP_ID_ONE(Verilog)
 IREP_ID_ONE(verilog_assignment_pattern)
 IREP_ID_ONE(verilog_logical_equality)
 IREP_ID_ONE(verilog_logical_inequality)
+IREP_ID_ONE(verilog_wildcard_equality)
+IREP_ID_ONE(verilog_wildcard_inequality)
 IREP_ID_ONE(verilog_explicit_cast)
 IREP_ID_ONE(verilog_size_cast)
 IREP_ID_ONE(verilog_implicit_typecast)

src/verilog/aval_bval_encoding.cpp

@@ -247,3 +247,37 @@ exprt aval_bval(const verilog_logical_inequality_exprt &expr)
   return if_exprt{
     has_xz, make_x(), aval_bval_conversion(equality, lower_to_aval_bval(type))};
 }
+
+exprt aval_bval(const verilog_wildcard_equality_exprt &expr)
+{
+  auto &type = expr.type();
+  PRECONDITION(type.id() == ID_verilog_unsignedbv);
+
+  // We are using masking based on the pattern given as rhs.
+  // The aval is the comparison value, and the
+  // negation of bval is the mask.
+  const auto &pattern_aval = ::aval(expr.rhs());
+  const auto &pattern_bval = ::bval(expr.rhs());
+  auto mask_expr = bitnot_exprt{pattern_bval};
+
+  return equal_exprt{
+    bitand_exprt{aval(expr.lhs()), mask_expr},
+    bitand_exprt{pattern_aval, mask_expr}};
+}
+
+exprt aval_bval(const verilog_wildcard_inequality_exprt &expr)
+{
+  auto &type = expr.type();
+  PRECONDITION(type.id() == ID_verilog_unsignedbv);
+
+  // We are using masking based on the pattern given as rhs.
+  // The aval is the comparison value, and the
+  // negation of bval is the mask.
+  const auto &pattern_aval = ::aval(expr.rhs());
+  const auto &pattern_bval = ::bval(expr.rhs());
+  auto mask_expr = bitnot_exprt{pattern_bval};
+
+  return notequal_exprt{
+    bitand_exprt{aval(expr.lhs()), mask_expr},
+    bitand_exprt{pattern_aval, mask_expr}};
+}

src/verilog/aval_bval_encoding.h

@@ -40,4 +40,9 @@ exprt aval_bval_concatenation(const exprt::operandst &, const typet &);
 exprt aval_bval(const verilog_logical_equality_exprt &);
 exprt aval_bval(const verilog_logical_inequality_exprt &);
 
+/// lowering for ==?
+exprt aval_bval(const verilog_wildcard_equality_exprt &);
+/// lowering for !=?
+exprt aval_bval(const verilog_wildcard_inequality_exprt &);
+
 #endif

src/verilog/expr2verilog.cpp

@@ -1252,6 +1252,18 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
       "!==",
       precedence = verilog_precedencet::EQUALITY);
 
+  else if(src.id() == ID_verilog_wildcard_equality)
+    return convert_binary(
+      to_multi_ary_expr(src),
+      "==?",
+      precedence = verilog_precedencet::EQUALITY);
+
+  else if(src.id() == ID_verilog_wildcard_inequality)
+    return convert_binary(
+      to_multi_ary_expr(src),
+      "!=?",
+      precedence = verilog_precedencet::EQUALITY);
+
   else if(src.id()==ID_not)
     return convert_unary(
       to_not_expr(src), "!", precedence = verilog_precedencet::NOT);

src/verilog/parser.y

@@ -372,32 +372,34 @@ int yyverilogerror(const char *error)
 %token TOK_UWIRE            "uwire"
 
 /* System Verilog Operators */
-%token TOK_VERTBARMINUSGREATER "|->"
-%token TOK_VERTBAREQUALGREATER "|=>"
-%token TOK_PLUSPLUS         "++"
-%token TOK_MINUSMINUS       "--"
-%token TOK_PLUSEQUAL        "+="
-%token TOK_PLUSCOLON        "+:"
-%token TOK_MINUSEQUAL       "-="
-%token TOK_MINUSCOLON       "-:"
-%token TOK_ASTERICEQUAL     "*="
-%token TOK_SLASHEQUAL       "/="
-%token TOK_PERCENTEQUAL     "%="
-%token TOK_AMPEREQUAL       "&="
-%token TOK_CARETEQUAL       "^="
-%token TOK_VERTBAREQUAL     "|="
-%token TOK_LESSLESSEQUAL    "<<="
-%token TOK_GREATERGREATEREQUAL ">>="
-%token TOK_LESSLESSLESSEQUAL "<<<="
+%token TOK_VERTBARMINUSGREATER  "|->"
+%token TOK_VERTBAREQUALGREATER  "|=>"
+%token TOK_PLUSPLUS             "++"
+%token TOK_MINUSMINUS           "--"
+%token TOK_PLUSEQUAL            "+="
+%token TOK_PLUSCOLON            "+:"
+%token TOK_MINUSEQUAL           "-="
+%token TOK_MINUSCOLON           "-:"
+%token TOK_ASTERICEQUAL         "*="
+%token TOK_SLASHEQUAL           "/="
+%token TOK_PERCENTEQUAL         "%="
+%token TOK_AMPEREQUAL           "&="
+%token TOK_CARETEQUAL           "^="
+%token TOK_VERTBAREQUAL         "|="
+%token TOK_LESSLESSEQUAL        "<<="
+%token TOK_GREATERGREATEREQUAL  ">>="
+%token TOK_LESSLESSLESSEQUAL    "<<<="
 %token TOK_GREATERGREATERGREATEREQUAL ">>>="
-%token TOK_HASHHASH         "##"
-%token TOK_HASHMINUSHASH    "#-#"
-%token TOK_HASHEQUALHASH    "#=#"
-%token TOK_COLONCOLON       "::"
-%token TOK_LSQASTERIC       "[*"
-%token TOK_LSQPLUS          "[+"
-%token TOK_LSQEQUAL         "[="
-%token TOK_LSQMINUSGREATER  "[->"
+%token TOK_HASHHASH             "##"
+%token TOK_HASHMINUSHASH        "#-#"
+%token TOK_HASHEQUALHASH        "#=#"
+%token TOK_COLONCOLON           "::"
+%token TOK_EQUALEQUALQUESTION   "==?"
+%token TOK_EXCLAMEQUALQUESTION  "!=?"
+%token TOK_LSQASTERIC           "[*"
+%token TOK_LSQPLUS              "[+"
+%token TOK_LSQEQUAL             "[="
+%token TOK_LSQMINUSGREATER      "[->"
 
 /* System Verilog Keywords */
 %token TOK_ACCEPT_ON        "accept_on"
@@ -3546,6 +3548,10 @@ expression:
 		{ init($$, ID_verilog_logical_equality); mto($$, $1); mto($$, $3); }
 	| expression TOK_EXCLAMEQUAL expression
 		{ init($$, ID_verilog_logical_inequality); mto($$, $1); mto($$, $3); }
+	| expression TOK_EQUALEQUALQUESTION expression
+		{ init($$, ID_verilog_wildcard_equality); mto($$, $1); mto($$, $3); }
+	| expression TOK_EXCLAMEQUALQUESTION expression
+		{ init($$, ID_verilog_wildcard_inequality); mto($$, $1); mto($$, $3); }
 	| expression TOK_EQUALEQUALEQUAL expression
 		{ init($$, ID_verilog_case_equality); mto($$, $1); mto($$, $3); }
 	| expression TOK_EXCLAMEQUALEQUAL expression

src/verilog/scanner.l

@@ -264,6 +264,8 @@ void verilog_scanner_init()
 "->"            { SYSTEM_VERILOG_OPERATOR(TOK_MINUSGREATER, "->"); }
 "'"             { SYSTEM_VERILOG_OPERATOR('\'', "'"); }
 "::"            { SYSTEM_VERILOG_OPERATOR(TOK_COLONCOLON, "::"); }
+"==?"           { SYSTEM_VERILOG_OPERATOR(TOK_EQUALEQUALQUESTION, "==?"); }
+"!=?"           { SYSTEM_VERILOG_OPERATOR(TOK_EXCLAMEQUALQUESTION, "!=?"); }
                 /* Table 16-1 in 1800-2017 suggests the following tokens for sequence operators */
 "[*"            { SYSTEM_VERILOG_OPERATOR(TOK_LSQASTERIC, "[*"); }
 "[+"            { SYSTEM_VERILOG_OPERATOR(TOK_LSQPLUS, "[+"); }

src/verilog/verilog_expr.h

@@ -108,6 +108,50 @@ to_verilog_logical_inequality_expr(exprt &expr)
   return static_cast<verilog_logical_inequality_exprt &>(expr);
 }
 
+/// ==?
+class verilog_wildcard_equality_exprt : public equal_exprt
+{
+public:
+};
+
+inline const verilog_wildcard_equality_exprt &
+to_verilog_wildcard_equality_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_wildcard_equality);
+  binary_exprt::check(expr);
+  return static_cast<const verilog_wildcard_equality_exprt &>(expr);
+}
+
+inline verilog_wildcard_equality_exprt &
+to_verilog_wildcard_equality_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_wildcard_equality);
+  binary_exprt::check(expr);
+  return static_cast<verilog_wildcard_equality_exprt &>(expr);
+}
+
+/// !=?
+class verilog_wildcard_inequality_exprt : public equal_exprt
+{
+public:
+};
+
+inline const verilog_wildcard_inequality_exprt &
+to_verilog_wildcard_inequality_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_wildcard_inequality);
+  binary_exprt::check(expr);
+  return static_cast<const verilog_wildcard_inequality_exprt &>(expr);
+}
+
+inline verilog_wildcard_inequality_exprt &
+to_verilog_wildcard_inequality_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_wildcard_inequality);
+  binary_exprt::check(expr);
+  return static_cast<verilog_wildcard_inequality_exprt &>(expr);
+}
+
 class function_call_exprt : public binary_exprt
 {
 public:

src/verilog/verilog_synthesis.cpp

@@ -402,6 +402,18 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
       op = synth_expr(op, symbol_state);
     return aval_bval(to_verilog_logical_inequality_expr(expr));
   }
+  else if(expr.id() == ID_verilog_wildcard_equality)
+  {
+    for(auto &op : expr.operands())
+      op = synth_expr(op, symbol_state);
+    return aval_bval(to_verilog_wildcard_equality_expr(expr));
+  }
+  else if(expr.id() == ID_verilog_wildcard_inequality)
+  {
+    for(auto &op : expr.operands())
+      op = synth_expr(op, symbol_state);
+    return aval_bval(to_verilog_wildcard_inequality_expr(expr));
+  }
   else if(expr.has_operands())
   {
     for(auto &op : expr.operands())

src/verilog/verilog_typecheck_expr.cpp

@@ -2599,6 +2599,20 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(
+    expr.id() == ID_verilog_wildcard_equality ||
+    expr.id() == ID_verilog_wildcard_inequality)
+  {
+    // ==? and !=?
+    Forall_operands(it, expr)
+      convert_expr(*it);
+
+    tc_binary_expr(expr);
+
+    expr.type() = verilog_unsignedbv_typet(1);
+
+    return std::move(expr);
+  }
   else if(expr.id()==ID_verilog_case_equality ||
           expr.id()==ID_verilog_case_inequality)
   {