Formal Verification的基礎(chǔ)知識

通過上一篇對Formal Verification有了基本的認(rèn)識；本篇將通過一個簡單的例子，感受一下Formal的“魅力”；目前Formal Tool主流的有Synopsys的VC Formal，Cadence的Jaspergold，Mentor的Questa FV，一些小的EDA廠家如：OneSpin[1]的Verify，symbioticeda[2]，SymbiYosys[3]；對于大公司，如Intel，使用自研formal工具；還有一些提供formal解決方案的公司，如OneSpin(已與Siemens EDA合作)，Oski Tec(已被NVIDIA收購)。

Assertion

具體assertion的語法不再介紹，可以參考《SystemVerilog Assertions and Functional Coverage》以及《Formal Verification --An Essential Toolkit for Modern VLSI Design》的 CHAPTER 3；

SVA in Formal

FPV對不同的SVA Property，調(diào)用合適的算法engine進(jìn)行建模，依據(jù)算法模型從初始狀態(tài)Reset state對DUT所有的input自動施加激勵，隨著cycle的depth增加，逐漸窮盡狀態(tài)空間。

The full space of all possible RTL state values: 最外層的紫方框為RTL的所有可能存在的狀態(tài)空間（input + state element(dff,latch))。
The reset states：初始狀態(tài)，一般從reset復(fù)位開始。The reachable states：從reset state可以，自動對input施加激勵，可以達(dá)到的狀態(tài)。(所以紫方框以內(nèi)綠橢圓以外的空間，是無法達(dá)到的空間，例如RTL中的dead code)Assumptions：使用SVA的assume對DUT進(jìn)行約束；橙色橢圓型，約束縮小了狀態(tài)空間。Assertion: 使用SVA的assert對property進(jìn)行斷言；斷言屬性定義了模型的行為，例如assert property: ( @(posedge clk) clr |=> ((overfloat==0)&&(cnt==0)));斷言了在clk上升沿采樣時，若clr為高(先行算子anteceden成功)，下一個clk上升沿采樣到的overfloat和cnt都為0（后續(xù)算子consequent）；而Formal工具要做的就是窮盡狀態(tài)空間找出一個counter-exampleCEX反例，進(jìn)行falsified證偽，例如overfloat和cnt都不為0或者只有一個為0；如果CEX出現(xiàn)，而assertion為golden，則就說明DUT不滿足spec。Asser1: pass，因為這個CEX不滿足assumptions的約束，不是一個有效狀態(tài)。Assert2: pass，因為這個CEX本身不是可以達(dá)到的狀態(tài)。Assert3: fail，有效狀態(tài)和約束內(nèi)，出現(xiàn)了一個CEX。Cover Points: 使用SVA的cover對property設(shè)置覆蓋點；相當(dāng)于設(shè)置一個觀察點，F(xiàn)ormal工具會窮盡狀態(tài)空間，找到一個滿足要求的狀態(tài)；Cover1: 該覆蓋點被coverCover2: 該覆蓋點在約束之外，unreachableCover3: 該覆蓋點在有效空間之外，unreachable

VC Formal定義了Assertion和Cover Points的結(jié)果如下：Assertion:proven: assertion pass，窮盡狀態(tài)空間也找不到一個CEXfalsified:assertion fail，出現(xiàn)不滿足斷言的CEXinconclusive: Formal在N個cycle depth內(nèi)，沒有找到CEX，屬于Bounded Proof，有界證明，這個"界“bounded (safe) depth就是N個cycle depth。vacuous:對于包含蘊含操作符|->|=>的property，如果antecedent一直未被觸發(fā)，也一定不會出現(xiàn)CEX，此時為空成功vacuous success。vacuous在Simulation中經(jīng)常出現(xiàn)，因為施加的有限激勵，沒有觸發(fā)antecedent成功。但是在Formal中，需要引起注意。Cover Points:Covered: 覆蓋Uncovered: 未覆蓋

the SVA differences

在Simaltion和Formal中，SVA的使用略有不同：

Simulation中的assume和assertion作用相同，不起到約束的作用；而Formal中，assume實現(xiàn)約束的作用；對于Simulation的vacuous success，并不會報錯引起用戶注意，一般建議對property同時做assert和cover處理。

Sequential depth

Sequential depth：也就是上文提及到的Cycle depth；較大的Sequential depth，容易產(chǎn)生inconclusive的結(jié)果。

