diff --git a/regression/verilog/expressions/wildcard_equality1.desc b/regression/verilog/expressions/wildcard_equality1.desc index 6b64197c3..8124a5547 100644 --- a/regression/verilog/expressions/wildcard_equality1.desc +++ b/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 diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 7b81f6f8a..1fa1c1ba4 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/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) diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.cpp index f51359843..f4e10f416 100644 --- a/src/verilog/aval_bval_encoding.cpp +++ b/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}}; +} diff --git a/src/verilog/aval_bval_encoding.h b/src/verilog/aval_bval_encoding.h index ff5c4894a..4a691390e 100644 --- a/src/verilog/aval_bval_encoding.h +++ b/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 diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 4855c24d5..4f68c607f 100644 --- a/src/verilog/expr2verilog.cpp +++ b/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); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 778ae5530..6e355e293 100644 --- a/src/verilog/parser.y +++ b/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 diff --git a/src/verilog/scanner.l b/src/verilog/scanner.l index b41acb01f..1c51add5d 100644 --- a/src/verilog/scanner.l +++ b/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, "[+"); } diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 8eb144852..fb62cdaa9 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -108,6 +108,50 @@ to_verilog_logical_inequality_expr(exprt &expr) return static_cast(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(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(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(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(expr); +} + class function_call_exprt : public binary_exprt { public: diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index ae60389f6..0af39d168 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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()) diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 05d39be61..90d1bcc4c 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/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) {