【已解决】Formality使用问题求助

高BN · 发表于 2018-9-18 15:44:04

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？注册

x

本帖最后由高BN 于 2018-9-21 13:54 编辑

最近在做的一个项目用formality做形式验证的时候总是出现verify无法通过的问题，查看发现都是超时后formality自动退出。analyze_points的结果是：Found 17 Hard Datapath Component Modules
--------------------------------------------------------
These modules contain arithmetic operators that may be
contributing to hard verifications.
Lowering the Design Compiler optimization level for the these
modules may permit verification to succeed.
--------------------------------------------------------

看意思是说降低这些module的优化等级，之前曾经采用过一个做法是把这些path放在一个group里然后把-weight设置的小一点，曾经有几个版本的代码综合后verify可以pass，但跑了很久。最近几个版本的代码又出现这个问题，不知道大家有没有遇到同样或者类似的问题，究竟是RTL代码本身的问题还是综合的优化策略有问题，或者是formality哪里的设置有问题呢？

高BN · 发表于 2018-9-18 15:46:14

综合工具用的是DC，做的是RTL code和DC后生成的netlist之间的verification。

SpunkyGG · 发表于 2018-9-19 17:04:33

根据提示来看，可能是DC优化的太深了，导致formal比不过，可以在DC里设置svp。别优化那么狠，以通过formal为优先。

高BN · 发表于 2018-9-20 10:12:08

回复 3# SpunkyGG

请问一下这个svp具体是什么设置？在DC的USERGUIDE里边没找到类似的内容，谢谢

高BN · 发表于 2018-9-21 13:54:07

回复 3# SpunkyGG

设置了set_vefification_priority之后问题解决了，十分感谢！

edwardk · 发表于 2018-11-18 19:19:15

这个还是个好东西啊，formality的资料还不好找啊

jack570321 · 发表于 2019-3-6 09:09:57

got it! thanks!

liufeiccccc · 发表于 2019-3-19 17:03:32

谢谢

liufeiccccc · 发表于 2019-3-19 17:04:32

谢谢楼主

yangxuchen · 发表于 2023-1-12 14:50:43

高BN 发表于 2018-9-21 13:54
**** 作者被禁止或删除内容自动屏蔽 ****

你好，请问你是对这提示的hard point 进行 set_verification_priority 还是直接 set hdlin_verification_priority "true" ?

[求助] 【已解决】Formality使用问题求助

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

站长推荐 /2