“空間爆炸”大大增加了formal工具處理的復(fù)雜度，在有限的資源內(nèi)，難以達(dá)到收斂。所以采用一些abstraction的手段，是十分有效且必要的。正確的abstraction處理，使用abstrct model代替real model，不會影響目標(biāo)結(jié)果，同時(shí)加速證明。

Abstraction vs. Reduction

abstraction不等同于簡單的reduction，如下示例：

RTL中，當(dāng)timer大于1000時(shí)，觸發(fā)timeout。需要運(yùn)行1000個(gè)cycle才會觸發(fā)。

Reduction將閾值設(shè)置為5，縮減到5個(gè)cycle觸發(fā)。

因?yàn)樵璕TL中還有一個(gè)heartbeat，可以重置timer，此時(shí)reduction不可以實(shí)現(xiàn)原RTL的所有場景（如heartbeat是由另一個(gè)計(jì)數(shù)器控制，閾值是100，而timer每次在5個(gè)cycle后就報(bào)timeout了，已不滿足原有時(shí)序關(guān)系） Abstraction通過assume重寫了rtl：1. heartbeat拉高，重置timer 2. heartbeat為低，timer非0，則下個(gè)cycle timer非0 3. heartbeat為低，timer為0，則下個(gè)cycle timer非0 Abstraction的方式可以復(fù)現(xiàn)原RTL的所有場景，同時(shí)縮短cycle depth.

采用Reduction還是Abstraction，需要case by case分析；有時(shí)Redcution也是Abstraction，理解RTL意圖才是關(guān)鍵。

Complexity Manager

有些需要abstraction處理的地方是顯而易見的，如較大的counter或者mem；我們也可以通過FPV工具自帶的復(fù)雜度分析功能來提取哪些地方是收斂瓶頸，然后針對此處做abstraction處理。

當(dāng)然并不是所有東西都要盡善盡美，要綜合ROI考量；對于難以full proof的assertion，采用bounded的方式也是合理可取的，后節(jié)對bounded proof會補(bǔ)充介紹。

常見的abstraction策略總結(jié)如下幾種：

Case Splitting

通過assume區(qū)分不同場景的case，單獨(dú)運(yùn)行。例如：assume property (mode == 2’b00); JasperGold也支持task分隔，更方便管理case splitting。

Counter Abstraction (Design Reductions)

FPV工具支持自動識別counter，jaspergold中可以通過abstract -counter處理；當(dāng)然也可以手動處理；

Constant Propagation and blackboxing

對于不關(guān)心的功能，可以設(shè)置為常量，如.scan_mode(0); 對于不關(guān)心的邏輯，可以設(shè)置為blackboxing；

Design Size (parameter) Reduction

對于參數(shù)化配置的rtl，縮減參數(shù)配置；對于較大的mem，過約束地址訪問空間；如下:

直接Reduction地址空間有一點(diǎn)不“安全”，這改變了原有RTL行為；需要配合simulation仿真加強(qiáng)驗(yàn)證結(jié)果的置信度；或者采用abstraction的方式，F(xiàn)PV工具也提供常見的mem，fifo abstraction model供用戶快速部署；Jaspergold的abstraction model如下：

Cutpoints and Abstract Models

Cutpoint：切斷rtl中的某個(gè)信號，其輸出值不再受原有邏輯錐影響，F(xiàn)PV工具會賦值為任意值驅(qū)動后續(xù)邏輯。blackboxing的所有輸出端口其實(shí)就是每個(gè)cutpoint的node.

Cupoint在不同F(xiàn)PV工具設(shè)置語法不同，JG中Stopat設(shè)置，VC Formal中snip_drive設(shè)置

單獨(dú)cutpoint某個(gè)信號，不加約束，可能會assertion誤報(bào)；一般需要額外assumption處理；如果簡單幾行assumption無法準(zhǔn)確描述，需要glue logic或者glue moduel提供abstract model建模描述；

Initial Value Abstractions (IVAs)

FPV工具每次從reset狀態(tài)開始，隨著cycle的深入，遍歷狀態(tài)空間。如果某些狀態(tài)需要較大的cycle depth，那么是否可以從一個(gè)中間狀態(tài)開始呢？答案是可以的，從某個(gè)中間狀態(tài)，而不是復(fù)位狀態(tài)開始，我們稱為“warm" state。Jaspergold可以通過abstrace -init_value約束一個(gè)初始值

Engine selection

fomal工具內(nèi)置不同的算法引擎，每個(gè)App的適用場景不同，調(diào)用的engine不同；對于FPV app，不同類型的assertion，也和不同類型的engine相”友好“。每個(gè)engine的具體特性，驗(yàn)證人員不需要特別了解（有些engine需要配合使用才能發(fā)揮最大效果；有些engine同時(shí)運(yùn)行可能沖突；有些engine一次只能處理一個(gè)assertion，有些可以并行處理多個(gè)），一般使用工具的auto模式，由工具自動編排調(diào)度engines即可。

不同F(xiàn)PV tool的Engine selection不同，以JasperGold為例：第一次運(yùn)行，工具并不知道哪個(gè)engine最適合哪個(gè)property;而是通過采用多個(gè)engine并行處理某一個(gè)assertion，如果其中一個(gè)engine求解成功，則這些engine會被安排處理下一個(gè)未處理的assertion。

