diff --git a/regression/verilog/SVA/sequence_followed_by1.desc b/regression/verilog/SVA/sequence_followed_by1.desc new file mode 100644 index 000000000..1869986d8 --- /dev/null +++ b/regression/verilog/SVA/sequence_followed_by1.desc @@ -0,0 +1,10 @@ +CORE +sequence_followed_by1.sv +--bound 20 --numbered-trace +^\[main\.property\.1\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$ +^\[main\.property\.2\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/sequence_followed_by1.sv b/regression/verilog/SVA/sequence_followed_by1.sv new file mode 100644 index 000000000..677796ebd --- /dev/null +++ b/regression/verilog/SVA/sequence_followed_by1.sv @@ -0,0 +1,12 @@ +module main(input clk); + + reg [31:0] x = 0; + + always @(posedge clk) + x<=x+1; + + initial p0: assert property (x == 0 #=# x == 1 #=# x == 2); + + initial p0: assert property (x == 0 #-# ##1 x == 1 #-# ##1 x == 2); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 0fe928fd5..57f614765 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -36,6 +36,8 @@ IREP_ID_ONE(sva_until) IREP_ID_ONE(sva_s_until) IREP_ID_ONE(sva_until_with) IREP_ID_ONE(sva_s_until_with) +IREP_ID_ONE(sva_overlapped_followed_by) +IREP_ID_ONE(sva_nonoverlapped_followed_by) IREP_ID_ONE(sva_overlapped_implication) IREP_ID_ONE(sva_non_overlapped_implication) IREP_ID_ONE(module_instance) diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index a45a195df..eea42fa0d 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -20,7 +20,9 @@ bool is_temporal_operator(const exprt &expr) expr.id() == ID_sva_until || expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually || - expr.id() == ID_sva_cycle_delay; + expr.id() == ID_sva_cycle_delay || + expr.id() == ID_sva_overlapped_followed_by || + expr.id() == ID_sva_nonoverlapped_followed_by; } bool has_temporal_operator(const exprt &expr) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 9d9296fcb..8b16c721f 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1141,6 +1141,12 @@ std::string expr2verilogt::convert( else if(src.id() == ID_sva_cycle_delay_plus) return convert_sva_unary("##[+]", to_unary_expr(src)); + else if(src.id() == ID_sva_overlapped_followed_by) + return precedence = 0, convert_sva_binary("#-#", to_binary_expr(src)); + + else if(src.id() == ID_sva_nonoverlapped_followed_by) + return precedence = 0, convert_sva_binary("#=#", to_binary_expr(src)); + else if(src.id()==ID_sva_cycle_delay) return convert_sva_cycle_delay(to_ternary_expr(src), precedence = 0); // not sure about precedence diff --git a/src/verilog/parser.y b/src/verilog/parser.y index e2a90456e..8010aa63c 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -372,6 +372,8 @@ int yyverilogerror(const char *error) %token TOK_LESSLESSLESSEQUAL "<<<=" %token TOK_GREATERGREATERGREATEREQUAL ">>>=" %token TOK_HASHHASH "##" +%token TOK_HASHMINUSHASH "#-#" +%token TOK_HASHEQUALHASH "#=#" %token TOK_COLONCOLON "::" /* System Verilog Keywords */ @@ -2059,6 +2061,8 @@ 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); } + | sequence_expr "#-#" property_expr { init($$, ID_sva_overlapped_followed_by); mto($$, $1); mto($$, $3); } + | sequence_expr "#=#" property_expr { init($$, ID_sva_nonoverlapped_followed_by); mto($$, $1); mto($$, $3); } | "nexttime" property_expr { init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); } | "nexttime" '[' constant_expression ']' property_expr %prec "nexttime" diff --git a/src/verilog/scanner.l b/src/verilog/scanner.l index 138f91b1a..5ba14c604 100644 --- a/src/verilog/scanner.l +++ b/src/verilog/scanner.l @@ -258,6 +258,8 @@ void verilog_scanner_init() "<<<=" { SYSTEM_VERILOG_OPERATOR(TOK_LESSLESSLESSEQUAL, "<<<="); } ">>>=" { SYSTEM_VERILOG_OPERATOR(TOK_GREATERGREATERGREATEREQUAL, ">>>="); } "##" { SYSTEM_VERILOG_OPERATOR(TOK_HASHHASH, "##"); } +"#-#" { SYSTEM_VERILOG_OPERATOR(TOK_HASHMINUSHASH, "#-#"); } +"#=#" { SYSTEM_VERILOG_OPERATOR(TOK_HASHEQUALHASH, "#=#"); } "<->" { SYSTEM_VERILOG_OPERATOR(TOK_LESSMINUSGREATER, "<->"); } "->" { SYSTEM_VERILOG_OPERATOR(TOK_MINUSGREATER, "->"); } "'" { SYSTEM_VERILOG_OPERATOR('\'', "'"); } diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 12bd75218..38a485757 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2260,12 +2260,13 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) return std::move(expr); } - else if(expr.id()==ID_sva_overlapped_implication || - expr.id()==ID_sva_non_overlapped_implication || - expr.id()==ID_sva_until || - expr.id()==ID_sva_s_until || - expr.id()==ID_sva_until_with || - expr.id()==ID_sva_s_until_with) + else if( + expr.id() == ID_sva_overlapped_implication || + expr.id() == ID_sva_non_overlapped_implication || + expr.id() == ID_sva_overlapped_followed_by || + expr.id() == ID_sva_nonoverlapped_followed_by || + expr.id() == ID_sva_until || expr.id() == ID_sva_s_until || + expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with) { convert_expr(expr.op0()); make_boolean(expr.op0());