Assertion Logic Contributes to State Space

COI

COI(CONES OF INFLUENCE)：COI是Formal工具對property的邏輯電路映射，也被稱作Logic Cones邏輯錐。COI包含property的所有input和state element，這些決定了不同的輸出結(jié)果。

Formal工具對一個property解析生成的COI Schematic：

從用戶角度，我們不必關(guān)心一個property的COI具體是什么樣子；用戶創(chuàng)建的所有property的COI集合對DUT RTL的覆蓋情況，類似于Simulation中的Code coverage，稱為Property Density。

The suggestion of SVA for Formal

formal model從SVA中提取，所以SVA的書寫方式，也會影響Formal的效率，推薦的SVA Coding Guidelines可以參考《VC_Formal_UG》Appendix B。下面介紹一些常見的assertion”技巧“:

uniform format

assertion的書寫，需要遵循同一的格式，每條assertion有相應(yīng)的文檔記錄；每條property都有可讀性的lable標(biāo)注；可以采用一些宏定義，簡化assertion的書寫，參考：prim_assert.sv[4]當(dāng)assertion的clock,reset都是同一個時，可以聲明default clocking和default disable iff，簡化書寫。

Immediate VS Concurrent

雖然立即斷言在一些情況下等效于并發(fā)斷言，如下：

//ConcurrentAssertion
assert_overfloat_func:assertproperty(`clk_rst$rose(overfloat)|->$past(cnt==4'hF));

//ImmediateAssertion
always@(posedgeclk)
if($rose(overfloat)&&(rstn==1))
assert_overfloat_func_2:assert($past(cnt==4'hF));

但是建議使用并發(fā)斷言，F(xiàn)ormal工具對蘊含操作符的支持更好。

Try use implication

不建議直接對sequence進(jìn)行斷言，sequence會在每個cycle都被檢查；推薦使用蘊含操作符的方式。

//BAD
propertysend_header_payload;
@(posedgeclk)disableiff(reset)
(enable##1header##1payload[*16]);
endproperty
//GOOD
propertysend_header_payload;
@(posedgeclk)disableiff(reset)
$rose(enable)|=>header##1payload[*16];
endproperty

SVA Modeling Layer Code

可以通過增加Auxiliary Code，簡化property的書寫難度；如下：

moduleassert_top(inputrstn,inputclk,inputA,
input,B,inputC,inputwr,inputrd);
//Requirement:inputsA,B,Caremutuallyexclusive
wire[2:0]my_bus={A,B,C};
a_abc_mutex:assertproperty(@(posedgeclk)$onehot0(my_bus));
//Requirement:Nomorethan5outstandingwr’s(withoutard)
//andnordbeforewr
reg[2:0]my_cnt;
always@(posedgeclkornegedgerstn)
if(!rstn)my_cnt<=?3’b000;
????????else
????????????if?(?wr?&&?!rd)?my_cnt?<=?my_cnt?+?1;
????????????else?if?(!wr?&&?rd)?my_cnt?<=?my_cnt?–?1;
????????????else?my_cnt?<=?my_cnt;
a_wr_outstand_le5:?assert?property?(@(posedge?clk)?my_cnt?<=?3’d5?);
a_no_rd_wo_wr:?assert?property?(@(posedge?clk)?!((my_cnt?==?3’d0)?&&?rd));
endmodule

use function

assertion中可以調(diào)用funciton。

//Computenextgrantforround-robinscheme
functionlogic[3:0]fv_rr_next(logic[3:0]req,logic[3:0]gnt);
fv_rr_next=0;
for(inti=1;(i<4);?i++)?begin
????????if?(req[(fv_which_bit(gnt)+i)%4])?begin
??????????fv_rr_next[(fv_which_bit(gnt)+i)%4]?=?1;
??????????break;
????????end
????end
endfunction

Page81_rr_next:??assert?property?(((opcode?==?NOP)?&&?
????(|gnt?==?1)?&&?(|req?==?1)?&&?(|(req&gnt)==4'b0))?|=>(gnt==fv_rr_next(req,gnt)))
else$error("Violationofroundrobingrantpolicy.");

as SIMPLE as possible

將一個大的assertion才分為多個小的assertion

$rose(START)|=>(ENABLE&&~START&&~STOP)[*7]
##1(ENABLE&&~START&&STOP)|=>
(~ENABLE&&~START&&~STOP);

$rose(START)|->~ENABLE##1ENABLE;
$rose(ENABLE)|->(~START&&~STOP)[*7];
$rose(STOP)|->ENABLE##1~ENABLE;
$fell(START)|=>##5$rose(STOP);

as SHORT as possible

盡量縮短Cycle Depth，使用[0:$]或者太大的時間delay不利于formal分析。

a5:assertproperty@(posedgeclk)a|->(##[0:$]b);
a6:assertproperty(@(posedgeclk)disableiff(~rst_n)A##1B|=>C##[1:100]D);

use Systemverilog

采用可綜合的systemvrilog語法，如interface,struct等，使用更便捷；像s_eventually, 在sv09才支持。

Formal Property Verification

以一個counter做簡單的演示：

modulecounter(
inputclk,
inputrstn,
inputen,
inputclr,
outputcnt,
outputoverfloat
);

reg[3:0]cnt;
regoverfloat;

always@(posedgeclk,negedgerstn)
begin
if(!rstn)
cnt<=?4'b0;
????else?if?(clr)
???????cnt?<=?0;
????else?if?(en?&?(cnt!=4'hF))
???????cnt?<=?cnt?+?1;
end


always@(posedge?clk,negedge?rstn)
begin
????if(!rstn)
???????overfloat?<=?1'b0;
????else?if?(clr)
???????overfloat?<=?1'b0;
????else?if?(cnt==15)
???????overfloat?<=?1'b1;
end

`ifdef?FPV

`define?clk_rst?@(posedge?clk)?disable?iff?(!rstn)


//ASSUME
assume_en_clr_conflit:?assume?property?(`clk_rst?!(en?&&?clr));

