Formality使用教程：加载源文件与检查RTL-GATE一致性

"Formality是一款强大的形式验证工具，用于检查RTL设计与门级网表的一致性。在本教程中，我们将学习如何加载源文件并使用Formality进行功能一致性检查。" Formality 使用指南主要涉及以下知识点： 1. **加载源文件**： 在进行形式验证时，首先需要加载RTL源代码和门级网表。在本例中，源文件是`fifo.v`，它位于`Rtl`目录下。通过点击Formality图形用户界面的`LOAD FILES`按钮，可以加载这个源文件。加载过程包括两个步骤： - **读取源文件**：选择`Rtl`目录下的`fifo.v`文件，点击`Open`按钮来打开它。 - **设置搜索目录**：确保编译器库路径正确，这样Formality才能找到相关的库文件。通常，这需要设置`DesignWareroot directory`，例如指向Synopsys的安装目录。 2. **设置Reference Design和Implementation Design**： - **Reference Design**：这是要验证的设计，通常是RTL源代码。在本教程中，将`fifo.v`设置为参考设计。 - **Implementation Design**：这是经过综合后的门级网表，对应于`fifo.vg`。这个设计代表了实际将在硬件中实现的版本。 3. **图形用户界面操作**： Formality的GUI提供了一种直观的方式来配置和执行验证任务。用户需要： - 点击`reference`按钮来设置参考设计，然后通过`ReadDesignFile`添加`fifo.v`。 - 使用`option`按钮设置Verilog读取选项，确保能够找到所有需要的库文件。 4. **形式验证的目标**： 主要目标是检查`fifo.v`的RTL描述与`fifo.vg`的门级表示是否功能一致。这一步骤对于确保硬件实现正确无误至关重要，尤其是在设计包含复杂逻辑和接口的情况下。 5. **其他目录和文件的作用**： - `Lib`目录包含了门级网表需要的技术库，例如`lsi_10k.db`，这是用于综合和形式验证的库文件。 - `Gate`目录包含未插入扫描链的门级网表，如`fifo.vg`。 - `Gate_with_scan`和`Gate_with_scan_jtag`目录分别包含插入扫描链和JTAG链的门级网表，这些是用于功能和边界扫描测试的。 6. **形式验证流程**： 一旦源文件加载并设置好参考和实施设计，用户可以通过Formality的图形界面或命令行工具执行一致性检查，确认RTL设计在转换为门级网表后仍保留其原始功能。 7. **扫描链和JTAG链**： 扫描链和JTAG链的使用允许在硬件测试阶段进行有效的故障检测和调试。`fifo_with_scan.v`和`fifo_with_scan_jtag.v`的目的是为了在形式验证过程中检查这些链的正确集成。 总结来说，Formality使用指南详细介绍了如何使用该工具加载源文件，设置参考和实施设计，并进行功能一致性检查，这对于任何进行集成电路设计的人来说都是至关重要的技能。