Merge pull request #1018 from diffblue/sva-sequence-to-property-parens

SVA: `and`/`or` as a sequence also need to work with parentheses

Author: tautschnig

regression/verilog/SVA/sequence_and1.desc

@@ -5,6 +5,7 @@ sequence_and1.sv
 ^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$
 ^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED up to bound \d+$
 ^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED up to bound \d+$
+^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_and1.sv

@@ -15,4 +15,7 @@ module main(input clk);
   initial p2: assert property (x == 0 and nexttime x == 1);
   initial p3: assert property (nexttime x == 1 and x == 0);
 
+  // It also yields a sequence when in parentheses.
+  initial p4: assert property ((x == 0 and x != 10) |=> x == 1);
+
 endmodule

regression/verilog/SVA/sequence_first_match2.desc

@@ -1,9 +1,9 @@
 CORE
 sequence_first_match2.sv
 --bound 5
-^\[.*\] \(##1 1\) or \(\(##2 1\) \|-> main.x == 1\): PROVED up to bound 5$
+^\[.*\] \(\(##1 1\) or \(##2 1\)\) \|-> main.x == 1: PROVED up to bound 5$
 ^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED up to bound 5$
-^\[.*\] 1 or \(\(##1 1\) \|-> main\.x == 0\): PROVED up to bound 5$
+^\[.*\] \(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
 ^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$
 ^EXIT=0$
 ^SIGNAL=0$

regression/verilog/SVA/sequence_implication2.desc

@@ -0,0 +1,8 @@
+CORE
+sequence_implication2.sv
+--module main
+^file .* line 4: sequence required$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/sequence_implication2.sv

@@ -0,0 +1,6 @@
+module main(input clk);
+
+  // The RHS must be a sequence
+  assert property (@(posedge clk) (always 1) |-> 1);
+
+endmodule : main

regression/verilog/SVA/sequence_or1.desc

@@ -5,6 +5,7 @@ sequence_or1.sv
 ^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
 ^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED up to bound \d+$
 ^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED up to bound \d+$
+^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence_or1.sv

@@ -15,4 +15,7 @@ module main(input clk);
   initial p2: assert property (x==0 or nexttime x == 1);
   initial p3: assert property (nexttime x==1 or x == 1);
 
+  // It also yields a sequence when in parentheses.
+  initial p4: assert property ((x == 0 or x != 10) |=> x == 1);
+
 endmodule

src/temporal-logic/normalize_property.cpp

@@ -24,7 +24,7 @@ exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
   // Same as a->always[1:1] b if lhs is not a sequence.
-  if(!is_SVA_sequence(expr.lhs()))
+  if(!is_SVA_sequence_operator(expr.lhs()))
   {
     auto one = natural_typet{}.one_expr();
     return or_exprt{

src/temporal-logic/temporal_logic.cpp

@@ -92,7 +92,7 @@ bool is_LTL_past(const exprt &expr)
   return !has_subexpr(expr, non_LTL_past_operator);
 }
 
-bool is_SVA_sequence(const exprt &expr)
+bool is_SVA_sequence_operator(const exprt &expr)
 {
   auto id = expr.id();
   // Note that ID_sva_overlapped_followed_by and ID_sva_nonoverlapped_followed_by
@@ -114,7 +114,7 @@ bool is_SVA_sequence(const exprt &expr)
 bool is_SVA_operator(const exprt &expr)
 {
   auto id = expr.id();
-  return is_SVA_sequence(expr) || id == ID_sva_disable_iff ||
+  return is_SVA_sequence_operator(expr) || id == ID_sva_disable_iff ||
          id == ID_sva_accept_on || id == ID_sva_reject_on ||
          id == ID_sva_sync_accept_on || id == ID_sva_sync_reject_on ||
          id == ID_sva_always || id == ID_sva_s_always ||

src/temporal-logic/temporal_logic.h

@@ -54,7 +54,7 @@ bool is_LTL_operator(const exprt &);
 bool is_LTL_past_operator(const exprt &);
 
 /// Returns true iff the given expression is an SVA sequence expression
-bool is_SVA_sequence(const exprt &);
+bool is_SVA_sequence_operator(const exprt &);
 
 /// Returns true iff the given expression is an SVA temporal operator
 bool is_SVA_operator(const exprt &);