相关阅读
Formality
https://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
svf文件的全称是Setup Verification for Formality，即Design Compiler提供给Formality的设置验证文件，它的作用是为Formality的指导模式(Guidance)和设置模式(Setup)提供信息，以帮助其更好地理解和处理设计流程中因使用Design Compiler而引起的设计变更的一种机制。
svf文件的详细介绍和生成命令在下面的博客中已经讨论，本文主要讨论Formality中的set_svf命令。
Design Compiler：set_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?spm=1001.2014.3001.5501 set_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文件，也可以在Formality工作目录中的formality_svf子目录中找到svf.txt文件，它是已加载的svf文件的文本可读形式（但它们两者只能查看加载的svf文件中的guide类命令，而无法查看用户执行的guide类命令）。
指定顺序
-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信息（不包括用户执行的guide类命令）。但是，最好使用 remove_guidance命令删除已加载的svf信息。
注意事项
只有在读取除工艺库外的设计文件之前才能使用set_svf命令，否则需要使用remove_container命令将设计文件全部移除。
