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

Abstraction vs. Reduction

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

RTL中，當timer大于1000時，觸發timeout。需要運行1000個cycle才會觸發。

Reduction將閾值設置為5，縮減到5個cycle觸發。

因為原RTL中還有一個heartbeat，可以重置timer，此時reduction不可以實現原RTL的所有場景（如heartbeat是由另一個計數器控制，閾值是100，而timer每次在5個cycle后就報timeout了，已不滿足原有時序關系） Abstraction通過assume重寫了rtl：1. heartbeat拉高，重置timer 2. heartbeat為低，timer非0，則下個cycle timer非0 3. heartbeat為低，timer為0，則下個cycle timer非0 Abstraction的方式可以復現原RTL的所有場景，同時縮短cycle depth.

采用Reduction還是Abstraction，需要case by case分析；有時Redcution也是Abstraction，理解RTL意圖才是關鍵。

Complexity Manager

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

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

常見的abstraction策略總結如下幾種：

Case Splitting

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

Counter Abstraction (Design Reductions)

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

Constant Propagation and blackboxing

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

Design Size (parameter) Reduction

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

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

Cutpoints and Abstract Models

Cutpoint：切斷rtl中的某個信號，其輸出值不再受原有邏輯錐影響，FPV工具會賦值為任意值驅動后續邏輯。blackboxing的所有輸出端口其實就是每個cutpoint的node.

Cupoint在不同FPV工具設置語法不同，JG中Stopat設置，VC Formal中snip_drive設置

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

Initial Value Abstractions (IVAs)

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

Engine selection

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

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

相當于多個engine”競爭“; 如果多個engine在限定時間內都沒有求解出來，則會放棄當前assertion，安排處理下一個未處理的assertion。當第二次求解之前的assertion時，engine的求解時間會乘以一個系數，例如之前1min沒有求解出，第二次可能會10min，第三次可能會100min. JG提供ProofGrid，可以圖像化顯示engine調度和進展；JG還提供了Proof Profiling Database，可以記錄上次求解時的高效engien，下次運行優先調度此engien；Proof Cache則可以保留一些中間數據，如果rtl和env改動不大，下次運行可以使用這些中間數據，加速求解；

Property Writing

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

1.Cut assertion

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

2.livness assertion

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

livness assertion的求解，工具會在stem后尋找一個loop，當找到這個loop時，就相當于找個一CEX，此assertion被證偽。

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

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

CEX場景是A一直發送數據，C一直輸出A的數據，B發送的第一筆數據被無限期阻塞。實際情況是A不會無限期連續發送數據，總會停止發送?？梢约由蟜airness constraints約束A的最大長度為某一個值。同理B也是。

1.Symbolic Variables

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

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

上述通過generate生成多個并行重復的assertion；而使用Symbolic Variables，聲明一個變量src_sel，并加上合理的約束，可以實現多個并行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)

小結

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

FPV for cache

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

以icache為例：icache大小32 KB，4路組相連，每個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存儲；當發生cache evict時，根據LRU(least recently used）策略替換某一個way的cacheline，lru數據放在lru_mem存儲，下圖未畫出（Cache的基本原理[2]）：

Case Splitting :將assertion歸為不同task分別運行；

Counter Abstraction :執行cache flush時，內部counter會遞增，依次flush 每個cacahe line。對整個空間做flush不現實,需要對counter做abstract;

Constant Propagation and blackboxing :測試function feature時，約束mbist為disabel constant；對不關心的邏輯blackboxing；

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

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

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

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

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

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

審核編輯：劉清