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

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

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

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

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

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

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

formal和simulation都需要關注不要出現over constraint，否則導致驗證空間的縮小；

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