<think>我们正在讨论的是如何使用Formality工具对Verilog RTL设计和.db门级网表进行形式验证。根据引用[1][2][3]，过程分为几个关键步骤：设置参考设计（Verilog RTL）、设置实现设计（.db网表）、读入库文件、设置顶层设计、匹配和验证。具体过程如下： 1. **设置参考设计（Reference Design）**： - 首先，读入RTL设计文件（.v）。在Formality GUI中，点击“Reference”标签，然后执行“Read Design File”，选择所有相关的Verilog文件[^3]。 - 如果RTL设计中使用了Design Ware库的IP，需要设置库文件的搜索路径[^3]。 - 指定顶层模块（Set Top Design），即设计的顶层模块名。 2. **设置实现设计（Implementation Design）**： - 实现设计是.db格式的门级网表。点击“Implementation”标签，同样执行“Read Design File”，但这里文件类型应选择“Database”（或.db）[^2]。Formality能够直接读入.db格式的网表文件。 - 注意：工艺库文件（.db）通常在此步骤之前已被读入（在后续的库读入步骤）。 3. **读入库文件（DB Libraries）**： - 无论是在Reference还是Implementation设置中，都需要读入库文件（DB Libraries）。这些库文件包含工艺库中标准单元（如与门、触发器）的功能模型[^3]。这一步确保网表中使用的每个标准单元都定义正确。 4. **设置SVF文件（可选但推荐）**： - SVF（Setup Verification File）由综合工具（如Design Compiler）生成，记录了综合过程中的优化步骤（如寄存器重命名、常量传播）。读入SVF文件可以帮助Formality正确匹配参考设计和实现设计的关键点[^1]。 5. **设置顶层设计和环境（Set Top and Setup）**： - 分别对参考设计和实现设计设置顶层模块名（必须一致）。 - 执行“Setup”操作，检查设计的完整性与一致性。 6. **匹配和验证（Match and Verify）**： - 执行“Match”操作：Formality自动尝试匹配参考设计和实现设计中的关键点（如寄存器和输入输出端口）。如果有SVF文件，匹配将更准确[^1]。 - 执行“Verify”操作：对匹配点之间的组合逻辑锥进行形式化等价验证（等价关系）。验证的核心方法： - 每个比较点建立输入约束集合$\Phi$ - 证明：$\forall i \in \Phi, f_{ref}(i) = f_{impl}(i)$ - 满足上述条件的验证点标记为"Verified"，否则为"Failed" - 验证算法通常使用基于SAT求解器或BDD的技术。 7. **查看报告**： - 验证完成后，查看报告（通常为绿色表示成功，红色为失败）。报告包括成功/失败的验证点数量、未验证点的原因分析。 ### 过程总结 ```mermaid graph LR A[设置参考设计] --> A1[读入RTL(.v)] B[设置实现设计] --> B1[读入.db网表] C[读入库文件] --> C1[工艺库.db] D[设置顶层设计] E[匹配] --> E1[使用SVF指导] F[验证] --> F1[逻辑锥等价性证明] A --> D B --> D C --> A & B D --> E E --> F ``` > **注意事项**: > 1. RTL和.db网表的顶层模块名必须相同。 > 2. 工艺库（.db）的版本必须与综合时保持一致，否则会引起单元功能不匹配。 > 3. 如果验证失败，Formality会提供反例波形（Counterexample），帮助定位差异点[^1]。 > 4. 异步路径可能需要添加额外约束，否则可能导致验证失败。 ### 相关问题§§ 1. Formality验证失败通常有哪些原因？ 2. 如何处理Formality验证中的时序约束？ 3. SVF文件在Formality验证中的作用是什么？ 4. Formality验证中常见的报告结果如何解读？ </think> ### Verilog与.db文件进行Formality验证的具体过程 Formality验证通过形式化方法证明RTL设计(Verilog)与门级网表(.db)功能等价，无需仿真。具体步骤如下： #### 1. 设置参考设计 (Reference Design) - **读入Verilog文件**：加载RTL设计文件 ```tcl read_verilog -container r -lib WORK {design.v} ``` - **指定顶层模块**：设置RTL顶层模块名 ```tcl set_top r:/WORK/top_module ``` - **处理特殊库**：若使用DesignWare IP需添加搜索路径[^3] #### 2. 设置实现设计 (Implementation Design) - **载入.db门级网表**：读取综合后的门级设计 ```tcl read_db -container i {gate_level.db} ``` - **指定匹配顶层**：命名必须与参考设计一致 ```tcl set_top i:/WORK/top_module ``` #### 3. 加载工艺库 - **读入标准单元库**：提供门级单元的功能定义 ```tcl read_db -container both {std_cell_library.db} ``` - 关键约束：工艺库版本必须与综合时完全一致[^1] $$ \text{lib\_version}_{\text{Formality}} \equiv \text{lib\_version}_{\text{Synthesis}} $$ #### 4. 导入SVF文件 (可选但推荐) - 加载综合转换记录文件： ```tcl set_svf -file synthesis.svf ``` - **解决重命名问题**：映射合成器优化的寄存器/端口，例如： - RTL: `reg [7:0] counter` - 网表: `counter_reg[7]` → SVF记录此映射关系[^1] #### 5. 建立等价模型 - **设计设置**：检查设计完整性 ```tcl setup ``` - **关键点匹配**：自动对齐寄存器和主I/O ```mermaid graph LR RTL[寄存器counter] --匹配--> Netlist[counter_reg] RTL[输入clk] --匹配--> Netlist[CTS_clk] ``` #### 6. 执行验证 - **逻辑锥等价证明**：比较组合逻辑功能 ```tcl verify ``` 数学原理：对于匹配点$n$，验证其驱动逻辑锥满足 $$ \forall \text{输入向量 } \vec{x}, \; f_{\text{RTL}}(\vec{x}) = g_{\text{门级}}(\vec{x}) $$ - **验证算法**：使用SAT或BDD求解器判断组合逻辑是否等价 #### 7. 结果分析 - **报告解读**： - **绿色标志**：所有点验证通过 - **红色标志**：存在不等价点（附带反例波形） - **常见错误处理**： ```mermaid graph TB 失败原因 --> 缺少SVF --> 重新生成SVF 失败原因 --> 时钟约束缺失 --> 添加set_case_analysis 失败原因 --> 工艺库版本冲突 --> 统一工具版本 ``` > ⚠️ **关键要求**： > 1. RTL与网表保持严格相同的顶层模块名 > 2. 工艺库必须包含所有实例化单元的功能模型 > 3. 推荐添加`set_zero_delay`将时序检查降低为纯组合验证[^1] 完整脚本示例： ```tcl set_top r:/WORK/top read_db -container r -lib WORK design.v set_top i:/WORK/top read_db -container i syn_output.db read_db -container both tech_28nm.db set_svf synthesis.svf setup verify ``` ### 相关问题