业界很多人用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问题。