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

The SVA operators 'and' and 'or' can be used to form SVA sequences or SVA
properties, depending on the types of the operands.  Furthermore, any
sequence expression is also a property expression.

This results in a conflict in the SystemVerilog grammar, as the context is
insufficient to determine whether an expression is a sequence_expr or a
property_expr.

This resolves the conflict by replicating the sequence_expr rules into
property_expr, and allowing property_expr to be used where sequence_expr
would be required.

To detect malformed input programs that use a property where a sequence is
required, a check is added to the type checker.

Author: kroening

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 &);