SVA(SystemVerilog Assertions )应用实例：如何断言只出现一次（有且只有一个）？

1.组合关系的序列和时序关系的序列

• 简单的布尔逻辑组成的就是组合关系的序列，如一根信号line_en，或者一个布尔表达式line_en && calc_en；
• 而描述好几个始终周期才能完成的事件的序列就是具有时序关系的序列，即带有延时的序列，如a ##2 b;

2.蕴含

上述两种序列（即所有序列）若是直接写进property，像下面这样：

property p1;
@posedge(clk)
    a ##2 b;
endproperty
           

则在每个时钟边缘都会去检查这个序列，对于上述两种序列略有不同，简介如下：

• 对于组合关系的序列当其布尔值不为1时判为失败；
• 对于时序关系的序列则会先会先看其开始是否有效（即寻找有效开始），如无效则直接判为失败，若有效则再去判断整个序列是否成功，不成功则失败，如a ##2 b，先看a的布尔值是否为1，不为1直接判失败，为1的话再看2拍以后b是否为1，不为1也判为失败；

由上可以看出对于具有时序关系的序列，由于未寻找到有效开始而被判为失败不是我们想要的，所以引入蕴含(组合关系也能用)。

其作用就是规定一个检查的起始点，在没到起始点之前都是空成功（状态是inactive）:

• 对于组合关系的序列，起始点去判断组合序列的布尔值，为1则finished,为0则failed，即其作为序列的长度只有1拍；

property p1;
@posedge(clk)
    $rose(line_en) |-> a;
endproperty
           

• 对于时序关系的序列，检查过程同上，只不过整个检查过程是有了一个开始点，在 r o s e ( l i n e e n ) 之 前 处 于 i n a c t i v e 状 态 ， 在 rose(line_en)之前处于inactive状态，在 rose(linee​n)之前处于inactive状态，在rose(line_en)是去检查序列的开始点a的布尔值，为0则继续处于inactive状态（并不failed），为1则进入active，并执行后续的判断过程；

  可见它是有可能一直处于inactive或active状态的可能的，即有可能没有finished；

property p1;
@posedge(clk)
    $rose(line_en) |-> a ##2 b;
endproperty
           

3.断言有且只有一个

基本知识就复习到这，下面进入主题，问题描述如下：

想监测在line_en拉高期间有且只有一个int脉冲；

我之前的第一反应是可以用intersect，因为刚好可以拆成两个序列：line_en和有且只有一个Int，但尝试了好多次都没成功，后来也试了within，throughout等等，下面带你体验一下菜鸟的心路历程 0 ：

首先把有且只有一个int的序列写出来，即有一个1后一直为0，直到line_en拉低，如下：

$rose(line_en) ##[1:$] Int[=1] ##1 !Int[*1:$] ##1 $fell(line_en)
           

3.1使用intersect

3.1.1 case1

