Formal驗證三要素解析：Input、Object與Output的作用

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

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

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

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

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

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

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

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

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