Formality:时序变换(五)(触发器复制)
2026/7/10 15:10:28 网站建设 项目流程

相关阅读

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 触发器复制

如图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命令。

需要专业的网站建设服务?

联系我们获取免费的网站建设咨询和方案报价,让我们帮助您实现业务目标

立即咨询