From 469806ca15c7aba8e002bde30afb58b558161af1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 19 Jun 2025 15:16:16 +0900 Subject: [PATCH] SVA: parentheses around the arguments of ## This adds parentheses around the arguments of SVA ## to avoid ambiguity. --- .../sva-buechi/sequence_repetition5.desc | 4 +- regression/verilog/SVA/empty_sequence1.desc | 2 +- .../verilog/SVA/sequence_repetition5.desc | 4 +- src/verilog/expr2verilog.cpp | 59 ++++++++----------- src/verilog/expr2verilog_class.h | 6 +- 5 files changed, 33 insertions(+), 42 deletions(-) diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc index b7d763a47..560a7442d 100644 --- a/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition5.desc @@ -1,8 +1,8 @@ CORE ../../verilog/SVA/sequence_repetition5.sv --buechi --bound 20 -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$ -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:9\]\) ##1 main.pulse: PROVED up to bound 20$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:8\]\) ##1 main.pulse: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/empty_sequence1.desc b/regression/verilog/SVA/empty_sequence1.desc index 7aaba5f11..cbb56dc0a 100644 --- a/regression/verilog/SVA/empty_sequence1.desc +++ b/regression/verilog/SVA/empty_sequence1.desc @@ -2,7 +2,7 @@ CORE empty_sequence1.sv --bound 5 ^\[main\.p0\] 1 \[\*0\]: REFUTED$ -^\[main\.p1\] 1 \[\*0\] ##1 main\.x == 0: REFUTED$ +^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/sequence_repetition5.desc b/regression/verilog/SVA/sequence_repetition5.desc index aa6cf0982..5e4c94893 100644 --- a/regression/verilog/SVA/sequence_repetition5.desc +++ b/regression/verilog/SVA/sequence_repetition5.desc @@ -1,8 +1,8 @@ CORE sequence_repetition5.sv --bound 20 -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$ -^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:9\]\) ##1 main.pulse: PROVED up to bound 20$ +^\[.*\] main\.pulse ##1 \(\!main\.pulse \[\*1:8\]\) ##1 main.pulse: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index d31d92f73..8c6149a5d 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -141,9 +141,8 @@ Function: expr2verilogt::convert_sva_cycle_delay \*******************************************************************/ -expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay( - const sva_cycle_delay_exprt &src, - verilog_precedencet precedence) +expr2verilogt::resultt +expr2verilogt::convert_sva_cycle_delay(const sva_cycle_delay_exprt &src) { std::string dest="##"; @@ -163,13 +162,13 @@ expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay( auto rhs = convert_rec(src.rhs()); - if(precedence > rhs.p) + if(rhs.p == verilog_precedencet::MIN) dest += '('; dest += rhs.s; - if(precedence > rhs.p) + if(rhs.p == verilog_precedencet::MIN) dest += ')'; - return {precedence, dest}; + return {verilog_precedencet::MIN, dest}; } /*******************************************************************\ @@ -224,33 +223,41 @@ Function: expr2verilogt::convert_sva_sequence_concatenation \*******************************************************************/ -expr2verilogt::resultt expr2verilogt::convert_sva_sequence_concatenation( - const binary_exprt &src, - verilog_precedencet precedence) +expr2verilogt::resultt +expr2verilogt::convert_sva_sequence_concatenation(const binary_exprt &src) { - if(src.operands().size()!=2) - return convert_norep(src); - std::string dest; auto op0 = convert_rec(src.op0()); auto op1 = convert_rec(src.op1()); - if(precedence > op0.p) + bool lhs_paren = op0.p == verilog_precedencet::MIN && + src.op0().id() != ID_sva_sequence_concatenation && + src.op0().id() != ID_sva_cycle_delay && + src.op0().id() != ID_sva_cycle_delay_plus && + src.op0().id() != ID_sva_cycle_delay_star; + + if(lhs_paren) dest += '('; dest += op0.s; - if(precedence > op0.p) + if(lhs_paren) dest += ')'; dest+=' '; - if(precedence > op0.p) + bool rhs_paren = op1.p == verilog_precedencet::MIN && + src.op1().id() != ID_sva_sequence_concatenation && + src.op1().id() != ID_sva_cycle_delay && + src.op1().id() != ID_sva_cycle_delay_plus && + src.op1().id() != ID_sva_cycle_delay_star; + + if(rhs_paren) dest += '('; dest += op1.s; - if(precedence > op0.p) + if(rhs_paren) dest += ')'; - return {precedence, dest}; + return {verilog_precedencet::MIN, dest}; } /*******************************************************************\ @@ -1838,9 +1845,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) convert_sva_binary("#=#", to_binary_expr(src)); else if(src.id()==ID_sva_cycle_delay) - return convert_sva_cycle_delay( - to_sva_cycle_delay_expr(src), precedence = verilog_precedencet::MIN); - // not sure about precedence + return convert_sva_cycle_delay(to_sva_cycle_delay_expr(src)); else if(src.id() == ID_sva_strong) return convert_function("strong", src); @@ -1862,9 +1867,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) } else if(src.id()==ID_sva_sequence_concatenation) - return convert_sva_sequence_concatenation( - to_binary_expr(src), precedence = verilog_precedencet::MIN); - // not sure about precedence + return convert_sva_sequence_concatenation(to_binary_expr(src)); else if(src.id() == ID_sva_sequence_first_match) return convert_sva_sequence_first_match( @@ -1885,16 +1888,6 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) 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); - // not sure about precedence - - else if(src.id() == ID_sva_sequence_throughout) - return convert_sva_sequence_concatenation( - to_binary_expr(src), precedence = verilog_precedencet::MIN); - // not sure about precedence - else if(src.id()==ID_sva_always) return precedence = verilog_precedencet::MIN, convert_sva_unary("always", to_sva_always_expr(src)); diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 32ac685a0..3e249abef 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -156,13 +156,11 @@ class expr2verilogt resultt convert_with(const with_exprt &, verilog_precedencet); - resultt - convert_sva_cycle_delay(const sva_cycle_delay_exprt &, verilog_precedencet); + resultt convert_sva_cycle_delay(const sva_cycle_delay_exprt &); resultt convert_sva_if(const sva_if_exprt &); - resultt - convert_sva_sequence_concatenation(const binary_exprt &, verilog_precedencet); + resultt convert_sva_sequence_concatenation(const binary_exprt &); resultt convert_sva_sequence_first_match(const sva_sequence_first_match_exprt &);