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文件失效时进行调试。

本文将详细阐述时序变换中的触发器复制。

二、触发器复制

如图1所示，在某些情况下，Design Compiler可能为了性能而复制触发器（可通过set_register_replication命令或compile_register_replication变量（对于拓扑模式）设置），随后在SVF文件中添加guide_reg_duplication命令；当Formality处理SVF文件时，将会确认guide_reg_duplication命令的有效性，如果有效（这里指的是命名相关的有效性，而不是功能相关）则将指定的触发器进行复制。

三、可能会出现的问题

问题1：guide_reg_duplication命令被Formality拒绝。

解决方案1：使用report_svf_operation -status rejected -command reg_duplication命令查看被拒绝的guide_reg_duplication命令。如果Formality提示"Cannot find reference cell"，即找不到指定的触发器，这时候应该检查SVF文件中是否有改变了触发器名字的命令以及其他有关名字的设置。

问题2：实现设计中存在未匹配的触发器。

解决方案2：使用report_unmatched_points命令查看，如果是因为触发器复制失败，则该触发器驱动的所有比较点可能都失败，且失败的模式中应当复制的触发器的值相反。如果已使用verify命令进行验证，可以使用analyze points -fail命令分析失败的比较点，但这是验证后的调试方式。

四、绕开SVF文件

当本应复制的触发器因为未使用SVF文件等原因没有正确合并时，可以使用set_user_match命令进行设置，需要注意的是，该命令并不会验证设置是否与真实情况一致，也就是说如果一个不应该复制的触发器被set_user_match命令错误地设置，会导致验证错误。手动使用guide_reg_duplication命令也是可以的，Formality不会确认其有效性。

五、示例

例1 触发器复制

// 参考设计 module duplication(a, clk, z1, z2); input a, clk; output z1, z2; reg a_r1; assign z1 = a_r1; assign z2 = a_r1; always @(posedge clk) begin a_r1 <= a; end endmodule // 实现设计 module duplication( a, clk, z1, z2 ); input a, clk; output z1, z2; DFFQXL a_r1_reg ( .D(a), .CK(clk), .Q(z1) ); DFFQXL a_r1_reg_rep1 ( .D(a), .CK(clk), .Q(z2) ); endmodule

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

图2 参考设计的原理图

图3 实现设计的原理图

例1的匹配结果如下所示，可以看出实现设计中存在一个未匹配的比较点。

*********************************** Matching Results *********************************** 3 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(1) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs ---------------------------------------------------------------------------------------- Unmatched Objects REF IMPL ---------------------------------------------------------------------------------------- Registers 0 1 DFF 0 1 ****************************************************************************************

此时的验证失败， 被复制的触发器驱动的输出端口z2验证失败，如下所示。

********************************* Verification Results ********************************* Verification FAILED ------------------- Reference design: r:/WORK/duplication Implementation design: i:/WORK/duplication 2 Passing compare points 1 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 1 1 0 2 Failing (not equivalent) 0 0 0 0 1 0 0 1 ****************************************************************************************

其中比较点z2失败的模式如图4所示，其中参考设计和实现设计的触发器值是相反的，即一个是1，另一个就是0。

图4 失败的模式

假设手动使用guide_reg_duplication命令（使用SVF文件也可），例1的SVF处理结果如下所示。

***************************** Guidance Summary ***************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- reg_duplication : 1 0 0 0 1

图5为SVF处理后(match命令可以完成这一点)的参考设计原理图。

图5 参考设计处理后的原理图

此时的验证结果如下所示，可以看出验证成功了。

********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/duplication Implementation design: i:/WORK/duplication 4 Passing compare points ---------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL ---------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 2 2 0 4 Failing (not equivalent) 0 0 0 0 0 0 0 0 ****************************************************************************************

六、写在最后

Design Compielr中Multibit优化的解组过程与触发器复制类似，此时Design Compiler会在SVF文件中添加guide_multibit命令。