形式验证 | set_case_analysis的处理

海狸先生0119 · 发表于 2024-1-27 10:21:57

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

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

x

请教大佬们：

1、我在综合时对某些point设置set_case_analysis,那么我做形式验证时，需要对这些point人为的设置set_constant吗？
2、综合生成的svf文件里会不会记录我在综合时对哪些point设置了set_case_analysis，进而在做形式验证时不再需要人为设置set_constant？
3、svf文件里的guide_constant对应的是set_case_analysis吗？
谢谢

。

zero_0 · 发表于 2024-1-27 16:21:10

1. 不用，逻辑没改变不用guide
2. 不会记录
3. 不是，就是逻辑上的constant

海狸先生0119 · 发表于 2024-1-29 11:44:06

zero_0 发表于 2024-1-27 16:21
1. 不用，逻辑没改变不用guide
2. 不会记录
3. 不是，就是逻辑上的constant

感谢大佬

[求助] 形式验证 | set_case_analysis的处理

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

站长推荐 /2