除了formal verification外，在基于SV/UVM的隨機(jī)驗(yàn)證中，也可以通過斷言來檢查所有模塊，如仲裁、FIFO和其他自定義邏輯。

但斷言的一個(gè)特征是空成功。（|->或|=>）的左側(cè)是檢查的條件，如果條件為true，右側(cè)結(jié)果的值才有意義。如果左側(cè)是false不成功，則默認(rèn)認(rèn)為該斷言屬性成功。這被稱為“空成功”。

考慮以下情況：

我們有一個(gè)仲裁器，在接收到request以后N個(gè)周期后，可以斷言grant。為了驗(yàn)證是否每個(gè)request都獲得grant，我們將有以下屬性：

property check();

@(posedge clk)

req |-> ##[0:$] gnt;

endproperty

但在這里，如果接收到請(qǐng)求之后，而我們從未從仲裁器那里獲得grant，那么這種斷言將在仿真結(jié)束時(shí)會(huì)空成功。

如果我們以某種方式使這種斷言的空成功轉(zhuǎn)化成fail，那么這將極大地有助于節(jié)省定位周期。

SystemVerilog LRM提供了一個(gè)“strong”運(yùn)算符來通知斷言失敗。根據(jù)IEEE 1800-2017，第16.12.1節(jié)：

strong(sequence_expr) evaluates to true if, and only if, there is a nonempty match of the sequence_expr.

在這里，如果接收到請(qǐng)求，那么我們正在等待至少一個(gè)非空匹配的grant。如果我們看到請(qǐng)求，但從未看到grant，斷言將失敗。

property check();

@(posedge clk)

req |-> strong(##[0:$] gnt);

endproperty

由于strong（sequence_expr）只需要一個(gè)匹配的sequence_expr，當(dāng)且僅當(dāng)屬性strong（first_match（sequence_expr））被計(jì)算為true時(shí)，strong（sequence_expr）的屬性才會(huì)被評(píng)估為true。