業界很多人用formality做形式驗證，檢查rtl或者網表在后端流程中有沒有變質，如果成功了當然很不錯，代表你的設計初衷得到實現了。這里介紹一個formality檢查電源連接的方法，在verify之前就可以看到設計中的電源連接問題。諸如：電源漏接，錯接，庫文件不支持等。做好了電源方案，floorplan才更具參考價值。做好了准備工作，才能心中有數。
當然了，巧婦難為無米之炊，你得先准備好upf文件，這個文件就是你電源設計的初衷，（power intent），upf有規范的標准，所以你不用擔心，找個參考文檔是分分鍾的事情。好了，有了設計和upf文件，代表你對設計有些成熟在心了，能保證沒有問題，一步到位？難，所以還是先檢查一下吧，為了不讓自己白跑一趟流程，做好這些准備工作還是很有必要。當然，如果你有dc綜合的環境，不妨在流程中用用check_mv_design來檢查，同樣可以在早期讓很多電源問題暴露出來。
沒有dc環境怎么辦？來用formality吧，非常簡單，一條命令analyze_upf搞定。2017.09版本之后就好用了。
需要專業的解釋嗎?當然。
analyze_upf commandis used to detect problems in the UPF file that prevents proper verification.
l Foridentified errors, it indicates users did not simulate using the UPF file thatis used in Formality.
l Run thiscommand before verification to identify issues in the UPF file in the referencedesign that can cause verification to erroneously succeed in all-state mode(verification_force_upf_supplies_on==false)
In the N-2017.09version if this command finds issues with the UPF file, either in a referenceor an implementation design
l Preventsfull verification from proceeding.
l Anyerrors detected are treated the same as errors that occur during load_upf.
l The UPFissues must be resolved to load the UPFs without errors.
能不能自動檢查呢? 當然可以，只不過工具默認把這個關了，看着有點着急。為啥呢？關了省時間啊。不過還是打開吧，前期發現並解決問題其實反而會省很多時間。電源沒問題了呢？關了吧，能省一分是一分。用法如下：
• Toautomatically run analyze_upf before preverify.
– set upf_auto_analyze true(the default isfalse)
– When the variable is true, the analyze_upfcommand is run on all containers at the beginning of the preverify step. This will occur when you run preverify,match, or verify commands.
當然了，要問synopsys有沒有專業的檢查upf的工具，有啊，VCLP啊，只不過有多個選擇總是好事，不妨試試用formality檢查設計中的upf問題。