diff --git a/regression/verilog/SVA/nexttime1.desc b/regression/verilog/SVA/nexttime1.desc new file mode 100644 index 000000000..29f289e1c --- /dev/null +++ b/regression/verilog/SVA/nexttime1.desc @@ -0,0 +1,12 @@ +KNOWNBUG +nexttime1.sv +--module main --bound 10 +^\[main\.property\.1\] s_nexttime\[0\] main\.counter == 0: PROVED up to bound 10$ +^\[main\.property\.2\] s_nexttime\[1\] main\.counter == 1: PROVED up to bound 10$ +^\[main\.property\.3\] nexttime\[8\] main\.counter == 8: PROVED up to bound 10$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Backend support missing. diff --git a/regression/verilog/SVA/nexttime1.sv b/regression/verilog/SVA/nexttime1.sv new file mode 100644 index 000000000..0e80bbdd3 --- /dev/null +++ b/regression/verilog/SVA/nexttime1.sv @@ -0,0 +1,23 @@ +module main(input clk); + + // count up from 0 to 10 + reg [7:0] counter; + + initial counter = 0; + + always @(posedge clk) + if(counter == 10) + counter = 0; + else + counter = counter + 1; + + // expected to pass + initial p1: assert property (s_nexttime[0] counter == 0); + + // expected to pass + initial p2: assert property (s_nexttime[1] counter == 1); + + // expected to pass + initial p3: assert property (nexttime[8] counter == 8); + +endmodule diff --git a/src/temporal-logic/negate_property.cpp b/src/temporal-logic/negate_property.cpp index d0e3de540..f5a56feeb 100644 --- a/src/temporal-logic/negate_property.cpp +++ b/src/temporal-logic/negate_property.cpp @@ -93,7 +93,7 @@ exprt negate_property(const exprt &expr) } else if(expr.id() == ID_sva_nexttime) { - unary_exprt result = to_sva_nexttime_expr(expr); + auto result = to_sva_nexttime_expr(expr); result.op() = negate_property(result.op()); return std::move(result); } diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 32f2f9351..11084db4c 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -112,9 +112,15 @@ exprt normalize_property(exprt expr) expr = normalize_pre_sva_non_overlapped_implication( to_sva_non_overlapped_implication_expr(expr)); else if(expr.id() == ID_sva_nexttime) - expr = X_exprt{to_sva_nexttime_expr(expr).op()}; + { + if(!to_sva_nexttime_expr(expr).is_indexed()) + expr = X_exprt{to_sva_nexttime_expr(expr).op()}; + } else if(expr.id() == ID_sva_s_nexttime) - expr = X_exprt{to_sva_s_nexttime_expr(expr).op()}; + { + if(!to_sva_s_nexttime_expr(expr).is_indexed()) + expr = X_exprt{to_sva_s_nexttime_expr(expr).op()}; + } else if(expr.id() == ID_sva_cycle_delay) expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr)); else if(expr.id() == ID_sva_cycle_delay_plus) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index b3de1d4ac..9d9296fcb 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -430,7 +430,7 @@ std::string expr2verilogt::convert_sva_unary( /*******************************************************************\ -Function: expr2verilogt::convert_sva +Function: expr2verilogt::convert_sva_binary Inputs: @@ -459,6 +459,35 @@ std::string expr2verilogt::convert_sva_binary( /*******************************************************************\ +Function: expr2verilogt::convert_sva_indexed_binary + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::string expr2verilogt::convert_sva_indexed_binary( + const std::string &name, + const binary_exprt &expr) +{ + std::string s0; + + if(expr.op0().is_not_nil()) + s0 = '[' + convert(expr.lhs()) + ']'; + + unsigned p1; + auto s1 = convert(expr.rhs(), p1); + if(p1 == 0) + s1 = "(" + s1 + ")"; + + return name + s0 + ' ' + s1; +} + +/*******************************************************************\ + Function: expr2verilogt::convert_replication Inputs: @@ -1161,11 +1190,11 @@ std::string expr2verilogt::convert( else if(src.id()==ID_sva_nexttime) return precedence = 0, - convert_sva_unary("nexttime", to_sva_nexttime_expr(src)); + convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src)); else if(src.id()==ID_sva_s_nexttime) - return precedence = 0, - convert_sva_unary("s_nexttime", to_sva_s_nexttime_expr(src)); + return precedence = 0, convert_sva_indexed_binary( + "s_nexttime", to_sva_s_nexttime_expr(src)); else if(src.id()==ID_sva_eventually) { diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index cacedd09a..ab62b14a0 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -92,6 +92,9 @@ class expr2verilogt std::string convert_sva_binary(const std::string &name, const binary_exprt &); + std::string + convert_sva_indexed_binary(const std::string &name, const binary_exprt &); + virtual std::string convert_replication(const replication_exprt &, unsigned precedence); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 85b867512..e2a90456e 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2059,11 +2059,18 @@ property_expr_proper: | property_expr "and" property_expr { init($$, ID_and); mto($$, $1); mto($$, $3); } | property_expr "|->" property_expr { init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); } | property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); } - | "nexttime" property_expr { init($$, "sva_nexttime"); mto($$, $2); } - | "s_nexttime" property_expr { init($$, "sva_s_nexttime"); mto($$, $2); } + | "nexttime" property_expr + { init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); } + | "nexttime" '[' constant_expression ']' property_expr %prec "nexttime" + { init($$, "sva_nexttime"); mto($$, $3); mto($$, $5); } + | "s_nexttime" property_expr + { init($$, "sva_s_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); } + | "s_nexttime" '[' constant_expression ']' property_expr %prec "s_nexttime" + { init($$, "sva_s_nexttime"); mto($$, $3); mto($$, $5); } | "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always" { init($$, ID_sva_ranged_always); swapop($$, $3); mto($$, $5); } - | "always" property_expr { init($$, "sva_always"); mto($$, $2); } + | "always" property_expr + { init($$, "sva_always"); mto($$, $2); } | "s_always" '[' constant_range ']' property_expr %prec "s_always" { init($$, ID_sva_s_always); swapop($$, $3); mto($$, $5); } | "s_eventually" property_expr diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index d490c31cc..6ce914555 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -11,13 +11,43 @@ Author: Daniel Kroening, kroening@kroening.com #include -class sva_nexttime_exprt : public unary_predicate_exprt +class sva_nexttime_exprt : public binary_predicate_exprt { public: + // nonindexed variant explicit sva_nexttime_exprt(exprt op) - : unary_predicate_exprt(ID_sva_nexttime, std::move(op)) + : binary_predicate_exprt(nil_exprt(), ID_sva_nexttime, std::move(op)) { } + + bool is_indexed() const + { + return index().is_not_nil(); + } + + const exprt &index() const + { + return op0(); + } + + exprt &index() + { + return op0(); + } + + const exprt &op() const + { + return op1(); + } + + exprt &op() + { + return op1(); + } + +protected: + using binary_predicate_exprt::op0; + using binary_predicate_exprt::op1; }; static inline const sva_nexttime_exprt &to_sva_nexttime_expr(const exprt &expr) @@ -34,13 +64,43 @@ static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr) return static_cast(expr); } -class sva_s_nexttime_exprt : public unary_predicate_exprt +class sva_s_nexttime_exprt : public binary_predicate_exprt { public: + // nonindexed variant explicit sva_s_nexttime_exprt(exprt op) - : unary_predicate_exprt(ID_sva_s_nexttime, std::move(op)) + : binary_predicate_exprt(nil_exprt(), ID_sva_s_nexttime, std::move(op)) { } + + bool is_indexed() const + { + return index().is_not_nil(); + } + + const exprt &index() const + { + return op0(); + } + + exprt &index() + { + return op0(); + } + + const exprt &op() const + { + return op1(); + } + + exprt &op() + { + return op1(); + } + +protected: + using binary_predicate_exprt::op0; + using binary_predicate_exprt::op1; }; static inline const sva_s_nexttime_exprt & diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index e1040e4ce..12bd75218 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1905,8 +1905,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) expr.type() = expr.op().type(); } else if( - expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime || - expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_s_eventually || + expr.id() == ID_sva_always || expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay_plus || expr.id() == ID_sva_cycle_delay_star) { @@ -2237,6 +2236,30 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) return std::move(expr); } + else if(expr.id() == ID_sva_nexttime) + { + if(to_sva_nexttime_expr(expr).is_indexed()) + convert_expr(to_sva_nexttime_expr(expr).index()); + + auto &op = to_sva_nexttime_expr(expr).op(); + convert_expr(op); + make_boolean(op); + expr.type() = bool_typet(); + + return std::move(expr); + } + else if(expr.id() == ID_sva_s_nexttime) + { + if(to_sva_s_nexttime_expr(expr).is_indexed()) + convert_expr(to_sva_s_nexttime_expr(expr).index()); + + auto &op = to_sva_s_nexttime_expr(expr).op(); + convert_expr(op); + make_boolean(op); + expr.type() = bool_typet(); + + return std::move(expr); + } else if(expr.id()==ID_sva_overlapped_implication || expr.id()==ID_sva_non_overlapped_implication || expr.id()==ID_sva_until ||