//COVER
cover_clr_overfloat:?cover?property?(`clk_rst?$fell(overfloat));
cover_cnt_value:?cover?property?(`clk_rst?(cnt==20));

//ASSERT
assert_clr_func:?assert?property(`clk_rst?clr?|=>((overfloat==0)&&(cnt==0)));


propertyp_en_func;
inttmp;
`clk_rst(en,tmp=cnt)|=>if(cnt!=4'hF)(tmp+1==cnt);
endproperty

assert_en_func:assertproperty(p_en_func);

assert_clr_overfloat:assertproperty(`clk_rst$fell(overfloat)|->$past(clr));
//PASS
assert_overfloat_func:assertproperty(`clk_rst$rose(overfloat)|->$past(cnt==4'hF));
//WRONGassertion
assert_overfloat_func_fail:assertproperty(`clk_rst(cnt==4'hF)|=>overfloat);

//ImmediateAssert
always@(posedgeclk)
if($rose(overfloat)&&(rstn==1))
assert_overfloat_func_2:assert($past(cnt==4'hF));

`endif
endmodule

Result:vacuity欄為property的先行算子成立的cycle depth。witness欄為property的后續(xù)算子成立的cycle depth。對于assert_overfloat_func這個property，witness早于vacuity1個cycle，是因為$past()是對過去的判斷。

Initial State定義clk,rstn；從復(fù)位狀態(tài)開始，F(xiàn)ormal工具自動對input信號灌入激勵。

#ClockDefinitions
create_clockclk-period100
#ResetDefinitions
create_resetrstn-senselow

#InitialisationCommands
sim_run-stable
sim_save_reset

ASSUME增加了en和clr不可能同時為高的約束。

COVER增加一些關(guān)心的cover point，工具可以快速地跑出對應(yīng)波形：例如$fell(overfloat)的cover:

200ns:完成復(fù)位2000ns:cover point match(注意采樣的上升沿前的數(shù)據(jù)）

對于(cnt==20))則是uncover，cnt最大值為15。

ASSERTassert_overfloat_func_fail: assert property (`clk_rst (cnt==4'hF) |=> overfloat);這個propery斷言失敗，被工具找到了一個CEX: 當(dāng)cnt==4'hF時，同時拉高clr，overfloat就不會為高了。

在這里插入圖片描述

assertion annotation:

**ENGINE** Type欄的e1,s6,t3為算法引擎的代號；工具會根據(jù)property的特性選擇合適的算法，調(diào)用相應(yīng)的引擎處理；VC Formal中的engines:

常見算法為：

?Binary Decision Diagrams orBDD

?"SATisfiability" Proofs orSAT

?Bounded Model Checking orBMC

?Craig Interpolation, usually shortened to "Craig"

?Property Directed Reachability orPDR

一般使用工具默認(rèn)分配的engine，當(dāng)然用戶也可以自己指定；VC Formal提供了多種引擎編排的recipes，適用FPV不同的使用場景。

JasperGold Result

CEX wave:

JasperGold中的engines:

FPV的使用場景

design exercise FPV

FPV不需要搭建平臺和手動施加激勵，適合快速的在一些新設(shè)計的RTL上跑一些基礎(chǔ)功能；例如上一節(jié)$fell(overfloat))這個cover point，如果通過Simulatin，需要搭建testbench并詳盡地施加每一拍的激勵；而使用Formal，設(shè)計人員不需要關(guān)注整個過程，只關(guān)注最終結(jié)果，工具會自動施加相應(yīng)的激勵并達(dá)到你想要的結(jié)果。

所以當(dāng)你有以下需求時，可以考慮使用design exercise FPV：

1.對于新設(shè)計的模塊，想要跑一些基礎(chǔ)功能進(jìn)行確認(rèn)

2.在驗證人員的驗證平臺還沒有準(zhǔn)備好時，需要自己提前做一些簡略地驗證

3.接手遺留的RTL代碼，可以跑一下FPV，結(jié)合波形加深對特定功能的理解

設(shè)計人員自己跑FPV，對RTL內(nèi)部細(xì)節(jié)很了解；思路一般是：首先增加感興趣的cover point；再添加一些assumption，可以過度約束；先跑出一些簡單功能的波形；增加一些assertion，做檢查；接著添加一些復(fù)雜功能的assertion和cover point，并逐漸放寬assumption；跑FPV并不是可以一次性把所有property都寫完備，需要"wiggle"幾輪，多次調(diào)試property；

有些公司對IP開發(fā)有額外的斷言標(biāo)準(zhǔn)要求，例如property應(yīng)該占RTL總代碼行數(shù)的三分之一；這些property既可以用于formal，也可以用于simulation。《Assertion-Based Design》，《Creating Assertion-Based IP》書籍中介紹了相關(guān)經(jīng)驗。

Bug hunting FPV

當(dāng)你有以下需求時，可以考慮使用Bug hunting FPV：

1.你所驗證的模塊有很多corner cases，需要額外的FPV驗證保證完備性

2.Simulation回歸random case時，陸續(xù)發(fā)現(xiàn)新的error，需要額外的FPV驗證提高置信度

3.對于一個成熟的模塊，加了一個新的feature，需要額外的FPV驗證

Bug hunting FPV是Simulation的補充驗證手段，采用更高層級的assertion，加入過約束，將注意力集中于某一個功能點；

full proof FPV

對一個設(shè)計只采用FPV進(jìn)行驗證，保證設(shè)計功能100%符合spec；這個從理論上是完全可行的，也是Formal Verification的初衷：只要property是完備的，正確的，相對于RTL，就可以建立一個golden model，遍歷RTL的所有狀態(tài)空間，保證100%正確。當(dāng)你滿足以下條件時，可以采用full proof FPV：

1.待測設(shè)計有一個詳細(xì)的規(guī)格書或者一個包含所有功能點的表格

2.待測設(shè)計是一個標(biāo)準(zhǔn)接口，可以采用商業(yè)的AIP進(jìn)行驗證

對于full proof FPV，每種Formal工具都有推薦的sign-off流程，來保證驗證的完備。

VC Formal的推薦流程如下：

JasperGold的推薦流程如下：

通過收集覆蓋率，保證property的完備，完成sign-off工作。具體后文介紹。

APPs

formal tool除了FPV，還提供了其他適用不同場景的APPs，如對于pinmux可以采用connectivity連通性檢查，對于寄存器的訪問采用register檢查，對于一塊mem，是否存在其他非法訪問路勁，可以才用security檢查；這一類app都是FPV的衍生，通過提供一文件或約束，工具自動產(chǎn)生property，調(diào)用最佳engine處理。相較于FPV，學(xué)習(xí)成本低。對于汽車產(chǎn)品，有額外的Functional Safety要求，工具會自動對rtl注錯分析其影響結(jié)果。

VC Fomrla Apps:

對于以上Apps, 可能除了DPV, JasperGold都有對應(yīng)的Apps.