相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482SVF文件的全称是Setup Verification for Formality即Design Compiler提供给Formality的设置验证文件它的作用是为Formality的指导模式(Guidance)和设置模式(Setup)提供信息以帮助其更好地理解和处理设计流程中因使用Design Compiler而引起的设计变更的一种机制。SVF文件的详细介绍和生成命令在下面的博客中已经讨论本文主要讨论Formality中的set_svf命令。Design Compilerset_svf命令以及SVF文件简介文章浏览阅读1k次点赞17次收藏31次。svf文件的全称是Setup Verification for Formality即Design Compiler提供给Formality的设置验证文件它的作用是为Formality的指导模式(Guidance)和设置模式(Setup)提供信息以帮助其更好地理解和处理设计流程中因使用Design Compiler而引起的设计变更的一种机制。对象名称更改(Object name changes)_svf 文件https://blog.csdn.net/weixin_45791458/article/details/144069207?spm1001.2014.3001.5501set_svf命令的BNF范式有关BNF范式可以参考以往文章为set_svf [-append] [-ordered] [-extension name] [filedirnames]指定追加-append表示将指定的SVF文件或目录中搜索到的SVF文件追加到已加载进Formality的svf信息后如果不指定该选项则会覆盖之前的svf信息。例如假设现在有两个SVF文件default.svf中含有两条guide类命令而test.svf中含有三条guide类命令现在分别使用两个set_svf命令先后加载这两个SVF文件当第二个set_svf命令不使用-append选项时第二次加载的SVF文件会覆盖第一次加载的SVF文件反之则会追加。具体情况如例1所示。// 例1 Formality (setup) set_svf default.svf SVF set to default.svf. 1 Formality (setup) report_guidance ************************************************** Report : guidance Reference : None Implementation : None Version : O-2018.06-SP1 Date : Wed Dec 11 22:51:11 2024 ************************************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 1 0 0 1 2 Note: If verification succeeds you can safely ignore unaccepted guidance commands. SVF files read: default.svf SVF files produced: /home/zhangchen/Desktop/vv/formality_svf/ svf.txt 1 Formality (setup) set_svf test.svf SVF set to test.svf. 1 Formality (setup) report_guidance ************************************************** Report : guidance Reference : None Implementation : None Version : O-2018.06-SP1 Date : Wed Dec 11 22:51:19 2024 ************************************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 1 0 0 2 3 Note: If verification succeeds you can safely ignore unaccepted guidance commands. SVF files read: test.svf SVF files produced: /home/zhangchen/Desktop/vv/formality_svf/ svf.txt 1 Formality (setup) set_svf -append default.svf SVF appended with default.svf. 1 Formality (setup) report_guidance ************************************************** Report : guidance Reference : None Implementation : None Version : O-2018.06-SP1 Date : Wed Dec 11 22:52:34 2024 ************************************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 1 0 0 4 5 Note: If verification succeeds you can safely ignore unaccepted guidance commands. SVF files read: test.svf default.svf SVF files produced: /home/zhangchen/Desktop/vv/formality_svf/ svf.txt 1顺带一提除了使用report_guidance命令查看已加载的SVF文件或用户执行的guide类命令也可以在Formality工作目录中的formality_svf子目录中找到svf.txt文件它是已加载的SVF文件的文本可读形式。用户通常无需显式执行report_guidance命令Formality在preverify阶段结束时会自动执行report_guidance命令如图1所示。图1 preverify阶段末尾的报告指定顺序-ordered选项用于指定了多于一个SVF文件或者指定了搜索目录的set_svf命令默认情况下set_svf命令按照时间戳顺序加载这些SVF文件。如果指定了-ordered选项set_svf命令按照SVF文件指定的顺序和搜索目录中的搜索顺序按照文件名顺序。例如假设现在有两个SVF文件default.svf时间戳更早中含有两条guide类命令而test.svf中含有三条guide类命令现在使用一个set_svf命令加载这两个SVF文件当不使用-ordered选项时会按照按照时间戳顺序加载这两个SVF文件反之则会按照SVF文件指定的顺序加载这两个SVF文件。具体情况如例2所示。Formality (setup) set_svf test.svf default.svf SVF set to default.svf test.svf. 1 Formality (setup) report_guidance ************************************************** Report : guidance Reference : None Implementation : None Version : O-2018.06-SP1 Date : Wed Dec 11 23:23:36 2024 ************************************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 1 0 0 4 5 Note: If verification succeeds you can safely ignore unaccepted guidance commands. SVF files read: default.svf test.svf SVF files produced: /home/zhangchen/Desktop/vv/formality_svf/ svf.txt 1 Formality (setup) set_svf -ordered test.svf default.svf SVF set to test.svf default.svf. 1 Formality (setup) report_guidance ************************************************** Report : guidance Reference : None Implementation : None Version : O-2018.06-SP1 Date : Wed Dec 11 23:24:03 2024 ************************************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 1 0 0 4 5 Note: If verification succeeds you can safely ignore unaccepted guidance commands. SVF files read: test.svf default.svf SVF files produced: /home/zhangchen/Desktop/vv/formality_svf/ svf.txt 1 Formality (setup) set_svf ./ SVF set to ./default.svf ./test.svf. 1 Formality (setup) report_guidance ************************************************** Report : guidance Reference : None Implementation : None Version : O-2018.06-SP1 Date : Wed Dec 11 23:28:38 2024 ************************************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 1 0 0 4 5 Note: If verification succeeds you can safely ignore unaccepted guidance commands. SVF files read: ./default.svf ./test.svf SVF files produced: /home/zhangchen/Desktop/vv/formality_svf/ svf.txt 1 Formality (setup) set_svf -ordered ./ SVF set to ./default.svf ./test.svf. 1 Formality (setup) report_guidance ************************************************** Report : guidance Reference : None Implementation : None Version : O-2018.06-SP1 Date : Wed Dec 11 23:28:50 2024 ************************************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 1 0 0 4 5 Note: If verification succeeds you can safely ignore unaccepted guidance commands. SVF files read: ./default.svf ./test.svf SVF files produced: /home/zhangchen/Desktop/vv/formality_svf/ svf.txt 1可以注意到例2中利用了不使用-append选项会导致后续set_svf命令覆盖的特性。指定拓展名-extension选项用于指定搜索目录时的文件拓展名默认为svf。指定SVF文件和搜索目录可以指定多个SVF文件或搜索目录作为参数这两者的组合也是可以接受的。删除已加载的svf信息当使用set_svf命令不指定SVF文件和搜索目录时可以删除已加载的svf信息但最好使用remove_guidance命令删除已加载的svf信息该命令只有在读取除工艺库外的设计文件之前才能使用。注意事项只有在读取除工艺库外的设计文件之前才能使用set_svf命令否则需要使用remove_container命令将设计文件全部移除。