Formality：时序变换（三）（相位反转）

相关阅读

Formalityhttps://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文件失效时进行调试（不是所有时序变换都会记录在SVF文件中，比如时钟门控(Clock Gating)）。

本文将详细阐述时序变换中的相位反转。

二、相位反转

图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) begin result <= !a; end endmodule // 实现设计 module inv_push(input a, clk, output z); reg result; assign z = !result; always @ (posedge clk) begin result <= a; end endmodule

对于例1，需要注意的是为了便捷，这里选择了等效的RTL描述作为实现设计，一般情况下，实现设计是综合后的网表。

下面的图2是参考设计的原理图，图3是实现设计的原理图。

图2 参考设计的原理图

图3 实现设计的原理图

例1的匹配是没有问题的，因为并没有影响比较点的数量和名字，如下所示。

*********************************** Matching Results *********************************** 2 Compare points matched by name 0 Compare points matched by signature analysis 0 Compare points matched by topology 2 Matched primary inputs, black-box outputs 0(0) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs ****************************************************************************************

但是验证却失败了，比较点result_reg以及其驱动的输出端口z全部验证失败，如下所示。

********************************* Verification Results ********************************* Verification FAILED ------------------- Reference design: r:/WORK/inv_push Implementation design: i:/WORK/inv_push 0 Passing compare points 2 Failing compare points 0 Aborted compare points 0 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_push Implementation design: i:/WORK/inv_push 2 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 ****************************************************************************************