property p1;
@posedge(clk)
    $rose(line_en) |-> ( $rose(line_en) ##[1:$] Int[=1] ##1 !Int[*1:$] ##1 $fell(line_en) )
    intersect line_en;
endproperty
           

这里是直接把line_en这个信号直接作为序列放了上来，由上面我们对组合序列和时序序列的分析可知line_en这个序列的长度只有1拍，所以在line_en为1的每一拍都去判断前面的序列，所以就会一直failed；

3.1.2 case2

property p1;
@posedge(clk)
    $rose(line_en) |-> ( $rose(line_en) ##[1:$] Int[=1] ##1 !Int[*1:$] ##1 $fell(line_en) )
    intersect ( $rose(line_en) ##[1:$] $fell(line_en) );
endproperty
           

这里把line_en这个组合序列改造为时序序列，但是intersect本来是用法是拿一个可以确定长度的序列去控制一个有无限延时的序列的长度，这里我们认为

( $rose(line_en) ##[1:$] $fell(line_en) )

是一个有限长度的序列，但这是不正确的，我们再来复习一下无限时序窗口：

由于无限时序窗口的存在，序列可以重复的满足检验，如

a ##[0:$] b

，b在a=1之后有很多次都为1，那么每一次都是满足检验的，那何时finish呢？

对于

a ##[0:$] b ##[0:$] c

考虑下面两种情况（为便于理解，假设每次拉高都只持续一拍）：

• a拉高后b拉高一次，接着c也拉高，这时就finish了，即每个都只用了一次；
• a拉高后b拉高一次，但直到b再次拉高以后c才拉高，这时也会finish，但是对于b而言它满足的两次的检验；

即为了整体的finish它会使前面的条件无限的重复满足检验，直到所有的都满足才算finished；

对应到这里就是，如果在line_en拉高期间，int始终为0即第一个序列没有满足检验，那么从

$rose(line_en)

到第一次遇到

$fell(line_en)

算是第二个序列的第一次满足检验，由于整体尚未全部满足，所以它会再等后面所有序列都满足的情况，即状态一直是inactive；

所以case2这种写法是在检验至多有一个Int。

另外，为了看起来更简洁，像这么长的序列一般要单独拿出来定义：

sequence s1;
( $rose(line_en) ##[1:$] Int[=1] ##1 !Int[*1:$] ##1 $fell(line_en) );
endsequence
           

下面我们的s1都是这个定义了。

3.1.3 case3

property p1;
@posedge(clk)
    $rose(line_en) |-> s1 intersect
    first_match( $rose(line_en) ##[1:$] $fell(line_en) );
endproperty
           

针对case2的问题，我们使用first_match强制line_en的序列使用第一次match，这样他的长度就和line_en一样长了，并且可以用intersect控制s1的长度了。

至此，intersect使用成功 0：

3.2使用throughout

3.2.1 case1

property p1;
@posedge(clk)
    $rose(line_en) |-> line_en throughout Int[=1]；
endproperty
           

这里是使用非连续重复和使用无限时序窗同样的问题，何时算finish？实际上非连续重复和跟随重复都是用无限时序窗组装成的，所以判断finish的思路是一样的。

所以这里写法只能检验至少有1个；

3.2.2 case2

property p1;
@posedge(clk)
    $rose(line_en) |-> line_en throughout s1；
endproperty
           

这样写就对了；

3.2.2 case2

property p1;
@posedge(clk)
    $rose(line_en) |-> ( line_en throughout Int[=1] )
    ##1 !Int[*1:$] ##1 $fell(line_en)；
endproperty
           

这样拆开组合写也是可以的，和case2的区别在于是如何描述这个过程的；

3.3使用within

3.3.1 case1

property p1;
@posedge(clk)
    $rose(line_en) |-> s1 within line_en;
endproperty
           

3.3.2 case2

property p1;
@posedge(clk)
    s1 within ( $rose(line_en) ##[1:$] $fell(line_en) );
endproperty
           

上述case1和case2和使用intersect的case1/2是一样的问题；

3.3.3 case3

property p1;
@posedge(clk)
    s1 within
    first_match( $rose(line_en) ##[1:$] $fell(line_en) );
endproperty
           

这个就有意思了，写法和intersect一样正确的写法，但你觉得它实现的功能是对的吗？

答案是不对的，反而是和throuout的case1的一样结果:检验的是至少有1个。

这里其实和无限时序窗的逻辑很类似，在于何时判为finish的，无限时序窗是可以重复多次的满足检验，这里是可以重复多次的不满足检验，分析如下，这里

A within B

会要求A比B短，所以这里主要是看A啥时候算finish：

上个图吧，看的更清楚

就比如这里，第一次Int拉高了，但是s1要求其后面一直为低，所以到第二次Int拉高的时刻对于s1的检验而言就failed了，但是这里更关注的是整体的成败，所以s1失败没关系，后面的序列还没结束，所以可以再等s1再一次满足检验，事实上如上图，Int第二次拉高后如果满足s1，那么到

$fell(line_en)

时整个检验就是成功，哪怕期间s1发生了一次failed,但并不报failed；

那何时报failed呢，要是到

$fell(line_en)

时s1一次也没有成功过，那对于整个检验才是failed；

4结语

这个问题是在实际中遇到的，想了很久都没解决，遇到各种各样的错误，学了某个东西遇到实际问题却不会用着实令人气愤，但一旦解决了第一个问题，后面再遇到问题就都上道了，你看这里我这菜鸟都可以把遇到的错误复盘出原因了，之前cshell也是。

不过掌握的这都是鸡毛蒜皮，还是很菜，嗨。

欢迎关注公众号 ：)