SVA: sequence 'and'/'or' vs. property 'and'/'or'

The 1800-2017 SystemVerilog grammar allows "a and b" and "a or b" to be
either a sequence, or a property.  If both "a" and "b" are sequences, then
"a and b" and "a or b" is a sequence as well.

This changes the grammar to allow the sequence case.

Author: kroening

regression/verilog/SVA/sequence_and1.desc

@@ -1,9 +1,12 @@
-KNOWNBUG
+CORE
 sequence_and1.sv
 
-^EXIT=0$
+^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$
+^\[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+$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The grammar for 'SVA sequence and' is missing.

regression/verilog/SVA/sequence_and1.sv

@@ -9,6 +9,10 @@ module main(input clk);
   initial p0: assert property (x == 0 and x == 1);
 
   // Given two sequences, 'and' yields a sequence, not a property
-  initial p1: assert property ((x == 0 and x == 1)[*1]);
+  initial p1: assert property (strong(x == 0 and x == 1));
+
+  // But given a property on either side, 'and' yields a property
+  initial p2: assert property (x == 0 and nexttime x == 1);
+  initial p3: assert property (nexttime x == 1 and x == 0);
 
 endmodule

regression/verilog/SVA/sequence_or1.desc

@@ -1,9 +1,12 @@
-KNOWNBUG
+CORE
 sequence_or1.sv
 
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED up to bound \d+$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED up to bound \d+$
+^\[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+$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The grammar for 'SVA sequence or' is missing.

regression/verilog/SVA/sequence_or1.sv

@@ -9,6 +9,10 @@ module main(input clk);
   initial p0: assert property (x == 0 or x == 1);
 
   // Given two sequences, 'or' yields a sequence, not a property
-  initial p1: assert property ((x == 0 or x == 1)[*1]);
+  initial p1: assert property (strong(x == 0 or x == 1));
+
+  // But given a property on either side, 'or' yields a property
+  initial p2: assert property (x==0 or nexttime x == 1);
+  initial p3: assert property (nexttime x==1 or x == 1);
 
 endmodule

src/verilog/parser.y

@@ -554,6 +554,10 @@ int yyverilogerror(const char *error)
 // whereas the table gives them in decreasing order.
 // The precendence of the assertion operators is lower than
 // those in Table 11-2.
+//
+// SEQUENCE_TO_PROPERTY is an artificial token to give
+// the right precedence to the conversion of a sequence_expr
+// to a property_expr.
 %nonassoc "property_expr_abort" // accept_on, reject_on, ...
 %nonassoc "property_expr_clocking_event" // @(...) property_expr
 %nonassoc "always" "s_always" "eventually" "s_eventually"
@@ -564,6 +568,7 @@ int yyverilogerror(const char *error)
 %right "iff"
 %left "or"
 %left "and"
+%nonassoc SEQUENCE_TO_PROPERTY
 %nonassoc "not" "nexttime" "s_nexttime"
 %left "intersect"
 %left "within"
@@ -2419,7 +2424,7 @@ sequence_formal_type:
 // for property_expr into property_expr and property_expr_proper.
 
 property_expr:
-	  sequence_expr
+	  sequence_expr %prec SEQUENCE_TO_PROPERTY
 	| property_expr_proper
 	;
 
@@ -2577,8 +2582,12 @@ sequence_expr_proper:
 		  // preserve the operand ordering as in the source code
 		  stack_expr($$).operands().insert(stack_expr($$).operands().begin(), stack_expr($1));
 		}
+	| sequence_expr "and" sequence_expr
+		{ init($$, ID_sva_and); mto($$, $1); mto($$, $3); }
 	| sequence_expr "intersect" sequence_expr
                 { init($$, ID_sva_sequence_intersect); mto($$, $1); mto($$, $3); }
+	| sequence_expr "or" sequence_expr
+		{ init($$, ID_sva_or); mto($$, $1); mto($$, $3); }
         | "first_match" '(' sequence_expr ')'
                 { init($$, ID_sva_sequence_first_match); mto($$, $3); }
         | "first_match" '(' sequence_expr ',' sequence_match_item_brace ')'