相关阅读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_merging命令或compile_enable_register_merging变量改变。等价即触发器的状态在任何情况下都是相同的反向等价触发器的状态在任何情况下都是不同的本文只讨论等价情况反向等价的分析是相同的随后在SVF文件中添加guide_reg_merging命令当Formality处理SVF文件时将会确认guide_reg_merging命令的有效性如果有效则将指定的触发器进行合并。三、可能会出现的问题问题1guide_reg_merging命令被Formality拒绝。解决方案1使用report_svf_operation -status rejected -command reg_merging命令查看被拒绝的guide_reg_merging命令。此时一般有两种情况1、Formality提示Cannot find master reference cell即找不到指定的触发器这时候应该检查SVF文件中是否有改变了触发器名字的命令以及其他有关名字的设置。2、Formality提示Could not verify SVF merged register即不认为是可以合并的触发器这时候可以使用verify命令进行单点验证用probe探针也可模式窗口中会给出Formality不认为触发器可以合并的原因。问题2参考设计中存在未匹配的触发器。解决方案2使用report_unmatched_points命令查看如果是因为触发器合并失败该触发器驱动的所有比较点可能都失败且失败的模式中应当合并的触发器的值相反对于反相等价则是相同。如果已使用verify命令进行验证可以使用analyze points -fail命令分析失败的比较点但这是验证后的调试方式。四、绕开SVF文件当本应合并的触发器因为未使用SVF文件等原因没有正确合并时可以使用set_constraint coupled/mutex命令进行设置需要注意的是该命令并不会验证设置是否与真实情况一致也就是说如果两个不应该合并的触发器被set_constraint coupled/mutex命令错误地设置会导致验证错误。手动使用guide_reg_merging命令也是可以的但Formality会确认其有效性。需要注意的是无法使用set_user_match命令将参考设计中的两个触发器与实现设计中的一个触发器匹配。五、示例例1 触发器合并// 参考设计 module merge(input a, clk, output z1, z2); reg a_r1, a_r2; assign z1 a_r1; assign z2 a_r2; always (posedge clk) begin a_r1 a; a_r2 a; end endmodule // 实现设计需要使用compiler_ultra命令 module merge( a, clk, z1, z2 ); input a, clk; output z1, z2; wire z1; assign z2 z1; DFFQXL a_r1_reg ( .D(a), .CK(clk), .Q(z1) ); 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 1(0) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs ---------------------------------------------------------------------------------------- Unmatched Objects REF IMPL ---------------------------------------------------------------------------------------- Registers 1 0 DFF 1 0 ****************************************************************************************此时的验证失败总共有两个失败点首先是参考设计中存在未匹配的触发器其次是比较点z2失败。********************************* Verification Results ********************************* Verification FAILED ------------------- Reference design: r:/WORK/merge Implementation design: i:/WORK/merge 2 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 1 1 0 2 Failing (not equivalent) 0 0 0 0 1 0 0 1 **************************************************************************************** Info: Try the analyze_points command to see if Formality can determine potential causes, or suggest next steps for a FAILED or INCONCLUSIVE verification. See the man page for analyze_points usage and options. Info: Formality Guide Files (SVF) can improve verification success by automating setup.其中比较点z2失败的模式如图4所示其中参考设计和实现设计的触发器值是相反的即一个是1另一个就是0。图4 失败的模式假设手动使用guide_reg_merging命令使用SVF文件也可例1的SVF处理结果如下所示。***************************** Guidance Summary ***************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- reg_merging : 1 0 0 0 1图5为SVF处理后(match命令可以完成这一点)的参考设计原理图。图5 参考设计处理后的原理图此时的验证结果如下所示可以看出验证成功了。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/merge Implementation design: i:/WORK/merge 3 Passing compare points ---------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL ---------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 2 1 0 3 Failing (not equivalent) 0 0 0 0 0 0 0 0 ****************************************************************************************六、写在最后Design Compielr中Multibit优化的合并过程与触发器合并类似此时Design Compiler会在SVF文件中添加guide_multibit命令。