相关阅读
Formality
https://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
一、引言
时序变换在Design Compiler的首次综合和增量综合中都可能发生，它们包括：时钟门控(Clock Gating)、寄存器合并(Register Merging)、寄存器复制(Register Replication)、常量寄存器移除(Constant Register Removal)、不可读寄存器移除(Unread register removal)、流水线重定时(Pipeline Retiming)、自适应重定时(Adaptive Retiming)、相位反转(Phase Inversion)、多比特寄存器组(Multibit Banking)。
合适的时序变换越多，就能获得更好的结果质量(QoR)，但时序变换会无法避免地造成等价性检查的困难，因为这改变了逻辑锥的结构。虽然使用SVF文件能够解决大部分的问题（关于SVF文件的介绍，参考Design Compiler：set_svf命令以及svf文件简介一文），但对这些时序变换的了解有助于在不使用SVF文件时进行设置和在SVF文件失效时进行调试。
本文将详细阐述时序变换中的相位反转。
二、相位反转
图1 相位反转的综合
如图1所示，在综合过程中，Design Compiler可能为了性能或面积将反相器移动并穿过寄存器边界（可以使用compile_seqmap_enable_output_inversion变量禁止（对于compile命令）或者-no_seq_output_inversion选项禁止（对于compile_ultra命令）），随后在SVF文件中添加guide_inv_push命令；当Formality处理SVF文件时，将会确认guide_inv_push命令的有效性，如果有效（这里指的是命名相关的有效性，而不是功能相关）则将在指定的寄存器输入输出添加反相器以便于验证。
三、可能会出现的问题
问题1：guide_inv_push命令被Formality拒绝。
解决方案1：使用report_svf_operation -status rejected -command inv_push命令查看被拒绝的guide_inv_push命令。如果Formality提示"Cannot find register"，即找不到指定的寄存器，这时候应该检查SVF文件中是否有改变了寄存器名字的命令以及其他有关名字的设置。
问题2：某个寄存器以及其驱动的所有比较点都验证失败，如果该寄存器拥有异步复位/置位，则该操作是一种失败的模式。
解决方案2：检查是否使用SVF文件或者手动使用guide_inv_push命令，使用set_inv_push命令进行设置或使用set_user_match -inverted进行反相匹配也是一种解决方案。需要注意的是，Formality并不会验证是否真的发生了相位反转，因此不正确的设置会导致验证错误。
四、示例
例1 相位反转
// 参考设计
module inv_push (input a, clk, output z);
reg result;assign z = result;
always @ (posedge clk) beginresult <= !a;
endendmodule// 实现设计
module inv_push (input a, clk, output z);
reg result;assign z = !result;
always @ (posedge clk) beginresult <= a;
endendmodule对于例1，需要注意的是为了便捷，这里选择了等效的RTL描述作为实现设计，一般情况下，实现设计是综合后的网表。
下面的图2是参考设计的原理图，图3是实现设计的原理图。
图2 参考设计的原理图
图3 实现设计的原理图
例1的匹配是没有问题的，因为并没有影响比较点的数量和名字，如下所示。
*********************************** Matching Results ***********************************2 Compare points matched by name0 Compare points matched by signature analysis0 Compare points matched by topology2 Matched primary inputs, black-box outputs0(0) Unmatched reference(implementation) compare points0(0) Unmatched reference(implementation) primary inputs, black-box outputs
****************************************************************************************但是验证却失败了，比较点result_reg以及其驱动的输出端口z全部验证失败，如下所示。
********************************* Verification Results *********************************
Verification FAILED
-------------------Reference design: r:/WORK/inv_pushImplementation design: i:/WORK/inv_push0 Passing compare points2 Failing compare points0 Aborted compare points0 Unverified compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 0 0 0 0
Failing (not equivalent) 0 0 0 0 1 1 0 2
****************************************************************************************其中比较点result_reg失败的模式如图4所示，其中参考设计和实现设计的寄存器行为是相反的，即一个读取1，另一个就读取0。
图4 失败的模式
假设手动使用guide_inv_push命令（使用SVF文件也可），例1的SVF处理结果如下所示。
***************************** Guidance Summary *****************************Status
Command Accepted Rejected Unsupported Unprocessed Total
----------------------------------------------------------------------------
inv_push : 1 0 0 0 1图5为SVF处理后(match命令可以完成这一点)的参考设计原理图。
图5 参考设计处理后的原理图
此时的验证结果如下所示，可以看出验证成功了。
********************************* Verification Results *********************************
Verification SUCCEEDED
----------------------Reference design: r:/WORK/inv_pushImplementation design: i:/WORK/inv_push2 Passing compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 1 1 0 2
Failing (not equivalent) 0 0 0 0 0 0 0 0
****************************************************************************************
