相关阅读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文件失效时进行调试不是所有时序变换都会记录在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命令的有效性如果有效这里指的是命名相关的有效性而不是功能相关则将在指定的触发器输入输出添加反相器以便于验证。三、可能会出现的问题问题1guide_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 ****************************************************************************************