Formality:时序变换(五)(触发器复制)

📅 2026/7/10 15:10:40
Formality:时序变换(五)(触发器复制)
相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.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 Compilerset_svf命令以及SVF文件简介一文但对这些时序变换的了解有助于在不使用SVF文件时进行设置和在SVF文件失效时进行调试。本文将详细阐述时序变换中的触发器复制。二、触发器复制​图1 触发器复制如图1所示在某些情况下Design Compiler可能为了性能而复制触发器可通过set_register_replication命令或compile_register_replication变量对于拓扑模式设置随后在SVF文件中添加guide_reg_duplication命令当Formality处理SVF文件时将会确认guide_reg_duplication命令的有效性如果有效这里指的是命名相关的有效性而不是功能相关则将指定的触发器进行复制。三、可能会出现的问题问题1guide_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命令。