From d6e7a431f41f13e89680da08cf0e4d7acfd82d19 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 2 Jun 2024 15:57:07 -0700 Subject: [PATCH] Operators ##[*] and ##[+] This adds the sequence operators ##[*] and ##[+]. --- regression/verilog/SVA/sequence3.sv | 15 +++++++ src/hw_cbmc_irep_ids.h | 2 + src/temporal-logic/normalize_property.cpp | 4 ++ src/temporal-logic/normalize_property.h | 2 + src/verilog/expr2verilog.cpp | 6 +++ src/verilog/parser.y | 4 ++ src/verilog/sva_expr.h | 50 +++++++++++++++++++++++ src/verilog/verilog_typecheck_expr.cpp | 4 +- 8 files changed, 86 insertions(+), 1 deletion(-) create mode 100644 regression/verilog/SVA/sequence3.sv diff --git a/regression/verilog/SVA/sequence3.sv b/regression/verilog/SVA/sequence3.sv new file mode 100644 index 000000000..0d2ce130d --- /dev/null +++ b/regression/verilog/SVA/sequence3.sv @@ -0,0 +1,15 @@ +module main; + + reg [31:0] x; + wire clk; + + initial x=0; + + always @(posedge clk) + if(x < 5) + x<=x+1; + + initial p0: assert property (##[*] x==6); // same as [0:$] + initial p1: assert property (##[+] x==0); // same as [1:$] + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index e1790cbb5..0fe928fd5 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -16,6 +16,8 @@ IREP_ID_ONE(E) IREP_ID_ONE(G) IREP_ID_ONE(X) IREP_ID_ONE(sva_cycle_delay) +IREP_ID_ONE(sva_cycle_delay_star) +IREP_ID_ONE(sva_cycle_delay_plus) IREP_ID_ONE(sva_sequence_concatenation) IREP_ID_ONE(sva_sequence_first_match) IREP_ID_ONE(sva_sequence_intersect) diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 7d2cc7b3a..32f2f9351 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -117,6 +117,10 @@ exprt normalize_property(exprt expr) 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) + expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}}; + else if(expr.id() == ID_sva_cycle_delay_star) + expr = X_exprt{to_sva_cycle_delay_star_expr(expr).op()}; // normalize the operands for(auto &op : expr.operands()) diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h index 05a87b5cb..72e685ae9 100644 --- a/src/temporal-logic/normalize_property.h +++ b/src/temporal-logic/normalize_property.h @@ -24,6 +24,8 @@ Author: Daniel Kroening, dkr@amazon.com /// ¬¬φ --> φ /// ¬Gφ --> F¬φ /// ¬Fφ --> G¬φ +/// [*] φ --> F φ +/// [+] φ --> X F φ exprt normalize_property(exprt); #endif diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 48bdc6955..b3de1d4ac 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1106,6 +1106,12 @@ std::string expr2verilogt::convert( else if(src.id()==ID_sva_non_overlapped_implication) return precedence = 0, convert_sva_binary("|=>", to_binary_expr(src)); + else if(src.id() == ID_sva_cycle_delay_star) + return convert_sva_unary("##[*]", to_unary_expr(src)); + + else if(src.id() == ID_sva_cycle_delay_plus) + return convert_sva_unary("##[+]", to_unary_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 0d0ef8033..85b867512 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2106,6 +2106,10 @@ cycle_delay_range: { init($$, ID_sva_cycle_delay); mto($$, $2); stack_expr($$).operands().push_back(nil_exprt()); } | "##" '[' cycle_delay_const_range_expression ']' { $$ = $3; } + | "##" '[' TOK_ASTERIC ']' + { init($$, ID_sva_cycle_delay_star); } + | "##" '[' TOK_PLUS ']' + { init($$, ID_sva_cycle_delay_plus); } ; cycle_delay_const_range_expression: diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index d52858b43..d490c31cc 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -521,4 +521,54 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr) return static_cast(expr); } +class sva_cycle_delay_plus_exprt : public unary_exprt +{ +public: + explicit sva_cycle_delay_plus_exprt(exprt op) + : unary_exprt(ID_sva_cycle_delay_plus, std::move(op), bool_typet()) + { + } +}; + +static inline const sva_cycle_delay_plus_exprt & +to_sva_cycle_delay_plus_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_cycle_delay_plus); + sva_cycle_delay_plus_exprt::check(expr); + return static_cast(expr); +} + +static inline sva_cycle_delay_plus_exprt & +to_sva_cycle_delay_plus_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_cycle_delay_plus); + sva_cycle_delay_plus_exprt::check(expr); + return static_cast(expr); +} + +class sva_cycle_delay_star_exprt : public unary_exprt +{ +public: + explicit sva_cycle_delay_star_exprt(exprt op) + : unary_exprt(ID_sva_cycle_delay_star, std::move(op), bool_typet()) + { + } +}; + +static inline const sva_cycle_delay_star_exprt & +to_sva_cycle_delay_star_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_cycle_delay_star); + sva_cycle_delay_star_exprt::check(expr); + return static_cast(expr); +} + +static inline sva_cycle_delay_star_exprt & +to_sva_cycle_delay_star_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_cycle_delay_star); + sva_cycle_delay_star_exprt::check(expr); + return static_cast(expr); +} + #endif diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 6acd3f629..e1040e4ce 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1906,7 +1906,9 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) } 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_s_nexttime || expr.id() == ID_sva_s_eventually || + expr.id() == ID_sva_cycle_delay_plus || + expr.id() == ID_sva_cycle_delay_star) { assert(expr.operands().size()==1); convert_expr(expr.op());