diff --git a/src/verilog.l b/src/verilog.l index 7793e2205..2672729f1 100644 --- a/src/verilog.l +++ b/src/verilog.l @@ -593,28 +593,28 @@ vnum {vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5} /* SystemVerilog 2009 */ { /* Keywords */ - "accept_on" { ERROR_RSVD_WORD("SystemVerilog 2009"); } + "accept_on" { FL; return yACCEPT_ON; } "checker" { FL; return yCHECKER; } "endchecker" { FL; return yENDCHECKER; } - "eventually" { ERROR_RSVD_WORD("SystemVerilog 2009"); } + "eventually" { FL; return yEVENTUALLY; } "global" { FL; return yGLOBAL__LEX; } - "implies" { ERROR_RSVD_WORD("SystemVerilog 2009"); } + "implies" { FL; return yIMPLIES; } "let" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "nexttime" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "reject_on" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "s_always" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "s_eventually" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "s_nexttime" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "s_until" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "s_until_with" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "strong" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "sync_accept_on" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "sync_reject_on" { ERROR_RSVD_WORD("SystemVerilog 2009"); } + "nexttime" { FL; return yNEXTTIME; } + "reject_on" { FL; return yREJECT_ON; } + "s_always" { FL; return yS_ALWAYS; } + "s_eventually" { FL; return yS_EVENTUALLY; } + "s_nexttime" { FL; return yS_NEXTTIME; } + "s_until" { FL; return yS_UNTIL; } + "s_until_with" { FL; return yS_UNTIL_WITH; } + "strong" { FL; return ySTRONG; } + "sync_accept_on" { FL; return ySYNC_ACCEPT_ON; } + "sync_reject_on" { FL; return ySYNC_REJECT_ON; } "unique0" { FL; return yUNIQUE0; } - "until" { ERROR_RSVD_WORD("SystemVerilog 2009"); } - "until_with" { ERROR_RSVD_WORD("SystemVerilog 2009"); } + "until" { FL; return yUNTIL; } + "until_with" { FL; return yUNTIL_WITH; } "untyped" { FL; return yUNTYPED; } - "weak" { ERROR_RSVD_WORD("SystemVerilog 2009"); } + "weak" { FL; return yWEAK; } } /* System Verilog 2012 */ @@ -875,6 +875,8 @@ vnum {vnum1}|{vnum2}|{vnum3}|{vnum4}|{vnum5} ">>>=" { FL; return yP_SSRIGHTEQ; } "->>" { FL; return yP_MINUSGTGT; } "##" { FL; return yP_POUNDPOUND; } + "#-#" { FL; return yP_POUNDMINUSPD; } + "#=#" { FL; return yP_POUNDEQPD; } "@@" { FL; return yP_ATAT; } "::" { FL; return yP_COLONCOLON; } ":=" { FL; return yP_COLONEQ; } diff --git a/src/verilog.y b/src/verilog.y index 854136a24..f7057328f 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -536,7 +536,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) // Double underscores "yX__Y" means token X followed by Y, // and "yX__ETC" means X folled by everything but Y(s). %token ya1STEP "1step" -//UNSUP %token yACCEPT_ON "accept_on" +%token yACCEPT_ON "accept_on" %token yALIAS "alias" %token yALWAYS "always" %token yALWAYS_COMB "always_comb" @@ -606,7 +606,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token yENDTASK "endtask" %token yENUM "enum" %token yEVENT "event" -//UNSUP %token yEVENTUALLY "eventually" +%token yEVENTUALLY "eventually" //UNSUP %token yEXPECT "expect" %token yEXPORT "export" %token yEXTENDS "extends" @@ -635,7 +635,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) //UNSUP %token yIGNORE_BINS "ignore_bins" //UNSUP %token yILLEGAL_BINS "illegal_bins" %token yIMPLEMENTS "implements" -//UNSUP %token yIMPLIES "implies" +%token yIMPLIES "implies" %token yIMPORT "import" %token yINITIAL "initial" %token yINOUT "inout" @@ -665,7 +665,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token yNEW__ETC "new" %token yNEW__LEX "new-in-lex" %token yNEW__PAREN "new-then-paren" -//UNSUP %token yNEXTTIME "nexttime" +%token yNEXTTIME "nexttime" %token yNMOS "nmos" %token yNOR "nor" %token yNOT "not" @@ -699,7 +699,7 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token yREALTIME "realtime" %token yREF "ref" %token yREG "reg" -//UNSUP %token yREJECT_ON "reject_on" +%token yREJECT_ON "reject_on" %token yRELEASE "release" %token yREPEAT "repeat" %token yRESTRICT "restrict" @@ -729,13 +729,13 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token ySUPER "super" %token ySUPPLY0 "supply0" %token ySUPPLY1 "supply1" -//UNSUP %token ySYNC_ACCEPT_ON "sync_accept_on" -//UNSUP %token ySYNC_REJECT_ON "sync_reject_on" -//UNSUP %token yS_ALWAYS "s_always" -//UNSUP %token yS_EVENTUALLY "s_eventually" -//UNSUP %token yS_NEXTTIME "s_nexttime" -//UNSUP %token yS_UNTIL "s_until" -//UNSUP %token yS_UNTIL_WITH "s_until_with" +%token ySYNC_ACCEPT_ON "sync_accept_on" +%token ySYNC_REJECT_ON "sync_reject_on" +%token yS_ALWAYS "s_always" +%token yS_EVENTUALLY "s_eventually" +%token yS_NEXTTIME "s_nexttime" +%token yS_UNTIL "s_until" +%token yS_UNTIL_WITH "s_until_with" %token yTABLE "table" //UNSUP %token yTAGGED "tagged" %token yTASK "task" @@ -765,8 +765,8 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token yUNIQUE "unique" %token yUNIQUE0 "unique0" %token yUNSIGNED "unsigned" -//UNSUP %token yUNTIL "until" -//UNSUP %token yUNTIL_WITH "until_with" +%token yUNTIL "until" +%token yUNTIL_WITH "until_with" %token yUNTYPED "untyped" %token yVAR "var" %token yVECTORED "vectored" @@ -1017,8 +1017,8 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) %token yP_ASTGT "*>" %token yP_ANDANDAND "&&&" %token yP_POUNDPOUND "##" -//UNSUP %token yP_POUNDMINUSPD "#-#" -//UNSUP %token yP_POUNDEQPD "#=#" +%token yP_POUNDMINUSPD "#-#" +%token yP_POUNDEQPD "#=#" %token yP_DOTSTAR ".*" %token yP_ATAT "@@" @@ -1068,15 +1068,14 @@ BISONPRE_VERSION(3.7,%define api.header.include {"V3ParseBison.h"}) // Lowest precedence // These are in IEEE 17.7.1 -//UNSUP %nonassoc yALWAYS yS_ALWAYS yEVENTUALLY yS_EVENTUALLY yACCEPT_ON yREJECT_ON ySYNC_ACCEPT_ON ySYNC_REJECT_ON +%nonassoc yALWAYS yS_ALWAYS yEVENTUALLY yS_EVENTUALLY yACCEPT_ON yREJECT_ON ySYNC_ACCEPT_ON ySYNC_REJECT_ON -%right yP_ORMINUSGT yP_OREQGT -//UNSUP %right yP_ORMINUSGT yP_OREQGT yP_POUNDMINUSPD yP_POUNDEQPD -//UNSUP %right yUNTIL yS_UNTIL yUNTIL_WITH yS_UNTIL_WITH yIMPLIES +%right yP_ORMINUSGT yP_OREQGT yP_POUNDMINUSPD yP_POUNDEQPD +%right yUNTIL yS_UNTIL yUNTIL_WITH yS_UNTIL_WITH yIMPLIES //UNSUP %right yIFF //UNSUP %left yOR //UNSUP %left yAND -//UNSUP %nonassoc yNOT yNEXTTIME yS_NEXTTIME +%nonassoc yNOT yNEXTTIME yS_NEXTTIME //UNSUP %left yINTERSECT //UNSUP %left yWITHIN //UNSUP %right yTHROUGHOUT @@ -6017,29 +6016,52 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex // // IEEE-2012: yIF and yCASE //UNSUP property_statementCaseIf { } // - //UNSUP ~o~pexpr/*sexpr*/ yP_POUNDMINUSPD pexpr { } - //UNSUP ~o~pexpr/*sexpr*/ yP_POUNDEQPD pexpr { } - //UNSUP yNEXTTIME pexpr { } - //UNSUP yS_NEXTTIME pexpr { } - //UNSUP yNEXTTIME '[' expr/*const*/ ']' pexpr %prec yNEXTTIME { } - //UNSUP yS_NEXTTIME '[' expr/*const*/ ']' pexpr %prec yS_NEXTTIME { } - //UNSUP yALWAYS pexpr { } - //UNSUP yALWAYS '[' cycle_delay_const_range_expression ']' pexpr %prec yALWAYS { } - //UNSUP yS_ALWAYS '[' constant_range ']' pexpr %prec yS_ALWAYS { } - //UNSUP yS_EVENTUALLY pexpr { } - //UNSUP yEVENTUALLY '[' constant_range ']' pexpr %prec yEVENTUALLY { } - //UNSUP yS_EVENTUALLY '[' cycle_delay_const_range_expression ']' pexpr %prec yS_EVENTUALLY { } - //UNSUP ~o~pexpr yUNTIL pexpr { } - //UNSUP ~o~pexpr yS_UNTIL pexpr { } - //UNSUP ~o~pexpr yUNTIL_WITH pexpr { } - //UNSUP ~o~pexpr yS_UNTIL_WITH pexpr { } - //UNSUP ~o~pexpr yIMPLIES pexpr { } + | ~o~pexpr/*sexpr*/ yP_POUNDMINUSPD pexpr + { $$ = $3; BBUNSUP($2, "Unsupported: #-# (in property expression)"); } + | ~o~pexpr/*sexpr*/ yP_POUNDEQPD pexpr + { $$ = $3; BBUNSUP($2, "Unsupported: #=# (in property expression)"); } + | yNEXTTIME pexpr + { $$ = $2; BBUNSUP($1, "Unsupported: nexttime (in property expression)"); } + | yS_NEXTTIME pexpr + { $$ = $2; BBUNSUP($1, "Unsupported: s_nexttime (in property expression)"); } + | yNEXTTIME '[' constExpr ']' pexpr %prec yNEXTTIME + { $$ = $5; BBUNSUP($1, "Unsupported: nexttime[] (in property expression)"); } + | yS_NEXTTIME '[' constExpr ']' pexpr %prec yS_NEXTTIME + { $$ = $5; BBUNSUP($1, "Unsupported: s_nexttime[] (in property expression)"); } + | yALWAYS pexpr + { $$ = $2; BBUNSUP($1, "Unsupported: always (in property expression)"); } + | yALWAYS anyrange pexpr %prec yALWAYS + { $$ = $3; BBUNSUP($1, "Unsupported: always[] (in property expression)"); } + | yS_ALWAYS anyrange pexpr %prec yS_ALWAYS + { $$ = $3; BBUNSUP($1, "Unsupported: s_always (in property expression)"); } + | yEVENTUALLY pexpr + { $$ = $2; BBUNSUP($1, "Unsupported: eventually (in property expression)"); } + | yS_EVENTUALLY pexpr + { $$ = $2; BBUNSUP($1, "Unsupported: s_eventually (in property expression)"); } + | yEVENTUALLY '[' constExpr ']' pexpr %prec yEVENTUALLY + { $$ = $5; BBUNSUP($1, "Unsupported: eventually[] (in property expression)"); } + | yS_EVENTUALLY anyrange pexpr %prec yS_EVENTUALLY + { $$ = $3; BBUNSUP($1, "Unsupported: s_eventually[] (in property expression)"); } + | ~o~pexpr yUNTIL pexpr + { $$ = $1; BBUNSUP($2, "Unsupported: until (in property expression)"); } + | ~o~pexpr yS_UNTIL pexpr + { $$ = $1; BBUNSUP($2, "Unsupported: s_until (in property expression)"); } + | ~o~pexpr yUNTIL_WITH pexpr + { $$ = $1; BBUNSUP($2, "Unsupported: until_with (in property expression)"); } + | ~o~pexpr yS_UNTIL_WITH pexpr + { $$ = $1; BBUNSUP($2, "Unsupported: s_until_with (in property expression)"); } + | ~o~pexpr yIMPLIES pexpr + { $$ = $1; BBUNSUP($2, "Unsupported: implies (in property expression)"); } // // yIFF also used by event_expression //UNSUP ~o~pexpr yIFF ~o~pexpr { } - //UNSUP yACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yACCEPT_ON { } - //UNSUP yREJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yREJECT_ON { } - //UNSUP ySYNC_ACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_ACCEPT_ON { } - //UNSUP ySYNC_REJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_REJECT_ON { } + | yACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yACCEPT_ON + { $$ = $5; BBUNSUP($2, "Unsupported: accept_on (in property expression)"); } + | yREJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yREJECT_ON + { $$ = $5; BBUNSUP($2, "Unsupported: reject_on (in property expression)"); } + | ySYNC_ACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_ACCEPT_ON + { $$ = $5; BBUNSUP($2, "Unsupported: sync_accept_on (in property expression)"); } + | ySYNC_REJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec ySYNC_REJECT_ON + { $$ = $5; BBUNSUP($2, "Unsupported: sync_reject_on (in property expression)"); } // // // IEEE: "property_instance" // // Looks just like a function/method call @@ -6114,7 +6136,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg //UNSUP // // UNSUP: This causes a big grammer ambiguity //UNSUP // // as ()'s mismatch between primary and the following statement //UNSUP // // the sv-ac committee has been asked to clarify (Mantis 1901) -//UNSUP | yP_POUNDPOUND '[' cycle_delay_const_range_expression ']' { } +//UNSUP | yP_POUNDPOUND anyrange { } //UNSUP | yP_POUNDPOUND yP_BRASTAR ']' { } //UNSUP | yP_POUNDPOUND yP_BRAPLUSKET { } //UNSUP ; @@ -6145,7 +6167,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg //UNSUPconst_or_range_expression: // ==IEEE: const_or_range_expression //UNSUP constExpr { $$ = $1; } -//UNSUP | cycle_delay_const_range_expression { } +//UNSUP | cycle_delay_const_range_expression { } // Use anyrange removing [] instead //UNSUP ; //UNSUPconstant_range: // ==IEEE: constant_range diff --git a/test_regress/t/t_assert_property_pexpr_unsup.out b/test_regress/t/t_assert_property_pexpr_unsup.out new file mode 100644 index 000000000..64a7f1351 --- /dev/null +++ b/test_regress/t/t_assert_property_pexpr_unsup.out @@ -0,0 +1,92 @@ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:24:13: Unsupported: strong (in property expression) + 24 | strong(a); + | ^ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:28:11: Unsupported: weak (in property expression) + 28 | weak(a); + | ^ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:32:9: Unsupported: until (in property expression) + 32 | a until b; + | ^~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:36:9: Unsupported: s_until (in property expression) + 36 | a s_until b; + | ^~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:40:9: Unsupported: until_with (in property expression) + 40 | a until_with b; + | ^~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:44:9: Unsupported: s_until_with (in property expression) + 44 | a s_until_with b; + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:48:9: Unsupported: implies (in property expression) + 48 | a implies b; + | ^~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:52:9: Unsupported: #-# (in property expression) + 52 | a #-# b; + | ^~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:56:9: Unsupported: #=# (in property expression) + 56 | a #=# b; + | ^~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:60:7: Unsupported: nexttime (in property expression) + 60 | nexttime a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:64:7: Unsupported: nexttime[] (in property expression) + 64 | nexttime [2] a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:68:7: Unsupported: s_nexttime (in property expression) + 68 | s_nexttime a; + | ^~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:72:7: Unsupported: s_nexttime[] (in property expression) + 72 | s_nexttime [2] a; + | ^~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:76:16: Unsupported: always (in property expression) + 76 | nexttime always a; + | ^~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:76:7: Unsupported: nexttime (in property expression) + 76 | nexttime always a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:80:20: Unsupported: always (in property expression) + 80 | nexttime [2] always a; + | ^~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:80:7: Unsupported: nexttime[] (in property expression) + 80 | nexttime [2] always a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:84:16: Unsupported: eventually (in property expression) + 84 | nexttime eventually a; + | ^~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:84:7: Unsupported: nexttime (in property expression) + 84 | nexttime eventually a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:88:20: Unsupported: always (in property expression) + 88 | nexttime [2] always a; + | ^~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:88:7: Unsupported: nexttime[] (in property expression) + 88 | nexttime [2] always a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:92:16: Unsupported: s_eventually (in property expression) + 92 | nexttime s_eventually a; + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:92:7: Unsupported: nexttime (in property expression) + 92 | nexttime s_eventually a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:96:35: Unsupported: always (in property expression) + 96 | nexttime s_eventually [2:$] always a; + | ^~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:96:16: Unsupported: s_eventually[] (in property expression) + 96 | nexttime s_eventually [2:$] always a; + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:96:7: Unsupported: nexttime (in property expression) + 96 | nexttime s_eventually [2:$] always a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:100:17: Unsupported: accept_on (in property expression) + 100 | accept_on (a) b; + | ^ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:104:22: Unsupported: sync_accept_on (in property expression) + 104 | sync_accept_on (a) b; + | ^ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:108:17: Unsupported: reject_on (in property expression) + 108 | reject_on (a) b; + | ^ +%Error-UNSUPPORTED: t/t_assert_property_pexpr_unsup.v:112:22: Unsupported: sync_reject_on (in property expression) + 112 | sync_reject_on (a) b; + | ^ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_property_pexpr_unsup.pl b/test_regress/t/t_assert_property_pexpr_unsup.pl new file mode 100755 index 000000000..d188a4276 --- /dev/null +++ b/test_regress/t/t_assert_property_pexpr_unsup.pl @@ -0,0 +1,20 @@ +#!/usr/bin/env perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2022 by Wilson Snyder. This program is free software; you +# can redistribute it and/or modify it under the terms of either the GNU +# Lesser General Public License Version 3 or the Perl Artistic License +# Version 2.0. +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +scenarios(vlt => 1); + +compile( + expect_filename => $Self->{golden_filename}, + verilator_flags2 => ['--assert'], + fails => 1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_assert_property_pexpr_unsup.v b/test_regress/t/t_assert_property_pexpr_unsup.v new file mode 100644 index 000000000..45a0897e5 --- /dev/null +++ b/test_regress/t/t_assert_property_pexpr_unsup.v @@ -0,0 +1,121 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2023 by Wilson Snyder. +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + // Inputs + clk, a, b + ); + + input clk; + int a; + int b; + int cyc = 0; + + always @(posedge clk) begin + cyc <= cyc + 1; + end + + // NOTE this grammar hasn't been checked with other simulators, + // is here just to avoid uncovered code lines in the grammar. + property p_strong; + strong(a); + endproperty + + property p_weak; + weak(a); + endproperty + + property p_until; + a until b; + endproperty + + property p_suntil; + a s_until b; + endproperty + + property p_untilwith; + a until_with b; + endproperty + + property p_suntilwith; + a s_until_with b; + endproperty + + property p_implies; + a implies b; + endproperty + + property p_poundminuspound1; + a #-# b; + endproperty + + property p_poundeqpound; + a #=# b; + endproperty + + property p_nexttime; + nexttime a; + endproperty + + property p_nexttime2; + nexttime [2] a; + endproperty + + property p_snexttime; + s_nexttime a; + endproperty + + property p_snexttime2; + s_nexttime [2] a; + endproperty + + property p_nexttime_always; + nexttime always a; + endproperty + + property p_nexttime_always2; + nexttime [2] always a; + endproperty + + property p_nexttime_eventually; + nexttime eventually a; + endproperty + + property p_nexttime_eventually2; + nexttime [2] always a; + endproperty + + property p_nexttime_seventually; + nexttime s_eventually a; + endproperty + + property p_nexttime_seventually2; + nexttime s_eventually [2:$] always a; + endproperty + + property p_accepton; + accept_on (a) b; + endproperty + + property p_syncaccepton; + sync_accept_on (a) b; + endproperty + + property p_rejecton; + reject_on (a) b; + endproperty + + property p_syncrejecton; + sync_reject_on (a) b; + endproperty + + always @(posedge clk) begin + if (cyc == 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule