描述
OneSpin 工具可验证综合和实现过程（即 RTL 和综合网表）中任意两个步骤之间的功能等效性
本答复记录涵盖有关 OneSpin 支持版本的详细信息，以及设置 OneSpin 以测试 Vivado 综合生成的网表的基本流程。
解决方案
OneSpin 支持 Vivado 生成的网表文件 (.v/.vhd)，该文件可作为等效校验的输入。
注：在调用以下命令前，您必须先安装 OneSpin：
请在 Linux 环境中使用“onespin”命令调用该工具。
对于 Windows，请使用 $ONESPINROOT\bin\onespin.bat 或点击 OneSpin 图标快捷方式。
OneSpin 工具需要一个“黄金”文件作为参考，才能交叉检查所生成的“修订”网表文件的功能性。
黄金文件可以使用“read_*”命令获得：
对于 VHDL 和 VHDL 2008 文件：
read_vhdl -version <87|93|2002|2008> -golden reference_file_name.vhd
对于 Verilog 和 SystemVerilog 文件：
read_verilog -version <1995|2001|sv2005|sv2009|sv2012> -golden revised_file_name.v
在 Vivado 中综合或实现后，可使用 write_verilog/write_vhdl 生成修订文件。
在项目模式下，打开综合／实现的设计，并在 Tcl 控制台中使用 write_verilog/write_vhdl 命令生成一个 Verilog(.v) 网表文件或 VHDL(.vhd) 网表文件。
在非项目流程中，使用 open_checkpoint 命令将设计加载到内存中，然后使用 write_verilog/write_vhdl 命令转储 RTL 网表。
修订的文件可以使用“read_*”命令获得：
read_vhdl -revised filename_vhdl_netlist.vhd
read_verilog -revised filename_verilog_netlist.v
使用帮助“type_command”获取该命令的详情及句法信息。
例如，在 shell 中键入帮助“read_vhdl”，可获得有关 read_vhdl 命令的详细信息。
随附的 Tcl 文件显示了一个示例和示例命令，其可用于形式等效校验。
注：更多高级用法和支持相关查询，请联系 OneSpin 支持，并参考以下链接，获得更多详情：
https://www.onespin.com/products/360-ec-fpga/。
OneSpin 360 (2019.2.1) 是 Vivado 2019.1 支持的版本。
查看 Vivado 版本说明 (UG973)，在“兼容的第三方工具”下获得支持的 OneSpin 版本。
