Formality指南：设置SCAN链的功能无效和Formality使用教程

设置SCAN链的功能无效-Formality使用指南 Formality是一种形式验证工具，用于检查RTL与GATE网表的正确性。本文档将指导读者如何使用Formality来检查RTL与GATE网表，并设置SCAN链的功能无效。 一、检查RTL与GATE网表 在Formality中，读者需要检查RTL源代码fifo.v和门级网表fifo.vg的功能一致性。为此，读者需要设置RTL源代码fifo.v为referencedesign，并设置门级网表fifo.vg为Implementationdesign。 （一）图形用户界面进行形式验证 在UNXI提示符下，输入fm（或formality），进入tutorial目录。在Formality图形界面中，点击reference按钮，进入ReadDesignFile对话框。在对话框中，选择Rtl目录下的fifo.v文件，点击Open按钮，打开fifo.v源代码。然后，点击option按钮，出现setverilogreadoption对话框。在对话框中，选择Variable，在DesingWareroot directory(hdlin_dwroot)输入：echo $SYNOPSYS，或者输入DesignCompiler的安装目录（本工作站的目录为/opt/tools/synopsys）。 二、设置SCAN链的功能无效 在Formality中，读者需要设置SCAN链的功能无效。为此，读者需要选择Implementation，选择Instance的顶层fifo，在顶层fifo的ports目录下面搜索找到名为test_se（SCAN功能的使能信号）的管脚。在Constant Value中选择值0，设置test_se的值为0，点击OK按钮。 三、Formality使用指南 Formality提供了一个图形用户界面，读者可以通过该界面来检查RTL与GATE网表的正确性。Formality还提供了多种功能，例如检查GATE网表和插入扫描链的GATE网表，检查带有扫描链和JTAG链的GATE网表和插入扫描链的GATE网表等。 四、FiFo的Tutorial目录结构 FiFo的Tutorial目录下包含以下几个子目录： * Rtl：fifo的RTL源代码；包含fifo.v,gray_counter.v,push_ctrl.v,gray2bin.v,pop_ctrl.v,rs_flop.v。 * Lib：门级网表需要的技术库；包含lsi_10k.db。 * Gate：综合的门级网表；包含fifo.vg和fifo_mod.vg。 * Gate_with_scan：插入扫描链的门级网表；包含fifo_with_scan.v。 * Gate_with_scan_jtag：带有扫描链和JTAG链的门级网表；包含fifo_with_scan_jtag.v。 五、结论 Formality是一种功能强大的形式验证工具，读者可以使用Formality来检查RTL与GATE网表的正确性，并设置SCAN链的功能无效。通过本文档，读者可以了解Formality的使用方法，并掌握Formality的基本功能。