Assertion

断言：用来与设计功能和时序作比较的属性描述。
立即断言：

assert (expression) [pass_statement] [else fail_statement]
always @(posedge clk) if (state == REQ)assert(reg1 || reg2)else begint=$time;#5 $error("assert failed at time %0t", t);endassert (myfunc(a,b)) count1 count+1; else -> event1;assert (y==0) else flag == 1;always @(state)assert (state == $onehot) else $fatal;

并行断言

assert property (cont_prop(rst,in1,in2)) pass_stat else fail_stat;property name；
...
endpropertyassert property name else ...;sequence name;endsequence

并行断言只会在时钟边沿激活，变量的值是采样到的值。

sequence、property和assertion

assertion可以直接包含一个property；
assertion可以独立声明property；
在property内部可以有条件地关闭： disable iff （）
property可以直接包含sequence，也可独立声明多个sequence。
sequence是用来表示一个或多个时钟周期内的时序描述；
sequence可以提供形式参数；

sequence s20_1(data, en);(!frame && (data == data_bus)) ##1 (c_be[0:3] == en);
endsequence

|-> ：条件满足，在当前周期评估其后算子；
|=> ：条件满足，在下一周期评估其后算子；
## ：周期延迟，##0指当前周期
##[min:max] ： 在一个范围内的时钟周期延迟，从min到max时间窗口中最早的时间来匹配。
$ ： 表示无穷大的周期。a ## [1:$]b。
[*n] ： 表示重复，重复连续的时钟周期。
[*m:n] ： 在一定范围内重复的事件。
[=m] ： 重复m次，不需要在连续周期内发生。
[=m:n] ： 从最小到最大重复发生的非连续周期次数。
[*0] ： 表示没有在任何正数时钟周期内有效。

and : 同一个起始点开始，seq1和seq2均满足，满足时刻发生在较晚序列的满足时刻。
intersect ： 同一起点，同一结束点；
or: seq1 和 seq2在同一时刻被触发，结束时间以序列满足的最后一个序列时间为准。
first_match：选择第一次匹配的时刻。
throughout ：检查一个信号或者表达式在贯穿一个序列时是否满足。sig1/exp2 throughout seq;在seq成立期间sig1/exp2成立，左边包含右边。
within：一个序列与另一个序列部分周期长度上的重叠。一个序列包含在另一个序列内。seq1 within seq2：seq2的起始点早于q1的起始点，seq2的结束点晚于等于seq1的结束点。
if...else：在sequence中使用if ..else
seq.end :检测序列的终点。
局部变量：

sequence t2;(a##[2:3] b) or (c ##[1:2] d);
endsequence
sequence ts2;first_match(t2);
endsequence

sequence checkBusIdle;(##[2:$] (frame && irdy));
endsequence
property first_match_idle@(posedge clk) first_match(checkBusIdle) |-> (state==busidle);
endproperty

//局部变量
sequence check_reg_wr_data;int local_data;(rd_cache_done, local_data=cache_rd_data) ##2 (reg_wr_data == (local_data+1)
endsequenceproperty checkreadidack;int loc_id;($rose(read),loc_id = readid) |=>not(($rose(read)&&readid==loc_id)[*1:$]) ##0($rose(readack)&&readackid ==loc_id);
endproperty

访问采样方法
访问当前周期采样值，访问上一周期采样值；检测采样值的变化。
$rose:
$fell:
$stabel(expression[,clocking_event]),连续两个周期内表达式的值保持不变
$past(expr[,numble_cycles][,gating_expr][,clocking_event])访问在过去若干采样周期前的数值。

disble iff 给assertion做局部的条件控制。

property name@(posedge clk) disable iff (!rst)...
endproperty