1. 在使用not 这个property operator时，要注意将它局限seqence中，而不要带implication。
2. 如何声明在seqenceA发生的条件下，sequenceB一定不会发生？
seqA|->seqB|->`false 例如：
(a##1b |=> c##1d)|->`false
3. first_match 操作符仅仅匹配拥有多次match可能性的sequence中的第一次。暗含的first_match
1） property仅仅由sequence构成，那么这个sequence等同于 first_match（sequence）
2） property 含有implication，那么consequent sequence等同于 first_match(sequence)
3） seq.ended 也存在多次匹配。
上述暗含first_match是因为，一旦满足了，线程就认为是sucessful 从而退出。
4） 最后也是最重要的： 在antecedent sequence 中不会暗含first_match. （因为只是条件，不是结果）
所以为了防止unexpected failure， antecedent 中需要first_match。
此外为了避免不必要的overlap assertion，要确认触发条件是唯一的，正确使用$rose 或者 $fell. 例如：
first_match($rose(a) ##[2:5]b) |=> c##d;
4. 重复运算符
1）连续重复： seq[*n] 连续出现n次 （间隔##1）
2）非连续重复： seq[=n] 重复出现的次数是n，但是可以不连续。seq xxx seq x seq x seq xx
3）跳转重复（非连续精确重复）: seq[->n], 非连续重复，但是最后一次必须是seq。 如 seq xx seq x seq x seq
5. [*0:m] 的解释
element in the sequence must repeat "0" times (也就是说可以被跳过），或者出现一次，或者连续出现两次。。。连续出现m次。0 让当前时间路径(cycle)成为可选项。
b[*0]##N a 等价于 ##(N-1) a
6. ##[0:$] 的用法
一直等待，直至后续seqence满足，永远不言败。如：
a |-> (##[0:$]##1 c) 如果a 条件满足，一直等到c为高。
7. sequence 组合 运算符
##0 ： sequence fusion
or：sequence disjunction 一个结束，就成功
and： sequence Non-Length-Matching 同时开始，各自结束（不一致）
intersect： sequence Length-Matching 同时开始，同时结束
within： sequence containment 一个包含另一个
throughout： conditions over sequence 重点还是在sequence上，不过附带条件也要满足，例如：
property p_handshake;
@(posedge clk)
$rose(req)|->##[1:4] enable throughout (ack ##[1:$] done);
endproperty
当req起来后，期望1~4个cycle内ack进行响应，并且随后done有效。在ack和done最终有效地期间内，enable保持高电平。
8. sequence 相关的method
1） ended ： endpoint detection 在单时钟的sequence中
2） matched ： endpoint detection 在多时钟的sequence中
3） triggered ： 当sequence结束时的delta cycle内进行扩展，比ended跨度更大（从observe<-->postponed），从而保证不会丢失这个事件。
.ended 返回一个值表明当前cycle sequence是否正好结束，啥时候开始我们不关心。（返回值仅仅花费一个cycle）。注意endpoint不是一个sequence。
例如：
property p_diff_than_prop1;
go|->qReqAck.ended##1done; //qReqAck.ended 只消耗一个cycle，即使go是在qReqAck开始之后有效，也成功
endproperty
利用endpoint 还可以追溯过去。即由结果追溯原因。
sequence qReq;
$rose(req)##3 `true;
endsequence
property pTraceBack
ack|->qReg.ended;
endproperty
在多时钟域下用matched取代ended，达到用destination clock (clkb) synchronize source clock (clka) 驱动下的 seqA.ended.
triggered 有效地防止了竞争以及丢失event， 因为ended不能用于disable iff（...）中，所以triggered是实现ended的不二之选。
主要用法有 ：
1） wait(seqA.triggered)
2） disable iff (seqA.triggered)
9. sequence event ： sequence 也可以表现为一种事件（当结束时刻）
@(seqA) // 等待seqA endpoint
wait(seqA) // 等待 seqA endpoint
