diff --git a/regression/verilog/SVA/sequence_first_match1.desc b/regression/verilog/SVA/sequence_first_match1.desc index 6460064f0..731f0ef5b 100644 --- a/regression/verilog/SVA/sequence_first_match1.desc +++ b/regression/verilog/SVA/sequence_first_match1.desc @@ -1,8 +1,8 @@ CORE sequence_first_match1.sv -^file .* line \d+: no support for 'first_match'$ -^EXIT=2$ +^\[.*\] first_match\(main\.x == 0\): FAILURE: property not supported by BMC engine$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/verilog/SVA/sequence_intersect1.desc b/regression/verilog/SVA/sequence_intersect1.desc index 43bdf903c..33e5b5cf4 100644 --- a/regression/verilog/SVA/sequence_intersect1.desc +++ b/regression/verilog/SVA/sequence_intersect1.desc @@ -1,8 +1,8 @@ CORE sequence_intersect1.sv -^file .* line \d+: no support for 'intersect'$ -^EXIT=2$ +^\[.*\] main\.x == 0 intersect main\.x == 1: FAILURE: property not supported by BMC engine$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/verilog/SVA/sequence_repetition1.desc b/regression/verilog/SVA/sequence_repetition1.desc index 250ee8177..938c543e0 100644 --- a/regression/verilog/SVA/sequence_repetition1.desc +++ b/regression/verilog/SVA/sequence_repetition1.desc @@ -1,6 +1,12 @@ -KNOWNBUG +CORE sequence_repetition1.sv --bound 10 +^\[.*\] 1 \[\*\] main\.half_x == 0: FAILURE: property not supported by BMC engine$ +^\[.*\] 1 \[->\] main\.half_x == 0: FAILURE: property not supported by BMC engine$ +^\[.*\] 1 \[=\] main\.half_x == 0: FAILURE: property not supported by BMC engine$ +^\[.*\] 1 \[\*\] main\.x == 0: FAILURE: property not supported by BMC engine$ +^\[.*\] 1 \[->\] main\.x == 0: FAILURE: property not supported by BMC engine$ +^\[.*\] 1 \[=\] main\.x == 0: FAILURE: property not supported by BMC engine$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/sequence_repetition2.desc b/regression/verilog/SVA/sequence_repetition2.desc new file mode 100644 index 000000000..858f0eb44 --- /dev/null +++ b/regression/verilog/SVA/sequence_repetition2.desc @@ -0,0 +1,15 @@ +CORE +sequence_repetition2.sv +--bound 10 +^\[main\.p0\] main\.x == 0\[\*\]: FAILURE: property not supported by BMC engine$ +^\[main\.p1\] main\.x == 1\[\*\]: FAILURE: property not supported by BMC engine$ +^\[main\.p2\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: FAILURE: property not supported by BMC engine$ +^\[main\.p3\] main\.x == 0\[\+\]: FAILURE: property not supported by BMC engine$ +^\[main\.p4\] main\.half_x == 0\[\*\]: FAILURE: property not supported by BMC engine$ +^\[main\.p5\] main\.x == 1\[\+\]: FAILURE: property not supported by BMC engine$ +^\[main\.p6\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: FAILURE: property not supported by BMC engine$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/sequence_repetition2.sv b/regression/verilog/SVA/sequence_repetition2.sv new file mode 100644 index 000000000..fbae5fadc --- /dev/null +++ b/regression/verilog/SVA/sequence_repetition2.sv @@ -0,0 +1,23 @@ +module main(input clk); + + reg [31:0] x = 0; + + // 0 1 2 3 4 ... + always_ff @(posedge clk) + x<=x+1; + + // 0 0 1 1 2 2 3 3 ... + wire [31:0] half_x = x/2; + + // should pass + initial p0: assert property (x==0[*]); + initial p1: assert property (x==1[*]); + initial p2: assert property (x==0[+] #-# x==1); + initial p3: assert property (x==0[+]); + initial p4: assert property (half_x==0[*]); + + // should fail + initial p5: assert property (x==1[+]); + initial p6: assert property (x==0[+] #=# x==1); + +endmodule diff --git a/regression/verilog/SVA/sequence_throughout1.desc b/regression/verilog/SVA/sequence_throughout1.desc index 14cd79449..230bcb0e0 100644 --- a/regression/verilog/SVA/sequence_throughout1.desc +++ b/regression/verilog/SVA/sequence_throughout1.desc @@ -1,8 +1,8 @@ CORE sequence_throughout1.sv -^file .* line \d+: no support for 'throughout'$ -^EXIT=2$ +^\[.*\] main\.x == 0 throughout main\.x == 1: FAILURE: property not supported by BMC engine$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/verilog/SVA/sequence_within1.desc b/regression/verilog/SVA/sequence_within1.desc index 04bdc5828..dc58d4062 100644 --- a/regression/verilog/SVA/sequence_within1.desc +++ b/regression/verilog/SVA/sequence_within1.desc @@ -1,8 +1,8 @@ CORE sequence_within1.sv -^file .* line \d+: no support for 'within'$ -^EXIT=2$ +^\[.*\] main\.x == 0 within main\.x == 1: FAILURE: property not supported by BMC engine$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index e34065a60..b3c7e50fa 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -74,7 +74,12 @@ bool is_SVA_sequence(const exprt &expr) id == ID_sva_non_overlapped_implication || id == ID_sva_cycle_delay || id == ID_sva_sequence_concatenation || id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match || - id == ID_sva_sequence_throughout || id == ID_sva_sequence_within; + id == ID_sva_sequence_throughout || id == ID_sva_sequence_within || + id == ID_sva_sequence_goto_repetition || + id == ID_sva_sequence_consecutive_repetition || + id == ID_sva_sequence_non_consecutive_repetition || + id == ID_sva_sequence_repetition_star || + id == ID_sva_sequence_repetition_plus; } bool is_SVA_operator(const exprt &expr) diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 2ad9ca817..60d6d87e9 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -110,6 +110,42 @@ Function: bmc_supports_SVA_property bool bmc_supports_SVA_property(const exprt &expr) { + // sva_sequence_first_match is not supported yet + if(has_subexpr(expr, ID_sva_sequence_first_match)) + return false; + + // sva_sequence_troughout is not supported yet + if(has_subexpr(expr, ID_sva_sequence_throughout)) + return false; + + // sva_sequence_intersect is not supported yet + if(has_subexpr(expr, ID_sva_sequence_intersect)) + return false; + + // sva_sequence_within is not supported yet + if(has_subexpr(expr, ID_sva_sequence_within)) + return false; + + // sva_sequence_repetition_plus is not supported yet + if(has_subexpr(expr, ID_sva_sequence_repetition_plus)) + return false; + + // sva_sequence_repetition_star is not supported yet + if(has_subexpr(expr, ID_sva_sequence_repetition_star)) + return false; + + // sva_sequence_non_consecutive_repetition is not supported yet + if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition)) + return false; + + // sva_sequence_consecutive_repetition is not supported yet + if(has_subexpr(expr, ID_sva_sequence_consecutive_repetition)) + return false; + + // sva_sequence_goto_repetition is not supported yet + if(has_subexpr(expr, ID_sva_sequence_goto_repetition)) + return false; + return true; } diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 29caf5089..acf6a4da6 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -453,6 +453,28 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary( /*******************************************************************\ +Function: expr2verilogt::convert_sva_unary + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +expr2verilogt::resultt expr2verilogt::convert_sva_unary( + const unary_exprt &src, + const std::string &name) +{ + auto op = convert_rec(src.op()); + if(op.p == verilog_precedencet::MIN && src.op().operands().size() >= 2) + op.s = "(" + op.s + ")"; + return {verilog_precedencet::MIN, op.s + name}; +} + +/*******************************************************************\ + Function: expr2verilogt::convert_sva_binary Inputs: @@ -1446,6 +1468,16 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) convert_sva_binary("intersect", to_binary_expr(src)); // not sure about precedence + else if(src.id() == ID_sva_sequence_throughout) + return precedence = verilog_precedencet::MIN, + convert_sva_binary("throughout", to_binary_expr(src)); + // not sure about precedence + + else if(src.id() == ID_sva_sequence_within) + return precedence = verilog_precedencet::MIN, + convert_sva_binary("within", to_binary_expr(src)); + // not sure about precedence + else if(src.id() == ID_sva_sequence_within) return convert_sva_sequence_concatenation( to_binary_expr(src), precedence = verilog_precedencet::MIN); @@ -1460,6 +1492,31 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) return precedence = verilog_precedencet::MIN, convert_sva_unary("always", to_sva_always_expr(src)); + else if(src.id() == ID_sva_sequence_repetition_star) + return precedence = verilog_precedencet::MIN, + convert_sva_unary(to_unary_expr(src), "[*]"); + // not sure about precedence + + else if(src.id() == ID_sva_sequence_repetition_plus) + return precedence = verilog_precedencet::MIN, + convert_sva_unary(to_unary_expr(src), "[+]"); + // not sure about precedence + + else if(src.id() == ID_sva_sequence_non_consecutive_repetition) + return precedence = verilog_precedencet::MIN, + convert_sva_binary("[=]", to_binary_expr(src)); + // not sure about precedence + + else if(src.id() == ID_sva_sequence_consecutive_repetition) + return precedence = verilog_precedencet::MIN, + convert_sva_binary("[*]", to_binary_expr(src)); + // not sure about precedence + + else if(src.id() == ID_sva_sequence_goto_repetition) + return precedence = verilog_precedencet::MIN, + convert_sva_binary("[->]", to_binary_expr(src)); + // not sure about precedence + else if(src.id() == ID_sva_ranged_always) { return precedence = verilog_precedencet::MIN, diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index ea3eabab8..f86e17fdc 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -120,6 +120,8 @@ class expr2verilogt resultt convert_sva_unary(const std::string &name, const unary_exprt &); + resultt convert_sva_unary(const unary_exprt &, const std::string &name); + resultt convert_sva_binary(const std::string &name, const binary_exprt &); resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &); diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index ca4919698..f8aaabec5 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2465,27 +2465,15 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) expr.id() == ID_sva_cycle_delay_plus || expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak || expr.id() == ID_sva_strong || expr.id() == ID_sva_nexttime || - expr.id() == ID_sva_s_nexttime) + expr.id() == ID_sva_s_nexttime || + expr.id() == ID_sva_sequence_first_match || + expr.id() == ID_sva_sequence_repetition_plus || + expr.id() == ID_sva_sequence_repetition_star) { convert_expr(expr.op()); make_boolean(expr.op()); expr.type()=bool_typet(); } - else if(expr.id() == ID_sva_sequence_first_match) - { - throw errort().with_location(expr.source_location()) - << "no support for 'first_match'"; - } - else if(expr.id() == ID_sva_sequence_repetition_plus) - { - throw errort().with_location(expr.source_location()) - << "currently no support for [+]"; - } - else if(expr.id() == ID_sva_sequence_repetition_star) - { - throw errort().with_location(expr.source_location()) - << "currently no support for [*]"; - } else if(expr.id() == ID_verilog_explicit_cast) { // SystemVerilog has got type'(expr). This is an explicit @@ -2959,20 +2947,24 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) return std::move(expr); } - else if(expr.id() == ID_sva_sequence_intersect) - { - throw errort().with_location(expr.source_location()) - << "no support for 'intersect'"; - } - else if(expr.id() == ID_sva_sequence_throughout) - { - throw errort().with_location(expr.source_location()) - << "no support for 'throughout'"; - } - else if(expr.id() == ID_sva_sequence_within) + else if( + expr.id() == ID_sva_sequence_intersect || + expr.id() == ID_sva_sequence_throughout || + expr.id() == ID_sva_sequence_within || + expr.id() == ID_sva_sequence_non_consecutive_repetition || + expr.id() == ID_sva_sequence_consecutive_repetition || + expr.id() == ID_sva_sequence_goto_repetition) { - throw errort().with_location(expr.source_location()) - << "no support for 'within'"; + auto &binary_expr = to_binary_expr(expr); + + convert_expr(binary_expr.lhs()); + make_boolean(binary_expr.lhs()); + convert_expr(binary_expr.rhs()); + make_boolean(binary_expr.rhs()); + + expr.type() = bool_typet(); + + return std::move(expr); } else if(expr.id()==ID_hierarchical_identifier) { @@ -3026,21 +3018,6 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) expr.type() = bool_typet(); return std::move(expr); } - else if(expr.id() == ID_sva_sequence_non_consecutive_repetition) - { - throw errort().with_location(expr.source_location()) - << "currently no support for [=]"; - } - else if(expr.id() == ID_sva_sequence_consecutive_repetition) - { - throw errort().with_location(expr.source_location()) - << "currently no support for [*]"; - } - else if(expr.id() == ID_sva_sequence_goto_repetition) - { - throw errort().with_location(expr.source_location()) - << "currently no support for [->]"; - } else { // type is guessed for now