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也是。

不過掌握的這都是雞毛蒜皮，還是很菜，嗨。

歡迎關注公衆号 ：)