1.14蕴含操作符

        属性p7有下列特别之处
        (1)属性在每一个时钟上升沿寻找序列的有效开始。在这种情况下,它在每个时钟上升沿检查信号“a”是否为高。
        (2)如果信号“a”在给定的任何时钟上升沿不为高,检验器将产生一个错误信息。这并不是一个有效的错误信息,因为我们并不关心只检查信号“a”的电平。这个错误只表明我们在这个时钟周期没有得到检验器的有效起始点。虽然这些错误是良性的,它们会在一段时间内产生大量的错误信息,因为检查在每个时钟周期都被执行。为了避免这些错误,某种约束技术需要被定义来在检查的起始点不有效时忽略这次检查SVA提供了一项技术来实现这个目的。这项技术叫作“蕴含”(Implication)。
        蕴含等效于一个if-then结构。蕴含的左边叫作“先行算子”( antecedent),右边叫作“后续算子”( consequent)。先行算子是约束条件。当先行算子成功时,后续算子才会被计算。如果先行算子不成功,那么整个属性就默认地被认为成功。这叫作“空成功”( vacuous success)。蕴含结构只能被用在属性定义中,不能在序列中使用。蕴含可以分为两类:交叠蕴含( Overlapped implication)和非交叠蕴含(Non- overlapped implication)。

1.14.1交叠蕴含

        交叠蕴含用符号“|->”表示。如果先行算子匹配,在同一个时钟周期计算后续算子表达式。下面用一个简单的例子解释。属性p8检查信号“a”在给定的时钟上升沿是否为高电平,如果a为高,信号“b”在相同的时钟边沿也必须为高。

property p8;
	@(posedge clk)  a|->b;
endproperty

a8 : assert property (p8);

        图1-11显示了断言a8在模拟中的响应。表1-5总结了信号“a”和信号“b”的采样值和断言的状态。表中一共显示了三种结果。当信号“a”检测为有效的高电平,而且信号“b”在同一个时钟沿也检测为高,这是一个真正的成功。若信号“a”不为高,断言默认地自动成功,则称为空成功。相应的,失败指的是信号“a”检测为高且在同一个时钟沿信号“b”未能检测为有效的高电平。

 

1.14.2非交叠蕴含

        非交叠蕴含用符号“|=>”表示。如果先行算子匹配,那么在下一个时钟周期计算后续算子表达式。后续算子表达式的计算总是有一个时钟周期的延迟。下面以属性p9举个简单的例子。该属性检查信号“a”在给定的时钟上升沿是否为高,如果为高,信号“b”必须在下一个时钟边沿为高。

property p9;
	@(posedge clk) a |=> b;
endproperty

a9 : assert property (p9);

        图1-12显示了断言a9在模拟中的响应。表1-6总结了信号“a和信号“b”的采样值以及断言的状态。应注意的是,断言在当前时钟周期开始,在下一个时钟周期成功的情况才是真正的成功。相应的,如果属性有一个有效的开始(信号“a”为高),且信号“b”在下一个时钟周期不为高,属性失败。

1.14.3后续算子带固定延迟的蕴含

        属性p10检查如果信号“a”在给定时钟上升沿为高,在两个时钟周期后信号“b”应该为高。类似的检查在前面已经用不使用蕴含的方式介绍过了。使用蕴含使得所有误报的错误都被消除。只有属性有效开始(信号“a”为高)时,才进行后续算子的检查(信号“a”)。图1-13显示了属性p10的一个模拟的例子。表1-7总结了属性p10中信号的采样值。

property p10;
	@(posedge clk) a-> ## 2 b;
endproperty

a10 : assert property (p10);

1.14.4使用序列作为先行算子的蕴含

        属性p10在先行算子的位置使用的是信号。先行算子同样可以使用序列的定义。在这种情况下,仅当先行算子中的序列成功时,才计算后续算子中的序列或者布尔表达式。在任何给定的时周期,序列slla检查如果信号“a”和信号“b”都为高,一个时钟周期之后信号“c”应该为高。序列s11b检查当前时钟上升沿的两个时钟周期后,信号“d”应为低。最终的属性检查如果序s11a成功,那么序列s11b被检查。如果没有监测到有效的序列slla,那么序列s11b将不被检查,属性检査得到一次空成功。

sequence s11a;
	@(posedge clk) (a && b )  ##1 c;
endsequence

sequence s11b;
	@(posedge clk) ##2 !d;
endsequence

property p11;
	s11a |-> s11b;
endproperty

        图1-14显示了断言a11在模拟中的表现。标记1s和1e表明了一个成功的属性检查的起始和结束。标记2s和2e标出了一个失败的起始和结束。在时钟周期11,信号“a”和信号“b”都为高。这表明2个时钟周期以后,即时钟周期14,信号“d”应该为低。但是在例子中的波形上信号“d”为高电平,因此属性失败。

        图中所有的空成功都用简单的竖线表示标记3s和3e显示了个成功的属性检查的起始和结束。表达式“a&&b”在时钟周期17为真,在一个时钟周期后,信号“c”像预期的一样为高。因此在时钟周期18,序列s11a成功。正如被期望的那样,接着信号“d”在两个时钟周期后为低。因此,属性在时钟周期20成功。