如何添加和加载sysnopsys的formality工具的waiver文件

在Synopsys Formality工具中，加载Waiver（豁免）文件通常用于指定针对特定规则或检查点的例外情况。以下是向Formality添加和加载Waiver文件的基本步骤：

1. **创建Waiver文件**:
- 使用文本编辑器创建一个新的纯文本文件，文件名通常包含`.waiver`后缀。例如，`my_design_waivers.waiver`.
- 在文件中，按照Formality的Waiver语法书写，每一行描述一条具体的豁免请求，包括豁免的规则ID、原因以及（如果需要）额外的详细信息。

RuleID: MyCustomRule
Reason: Special case due to legacy code
Description: This waiver applies only when the LegacyFunction is called

2. **设置路径**:
- 确保waiver文件位于Formality可以访问的位置。这可能是项目目录下的` Formality_Waivers`文件夹或其他Formality配置中指定的目录。

3. **在Formality配置中引用Waiver文件**:
- 打开Formality的工作目录或项目配置文件（如`formal.tcl`或`.formalrc`），在这里指定waiver文件的路径。通常，会有一个`add_waiver_file`命令来完成这个任务。

set ::formal::waivers [list [file normalize "[path/to/your/waiver/file]"]]

请注意，替换`[path/to/your/waiver/file]`为实际的waiver文件路径。

4. **运行Formality**:
- 完成配置后，重新运行Formality工具。Formality会在启动时自动读取并应用waiver文件中的内容。

如果你遇到具体的问题，比如waiver未生效，可能需要检查waiver语法是否正确，或者Formality的日志以获取更多信息。