问题描述
Q1） Xilinx是否支持等效性检查和模型检查？
Q2）什么是形式验证？
Q3）为什么Xilinx支持等效性检查？
Q4） Xilinx何时支持模型检查？
Q5）等效性检查是否取代仿真？
Q6）我什么时候应该使用等效性检查？
Q7） Xilinx是否支持XST后流？
Q8）如何使用等效性检查获益？
Q9） Xilinx支持哪些供应商？
Q10）关于支持相关问题，我应该联系谁？
Q11）是否有任何Xilinx应用笔记讨论流程？
Q12）流程是否适用于所有语言？
Q13）支持哪些平台？
Q14）如何使用等效性检查将FPGA重新定位到ASIC？
Q15） Xilinx提供哪些库？
Q16）在哪里可以找到支持的形式验证工具的形式验证库？
解决/修复方法
Q1）Xilinx是否支持等效性检查和模型检查？
A1 ）Xilinx仅支持当前ISE软件中的等效性检查。
Q2）什么是形式验证？
A2 ）形式验证是一种基于算法的逻辑验证方法，可以详尽地证明设计的功能特性。
通常，有两种类型的形式验证，如下所示：
等价检查
验证处于相同或不同抽象级别的两个设计的功能等效性（例如，RTL到RTL，RTL到门或门到门）。
等效性检查用于设计实现验证。
模型检查
验证实现是否满足设计的属性。
在设计创建阶段的早期使用模型检查来发现功能性错误。
Q3）为什么Xilinx支持等效性检查？
A3 ）随着器件尺寸和复杂性的增加，功能仿真对于测试平台生成和仿真运行时都变得非常耗时。
正式验证很有吸引力，因为它的运行时间很短，并且具有完整的功能覆盖。
此外，形式验证是ASIC设计环境中经过验证的技术/流程。
随着越来越多的ASIC设计人员使用FPGA进行设计，形式验证成为设计中更重要的流程。
Q4）Xilinx何时支持模型检查？
A4 ）模型检查不是一项成熟的技术，客户接受度非常慢，因为每个供应商都有自己的专有属性描述语言。
当建立用于描述设计属性的单一标准语言时，可以增加采用该技术。
Xilinx将根据客户需求评估对模型检查的支持。
Q5）等效性检查是否取代仿真？
A5 ）等效性检查增强了功能仿真。
对于数百万门设计，等效检查是唯一可行的解决方案，因为仿真运行可能需要数天或数周才能完成。
此外，仿真设计的覆盖范围还不完整;等效检查提供100％覆盖率，在仿真所需时间的一小部分内没有测试向量。
Q6）我什么时候应该使用等效性检查？
A6 ）您应该在整个FPGA实现流程中使用等效性检查。
您可以使用它来验证设计重新优化，综合以及根据黄金RTL模型布置和布线结果。
Q7）Xilinx支持XST后流吗？
A7 ）不。
Q8）如何使用等效性检查获益？
A8 ）等效性检查可帮助您更快地验证设计。
它有助于确保最终网表中的功能与黄金RTL设计规范相匹配。
等效性检查还可以帮助您更有效地隔离和调试问题。
Q9）Xilinx支持哪些供应商？
A9 ）ISE Design Suite支持以下供应商：
Synopsys形式：
Cadence Conformal LEC：
Mentor Graphics Formal Pro（由供应商直接支持）：
Vivado支持OneSpin和Cadence Encounter Conformal上的Vivado 2018.1。
Q10）关于支持相关问题，我应该联系谁？
A10 ）对于工具和流程问题：
Synopsys形式：
Cadence Conformal：
http://www.cadence.com/support/
证明eCheck：
http://www.prover.com/contact/
对于库问题：
Xilinx支持：
https://www.xilinx.com/support.html#serviceportal
Q11）是否有任何Xilinx应用笔记讨论流程？
A11 ）关于形式验证的所有Xilinx应用笔记现已过时。
有关使用形式验证的信息，请参阅以下内容：
Cadence Conformal 🙁 Xilinx答复20617）
Prover eCheck 🙁 Xilinx答案20685）
Q12）流程是否适用于所有语言？
A12 ）RTL级别：可以是VHDL或Verilog;联系正式验证供应商以获取更多信息。
门级：Xilinx仅支持Verilog流。
Q13）支持哪些平台？
A13 ）支持以下平台：
Synopsys Formality
Sun OS Unix *：是的
Linux Enterprise Edition *：是的
Windows XP / 2000 *：没有
Cadence Conformal
Sun OS Unix *：是的
Linux Enterprise Edition *：是的
Windows XP / 2000 *：没有
证明eCheck
Sun OS Unix *：是的
Linux Enterprise Edition *：是的
Windows XP / 2000 *：是的
*仅限Xilinx ISE支持的版本
Q14）如何使用等效性检查将FPGA重新定位到ASIC？
A14 ）您可以使用以下两种方法之一将FPGA重新定位到ASIC：
- RTL-to-Gate：如果FPGA和ASIC的源RTL相同，则使用此方法。
- FPGA Gate-to-ASIC Gate：使用此方法将FPGA门级网表与ASIC门级网表进行比较。
注意：有关这些流程的更多信息，请直接与正式验证供应商联系。
Q15）Xilinx提供哪些库？
A15 ）Xilinx提供以下两个用于形式验证的库：
- UNISIM库* – 用于具有用于RTL实例化的特定于技术的实例化单元的设计。
- SimPrim Library * – 用于后NGDBuild和后置和布线网表。
*这些与Xilinx提供的仿真库不同。
Q16）在哪里可以找到支持的形式验证工具的形式验证库？
A16 ）对于旧的ISE版本，请参阅以下位置的CAE供应商库产品：
http://www.xilinx.com/support/download/index.htm#tab-cl
从ISE Design Suite的12.1版本开始，这些库随软件一起提供。
这些文件可以在以下位置获得：$ XILINX / verilog / xeclib /。
Vivado交付的库可以在$ XILINX_VIVADO / data / verilog / src / xeclib /下获得。
没有回复内容