网站建设mfdos下载百度 安装

        蕴含( (implication)是目前讨论到的允许定义前提条件的一项技术。例如,要对一个指定的序列进行检验,必须某个前提条件为真。也有这样的情况,要求在检验序列的整个过程中,某个条件必须一直为真。蕴含只在时钟边沿检验前提条件一次,然后就开始检验后续算子部分,因此它不检测先行算子是否一直保持为真。为了保证某些条件在整个序列的验证过程中一直为真,可以使用“ throughout”运算符。运算符“ throughout”的基本语法如下所示:

(expression ) throughout (sequence definition)

        属性p31检查下列内容:
        a.在信号“ start”的下降沿开始检査。
        b.检查表达式((!a && !b )##1 (c[->3]) ##1 (a && b));
        c.序列检查在信号“a”和“b”的下降沿与信号“a”和“b的上升沿之间,信号“c”应该连续或间断地出现3次为高电平。
        d.在整个检验过程中,信号“ start”保持为低。

property p31;@(posedge clk) $fell(start) |->(!start) throughout (##1 (!a && !b) ##1 (c[->3] ##1 (a &&b )));
endproperty

        图1-33显示了属性p31在模拟中的响应。检验在时钟周期3成功,在时钟周期16失败。
        成功1——信号“ start”在时钟周期3被检测到一个下降沿因此属性的先行算子成功个周期后,信号“a”和信号“b如期在时钟周期4为低。之后,信号“c”如期望地分别在时钟周期6,9,11重复三次。接着在时钟周期12,信号“a”和信号“b”如期为高。因此属性从时钟周期3开始,在时钟周期12成功。注意到,信号“ start”从时钟周期3一直到时钟周期12保持低电平。这是本次检验成功的关键。

        失败1——信号“sa”在时钟周期16检测到一个下降沿,因此属性的先行算子成功。一个周期后,信号“a”和信号“b如期在时钟周期17为低。之后,期望信号“c”重复为高三次我们分别在时钟周期18和20发现两次重复。但是在时钟周期21,信号“c”的第三次重复还没出现,信号“ start”就被检测出高电平,因此检验在时钟周期21失败。违背了“ throughout”的条件导致了整个检验的失败