使用abstrct model代替real model

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

Abstraction vs. Reduction

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

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

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

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

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

Complexity Manager

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

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

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

Case Splitting

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

Counter Abstraction (Design Reductions)

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

Constant Propagation and blackboxing

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

Design Size (parameter) Reduction

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

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

Cutpoints and Abstract Models

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

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

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

Initial Value Abstractions (IVAs)

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

Engine selection

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

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

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

Property Writing

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

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。

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

CEX場景是A一直發(fā)送數(shù)據(jù)，C一直輸出A的數(shù)據(jù)，B發(fā)送的第一筆數(shù)據(jù)被無限期阻塞。實際情況是A不會無限期連續(xù)發(fā)送數(shù)據(jù)，總會停止發(fā)送?？梢约由蟜airness constraints約束A的最大長度為某一個值。同理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生成多個并行重復的assertion；而使用Symbolic Variables，聲明一個變量src_sel，并加上合理的約束，可以實現(xiàn)多個并行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é)

上述介紹的多種方法，都是為了降低復雜度；需要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存儲；當發(fā)生cache evict時，根據(jù)LRU(least recently used）策略替換某一個way的cacheline，lru數(shù)據(jù)放在lru_mem存儲，下圖未畫出（Cache的基本原理[2]）：

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

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

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

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

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

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

Cut assertion :對從取指到icache返回指令的斷言，可以看作一個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；

審核編輯：劉清