61I形式验证-我是否可以使用等价性检查来将FPGA重新定位为ASIC？如果是这样，怎么办？

描述

一般描述：

我可以使用等价性检查来将FPGA重新定位为ASIC吗？如果是这样，怎么办？

解决方案

当您从一个技术到另一个目标时，可以用两种方式使用等价性检查：

方法1：RTL与门

如果源RTL对于FPGA和ASIC都是相同的，则可以执行RTL对ASIC进行门检查。（此流程不需要正式的验证工具来支持FPGA流。）

如果使用此方法，则状态机编码差异可能是有问题的。从RTL代码读取FSM描述的综合和形式化验证工具可以对FSM进行不同编码。例如，综合可以使用一个热编码方法，而等效性检查工具使用二进制编码。编码FSM的这些差异可能导致验证失败，除非指示等效性检查工具使用相同的一个热编码方案。

方法2：FPGA门到ASIC门

如果要将FPGA门级网表与ASIC门级网表进行比较，请使用此方法。（Xilinx尚未验证此流程，建议与您的正式验证工具供应商联系以获取其他信息。）

由于ASIC和FPGA技术原语可能存在差异，因此此流程可能无法成功执行等价性检查。例如，如果设计使用RAM、Mult18x18s和SRL16s，则如果ASIC技术没有完全相同的原语，则这些工具可能无法验证这些功能。如果两个NETLIST是由同一RTL创建的，则流程不起作用。

ASIC和FPGA综合工具可以使用不同的顺序优化（例如，重新定时等）和不同的技术库来综合RTL代码。相应的门级网表可以具有非常不同的比较点（触发器和顺序元件的数目），这导致等效性检查工具失败。

注意：如果使用的是从同一源RTL创建的NETLIST，Xilinx建议使用方法1。

有关相关的黄金时段信息，请参阅以下答案记录：

（赛灵思解答12802）“什么是形式验证？”

（赛灵思解答12803）“什么样的用户会对正式的验证流程感兴趣？”

（赛灵思解答12804）“Xilinx支持等价性检查和模型检查吗？”

（赛灵思解答12805）“Xilinx是否支持RTL到RTL、RTL到GATE或门到门的等效性检查？”

（赛灵思解答12806）“为什么Xilinx支持等价性检查？”

（赛灵思解答12807）“Xilinx计划支持模型检查吗？”

（赛灵思解答12808）-“等效检查是否代替仿真？”

（赛灵思解答12809）-“我应该什么时候使用等价性检查？”

（赛灵思解答12810）“我如何从使用等价性检查中获益？”

（赛灵思解答12812）“哪些等价性检查工具供应商支持Xilinx？”

（赛灵思解答12813）“Xilinx支持哪些平台？”

（赛灵思解答12814）-我是一个正式的客户。我与谁联系支持相关问题？”

（赛灵思解答12815）-“关于验证流的应用笔记可用吗？”

（赛灵思解答12816）-“验证流的局限性是什么？”

（赛灵思解答12817）“验证流程是否与SyopSoopFCII、Synplicity Synplify和Mentor Leonardo频谱综合工具一起工作？”

（赛灵思解答12818）“验证流程是否与所有语言一致？”

（赛灵思解答12820）-“谁供应库？”

（赛灵思解答12821）“Xilinx提供哪些库？”

（赛灵思解答12822）-“如何安装Xilinx应用程序注释411引用的库？”

（赛灵思解答12823）-“Xilinx产品家族的支持是什么？”