篇14-first_match构造/throughout构造/within构造

1.first_match构造

(1) 使用了逻辑运算符（如“and”和“or”）的序列中指定了时间窗，有可能出现同一检验具有多个匹配的情况。“first_match”构造可以确保只用第一次序列匹配，而丢弃其他的匹配。

(2) 当多个序列被组合在一起，其中只需时间窗的第一次匹配来检验属性剩余的部分时，“first_match”构造非常有用。

     在下面的例子中，属性用运算符“or”将两个序列组合在一起。这个属性的几个可能的匹配如下所示。

2.first_match构造实例

3.throughout构造

(1) 蕴含（implication）是目前讨论到的允许定义前提条件的一项技术。例如，要对一个指定的序列进行检验，必须某个前提条件为真。但是蕴含只在时钟沿检验前提条件一次，然后就开始检验后续算子部分，它不检测先行算子是否一直保持为真。

(2) 存在情况:要求在检验序列的整个过程中，某个条件必须一直为真。为了保证某些条件在整个序列的验证过程中一直为真，可以使用“throughout”运算符。

(3) 运算符“throughout”的基本语法如下所示：（expression）throughout （sequence definition）；

4.throughout实例

属性p31检查下列内容：

(1) 在信号“start”的下降沿开始检查。

(2) 检查表达式((!a&&!b)##1(c[->3])##1(a&&b))。

(3) 序列检查在信号“a”和“b”的下降沿与信号“a”和“b”的上升沿之间，信号“c”应该连续或间断地出现3次为高电平。

(4) 在整个检验过程中，信号“start”保持为低。

5.within构造

(1) “within”构造允许在一个序列中定义另一个序列。

(2) within的语法: seq1 within seq2; 表示seq1在seq2的开始到结束的范围内发生，且序列seq2的开始匹配点必须在seq1的开始匹配点之前发生，序列seq1的结束匹配点必须在seq2的结束匹配点之前结束。       

6.within构造实例

属性p32检查序列s32a在信号“start”的上升沿和下降沿之间发生。信号“start”的上升和下降由序列s32b定义。