相當(dāng)于多個(gè)engine”競爭“; 如果多個(gè)engine在限定時(shí)間內(nèi)都沒有求解出來，則會放棄當(dāng)前assertion，安排處理下一個(gè)未處理的assertion。當(dāng)?shù)诙吻蠼庵暗腶ssertion時(shí)，engine的求解時(shí)間會乘以一個(gè)系數(shù)，例如之前1min沒有求解出，第二次可能會10min，第三次可能會100min. JG提供ProofGrid，可以圖像化顯示engine調(diào)度和進(jìn)展；JG還提供了Proof Profiling Database，可以記錄上次求解時(shí)的高效engien，下次運(yùn)行優(yōu)先調(diào)度此engien；Proof Cache則可以保留一些中間數(shù)據(jù)，如果rtl和env改動不大，下次運(yùn)行可以使用這些中間數(shù)據(jù)，加速求解；

Property Writing

Formal Verification (二) FPV、APPs[1]在這一篇中講解如何書寫友好的property；本節(jié)再補(bǔ)充三點(diǎn)：

1.Cut assertion

如果一個(gè)end-to-end的assertion跨越的cycle很長，可以嘗試在中間分隔多個(gè)assertion

2.livness assertion

對于livness assertion（含有[0:$],eventually等無限周期的），如果可以使用固定周期值，建議使用固定值，切換為safety assertion。

livness assertion的求解，工具會在stem后尋找一個(gè)loop，當(dāng)找到這個(gè)loop時(shí)，就相當(dāng)于找個(gè)一CEX，此assertion被證偽。

engine對于loop的尋找是很艱難的，所以livness assertion一般很難被full proof。

當(dāng)發(fā)現(xiàn)CEX時(shí)，也不一定是RTL的問題，可能是缺少fairness constraints. 例如兩個(gè)入口port（A，B), 一個(gè)出口port（C），C round-robin處理A,B的burst數(shù)據(jù)；斷言當(dāng)A port接收數(shù)據(jù)后，無限期 s_eventually周期后，C port一定把A的數(shù)據(jù)送出；斷言當(dāng)B port接收數(shù)據(jù)后，無限期 s_eventually周期后，C port一定把B的數(shù)據(jù)送出；此時(shí)兩個(gè)livness assertion fail。

CEX場景是A一直發(fā)送數(shù)據(jù)，C一直輸出A的數(shù)據(jù)，B發(fā)送的第一筆數(shù)據(jù)被無限期阻塞。實(shí)際情況是A不會無限期連續(xù)發(fā)送數(shù)據(jù)，總會停止發(fā)送。可以加上fairness constraints約束A的最大長度為某一個(gè)值。同理B也是。

1.Symbolic Variables

Symbolic Variables有很多叫法例如Pseudo-constants、Free variables，采用這總方式書寫assertion，不僅減少assertion數(shù)量，便于描述assertion,對工具也更友好。如下示例：

genvari;
generatefor(i=0;i
$past(rv_plic.le[i])||$past(intr_src_i[i]),clk_i,!rst_ni)
end

上述通過generate生成多個(gè)并行重復(fù)的assertion；而使用Symbolic Variables，聲明一個(gè)變量src_sel，并加上合理的約束，可以實(shí)現(xiàn)多個(gè)并行assertion的效果。

logic[$clog2(N_SOURCE)-1:0]src_sel;
`ASSUME_FPV(IsrcRange_M,src_sel>=0&&src_sel
$past(rv_plic.le[src_sel])||$past(intr_src_i[src_sel]),clk_i,!rst_ni)

小結(jié)

上述介紹的多種方法，都是為了降低復(fù)雜度；需要case by case的分析采用哪一種；還有一些方法屬于更高階的使用，需要tool by tool。如JasperGold提供SST(State-Space Tunneling)功能，通過增加helper assertions加速求解。

FPV for cache

驗(yàn)證cache采用FPV的手段，是一個(gè)典型的場景，會覆蓋上述提到的所有abstraction strategy。

以icache為例：icache大小32 KB，4路組相連，每個(gè)cache line大小是32B，一共有256組set；cache line size是32 Bytes，offset為5位；256組，index為8位，剩下的為tag部分，占用35位，其中tag的最高bit為valid flag；tam部分放在tag_mem存儲；data放在data_mem存儲；當(dāng)發(fā)生cache evict時(shí)，根據(jù)LRU(least recently used）策略替換某一個(gè)way的cacheline，lru數(shù)據(jù)放在lru_mem存儲，下圖未畫出（Cache的基本原理[2]）：

Case Splitting :將assertion歸為不同task分別運(yùn)行；

Counter Abstraction :執(zhí)行cache flush時(shí)，內(nèi)部counter會遞增，依次flush 每個(gè)cacahe line。對整個(gè)空間做flush不現(xiàn)實(shí),需要對counter做abstract;

Constant Propagation and blackboxing :測試function feature時(shí)，約束mbist為disabel constant；對不關(guān)心的邏輯blackboxing；

Design Size (parameter) Reduction :icache可能支持多bank，不同組相連，不同cache line size的配置，選取一個(gè)最小的特征配置；

Cutpoints and Abstract Models :為了減少mem空間，需要過約束取指端口命中的set數(shù)量，同時(shí)對tag_mem,data_mem，lru_mem做abstraction處理；

Initial Value Abstractions :FPV默認(rèn)從復(fù)位開始，icache復(fù)位后自動flush cache，所有每次都是從invalid狀態(tài)開始 ”震蕩“ 狀態(tài)空間；可以利用IVAs給tag_mem，data_men，lru_mem使用約束賦合理的初始值，加速求解；

Cut assertion :對從取指到icache返回指令的斷言，可以看作一個(gè)end to end的斷言，如果cache miss, cycle-depth會增加，F(xiàn)PV求解難度加大，可以嘗試cut assertion；

livness assertion :上述end to end的assertion，一般也是livness的；可能需要添加一些fairness constraints；一般livness assertion都是bounded proof；

Symbolic Variables :對于同一set不可能出現(xiàn)相同tag的斷言，采用Symbolic Variables的方式書寫assertion；

審核編輯：劉清