Formal驗(yàn)證三要素解析：Input、Object與Output的作用

Formal三要素：input(輸入) + object(對(duì)象) + output(輸出)。Formal有點(diǎn)像上帝，我們把input和object灌進(jìn)formal，formal會(huì)給出個(gè)output來指示結(jié)果是否正確。

Object：是我們要證明的對(duì)象，通常是DUT；

Input：是我們給的輸入，通常是assert和assume，assert是預(yù)期的行為，assume是假定的行為；

Output：是formal依據(jù)input和object推導(dǎo)出的結(jié)果。Output通常有三種結(jié)果：1. 證明成功；2. 證明失敗，并給出反例波形；3. 還沒有證明完成，可能需要更多的時(shí)間；

由于Formal本身性質(zhì)，證明的cycle時(shí)間越長(zhǎng)，所需要的計(jì)算量是指數(shù)級(jí)增長(zhǎng)的，在超過formal可驗(yàn)證時(shí)間之外的bug是無法檢查出來。有兩種方法可以降低：1. 減少FF，2. 減低bug檢查的cycle。

在formal驗(yàn)證中，需要注意不要over constraint，否則會(huì)漏檢測(cè)bug，寧愿constraint放寬點(diǎn)，這樣會(huì)覆蓋的范圍更廣點(diǎn)，雖然可能會(huì)導(dǎo)致誤報(bào)一些counter examples，但驗(yàn)證更全面的，這有點(diǎn)類似simulation。為了檢查formal有沒有過約束，一方面可以assert和assume互換交叉驗(yàn)證，另一方面可以利用formal工具生成的覆蓋率來分析所灌入的激勵(lì)是否過約束和check的點(diǎn)是否都覆蓋，這一點(diǎn)也類似simulation。

formal和simulation的一大區(qū)別是：formal只要用戶沒有說不能做，它都全部遍歷；simulation是遍歷用戶規(guī)定的行為，雖然這些行為是用戶自己random出來的，但也算是用戶規(guī)定的范圍。

formal和simulation都需要關(guān)注不要出現(xiàn)over constraint，否則導(dǎo)致驗(yàn)證空間的縮小；

formal和simulation也都需要關(guān)注覆蓋率，來調(diào)整constraint；formal和simulation的完備性目前只能通過人和工具一塊分析盡可能達(dá)到的。人根據(jù)經(jīng)驗(yàn)想好各種可能得場(chǎng)景和激勵(lì)，工具可以生成覆蓋率來查看DUT驗(yàn)證的是否充分。