1，system functions

$onehot (<expression>) returns true if only one bit of the expression is high--獨熱碼
$onehot0(<expression>) returns true if at most one bit of the expression is high--最多有1bit為高
$isunknown (<expression>) returns true if any bit of the expression is X or Z. This is equivalent to ^<expression> === ’bx.--是否為未知態

2，property

A property defines a behavior of the design. A property can be used for verification as an assumption, a checker, or a coverage specification. In order to use the behavior for verification, an assert, assume or cover statement must be used. A property declaration by itself does not produce any result.
屬性定義了design的行為。屬性可以作為假設、檢查器或覆蓋率規範用於驗證。為了使用行為進行驗證，必須使用ASSERT、ASSET或COVER語句。屬性宣告本身不會產生任何結果。
 

example1:

// Reuseable property to check that a signal is in a safe state
property SIGNAL_VALID(signal);
  @(posedge PCLK)
  !$isunknown(signal);
endproperty: SIGNAL_VALID

RESET_VALID: assert property(SIGNAL_VALID(PRESETn));
PSEL_VALID: assert property(SIGNAL_VALID(PSEL));

在波形上可以看到x態。

在log中可以看到assert報錯的資訊

3，sampled value functions

$sampled(expression [, clocking_event])
$rose( expression [, clocking_event]) 
$fell( expression [, clocking_event]) 
$stable( expression [, clocking_event]) 
$past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])

其中，detect changes in sampled values的3個方法如下：

$rose returns true if the least significant bit of the expression changed to 1. Otherwise, it returns false.
$fell returns true if the least significant bit of the expression changed to 0. Otherwise, it returns false. 
$stable returns true if the value of the expression did not change. Otherwise, it returns false.

$sampled返回上次取樣到的值，描述如下：

Function $sampled returns the sampled value of the expression with respect to the last occurrence of the clocking event. When $sampled is invoked prior to the occurrence of the first clocking event, the value of X is returned. The use of $sampled in assertions, although allowed, is redundant, as the result of the function is identical to the sampled value of the expression itself used in the assertion

$past返回上次的採用值，example如下：

$past can be used in any System Verilog expression. An example is shown below.
always @(posedge clk) 
　　reg1 <= a & $past(b);
In this example, the clocking event (posedge clk) is applied to $past. $past is evaluated in the current occurrence of (posedge clk), and returns the value of b sampled at the previous occurrence of (posedge clk).

4，Two forms of implication are provided: overlapped using operator |->, and non-overlapped using operator |=>

For overlapped implication, if there is a match for the antecedent sequence_expr, then the end point of the match is the start point of the evaluation of the consequent property_expr.
For non-overlapped implication, the start point of the evaluation of the consequent property_expr is the clock tick after the end point of the match. 
Therefore:
sequence_expr |=> property_expr
is equivalent to: 
sequence_expr ##1 ‘true |-> property_expr---##1表示等待一個時鐘週期

example：

property data_end; 
    @(posedge mclk) 
    data_phase |-> ((irdy==0) && ($fell(trdy) || $fell(stop))) ;
endproperty

data_phase在clock tick 2時滿足條件，立即開始檢測後面的條件是否滿足，irdy在tick 4時滿足，stop在tick 6時滿足。

5，Repetition in sequences

Three kinds of repetition are provided

---consecutive repetition ( [* ): Consecutive repetition specifies finitely many iterative matches of the operand sequence,
with a delay of one clock tick from the end of one match to the beginning of the next.
The overall repetition sequence matches at the end of the last iterative match of the operand.

example:

(a[*0:3] ##1 b ##1 c) 
is equivalent to
   (b ##1 c) 
or (a ##1 b ##1 c) 
or (a ##1 a ##1 b ##1 c) 
or (a ##1 a ##1 a ##1 b ##1 c)

To specify a finite, but unbounded, number of iterations, the dollar sign ( $ ) is used. For example, the repetition:
a ##1 b [*1:$] ##1 c
matches over an interval of three or more consecutive clock ticks if a is true on the first clock tick,
c is true on the last clock tick, and b is true at every clock tick strictly in between the first and the last.

— goto repetition ( [-> ): Goto repetition specifies finitely many iterative matches of the operand boolean expression, 
with a delay of one or more clock ticks from one match of the operand to the next successive match and no match of the operand strictly in between.
The overall repetition sequence matches at the last iterative match of the operand.

example:

a ##1 b [->2:10] ##1 c
matches over an interval of consecutive clock ticks provided a is true on the first clock tick, c is true on the last clock tick, 
b is true on the penultimate clock tick, and, including the penultimate, there are at least 2 and at most 10 not-necessarily-consecutive
clock ticks strictly in between the first and last on which b is true. This sequence is equivalent to:
a ##1 ((!b[*0:$] ##1 b) [*2:10]) ##1 c

— non-consecutive repetition ( [= ): Non-consecutive repetition specifies finitely many iterative matches of the operand boolean expression,
with a delay of one or more clock ticks from one match of the operand to the next successive match and no match of the operand strictly in 
between. The overall repetition sequence matches at or after the last iterative match of the operand, but before any later match of the operand.

example:

a ##1 b [=2:10] ##1 c
matches over an interval of consecutive clock ticks provided a is true on the first clock tick, c is true on the last clock tick, 
and there are at least 2 and at most 10 not-necessarily-consecutive clock ticks strictly in between the first and last on which b is true. 
This sequence is equivalent to:
a ##1 ((!b [*0:$] ##1 b) [*2:10]) ##1 !b[*0:$] ##1 c