diff --git a/regression/verilog/SVA/sequence_and1.desc b/regression/verilog/SVA/sequence_and1.desc index 02dcee36..f689eba5 100644 --- a/regression/verilog/SVA/sequence_and1.desc +++ b/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. diff --git a/regression/verilog/SVA/sequence_and1.sv b/regression/verilog/SVA/sequence_and1.sv index f644d874..db45a40f 100644 --- a/regression/verilog/SVA/sequence_and1.sv +++ b/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 diff --git a/regression/verilog/SVA/sequence_or1.desc b/regression/verilog/SVA/sequence_or1.desc index 849973e6..8ad2b106 100644 --- a/regression/verilog/SVA/sequence_or1.desc +++ b/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. diff --git a/regression/verilog/SVA/sequence_or1.sv b/regression/verilog/SVA/sequence_or1.sv index 2a55a244..9bb20a1a 100644 --- a/regression/verilog/SVA/sequence_or1.sv +++ b/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 diff --git a/src/verilog/parser.y b/src/verilog/parser.y index a898a424..eee3af01 100644 --- a/src/verilog/parser.y +++ b/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 ')'