From 42e80b010f3f1c853483ff5894962c8e70c6436d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 14 Nov 2024 09:51:44 +0000 Subject: [PATCH] SystemVerilog: set membership operator This adds the set membership operator, 1800-2017 11.4.13. --- CHANGELOG | 1 + regression/verilog/expressions/inside1.desc | 13 ++++ regression/verilog/expressions/inside1.sv | 10 +++ src/hw_cbmc_irep_ids.h | 2 + src/verilog/expr2verilog.cpp | 68 ++++++++++++++++++++ src/verilog/expr2verilog_class.h | 6 +- src/verilog/parser.y | 16 +++++ src/verilog/verilog_expr.cpp | 51 +++++++++++++++ src/verilog/verilog_expr.h | 69 ++++++++++++++++++++- src/verilog/verilog_synthesis.cpp | 6 ++ src/verilog/verilog_typecheck_expr.cpp | 18 ++++++ 11 files changed, 258 insertions(+), 2 deletions(-) create mode 100644 regression/verilog/expressions/inside1.desc create mode 100644 regression/verilog/expressions/inside1.sv diff --git a/CHANGELOG b/CHANGELOG index dc60b0654..f7505385d 100644 --- 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 new file mode 100644 index 000000000..790697973 --- /dev/null +++ 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 new file mode 100644 index 000000000..f9d7819dd --- /dev/null +++ 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 index 589ba4563..b9da54976 100644 --- 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 index 462e87aaf..0f0bd86aa 100644 --- 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 index 3e6cb3b1b..63a0e1f95 100644 --- 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 index d001ff5e6..8def3f65b 100644 --- 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 index 258e7f6fd..6ff6b0aaf 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -15,6 +15,18 @@ Author: Daniel Kroening, kroening@kroening.com #include #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 index 36b3823b0..83e6cb4a9 100644 --- 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(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(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(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(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(expr); +} + #endif diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index e87cd9185..0b489b052 100644 --- 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 index befab2870..df419ceca 100644 --- 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