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文件失效时进行调试不是所有时序变换都会记录在SVF文件中比如时钟门控(Clock Gating)。本系列将分多篇文章对这些时序变换分别进行介绍。二、常量触发器移除图1 常量触发器的综合如图1所示当Design Compiler识别到常量触发器后默认情况下它会将其从设计中移除并直接传播常量逻辑可通过compile_seqmap_propagate_constants变量或set_constant_register_removal、set_compile_directives命令改变随后在SVF文件中添加guide_reg_constant命令当Formality处理SVF文件时将会确认guide_reg_constant命令的有效性如果有效则将参考设计中指定的触发器识别为常量触发器这有时很重要因为参考设计中一般不允许出现未匹配的非常量触发器在某些简单的设计中甚至无需SVF文件Formality也能正确识别常量触发器。关于Design Compiler中常量触发器移除的更多细节可以参考下面的博客。Design Compiler常量触发器的移除https://chenzhang.blog.csdn.net/article/details/157099522?spm1001.2014.3001.5502三、可能会出现的问题问题1guide_reg_constant命令被Formality拒绝。解决方案1使用report_svf_operation -status rejected -command reg_constant命令查看被拒绝的guide_reg_constant命令。此时一般有两种情况1、Formality提示Cannot find master reference cell即找不到指定的常量触发器这时候应该检查SVF文件中是否有改变了触发器名字的命令以及其他有关名字的设置。2、Formality提示Could not verify SVF constant register即不认为是一个常量触发器这时候可以使用verify *** -constant0/1命令进行验证模式窗口中会给出Formality不认为是一个常量触发器的原因。问题2参考设计中存在未匹配的触发器。解决方案2使用report_unmatched_points命令查看如果未匹配的触发器已被识别为常量触发器则无需任何操作如果未匹配的触发器没有被识别为常量触发器该触发器驱动的所有比较点可能都失败且失败的模式中该触发器的值应该与期望的常量值相反。如果已使用verify命令进行验证可以使用analyze points -fail命令分析失败的比较点但这是验证后的调试方式。四、绕开SVF文件当本应识别为常量触发器的触发器因为未使用SVF文件等原因没有正确识别时可以使用set_constant命令进行设置需要注意的是该命令并不会验证设置是否与真实情况一致也就是说如果一个非常量触发器被set_constant命令错误地设置为常量触发器会导致验证错误。手动使用guide_reg_constant命令也是可以的但Formality会确认其有效性。五、示例例1 简单的常量触发器无需使用SVF文件和用户设置// 参考设计 module constant(input a, b, clk, output reg z); reg b_r; always(posedge clk) begin z a | b_r; b_r b ^ b; // 总是0 end endmodule // 实现设计 module constant( a, b, clk, z ); input a, b, clk; output z; wire N0; assign N0 a; DFFQXL z_reg ( .D(N0), .CK(clk), .Q(z) ); endmodule例1的匹配结果如下所示其中Constrianed 0X表示该常量触发器只能在0和X之间取值X是触发器的初始状态。*********************************** 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 1(0) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs ---------------------------------------------------------------------------------------- Unmatched Objects REF IMPL ---------------------------------------------------------------------------------------- Registers 1 0 Constrained 0X 1 0 ****************************************************************************************例1的验证结果如下所示可以看到即使参考设计中出现了未匹配的触发器但由于其被识别为常量触发器因此验证成功。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/constant Implementation design: i:/WORK/constant 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 ****************************************************************************************例2 复杂的常量触发器需要使用SVF文件或用户设置// 参考设计 module constant1(input [4:0]a, b, input clk, output reg z); reg b_r; wire [9:0] constexp; assign constexp a * b - (a[4] ? (b 4) : 0) - (a[3] ? (b 3) : 0) - (a[2] ? (b 2) : 0) - (a[1] ? (b 1) : 0) - (a[0] ? (b 0) : 0); // 实际上是a*b -a*b always (posedge clk) begin z a[4]|b_r; b_r constexp[8]; end endmodule // 实现设计需要使用compiler_ultra命令 module constant1 ( a, b, clk, z ); input [4:0] a; input [4:0] b; input clk; output z; DFFQXL z_reg ( .D(a[4]), .CK(clk), .Q(z) ); endmodule假设使用SVF文件手动使用guide_reg_constant命令也可例2的SVF处理结果如下所示。***************************** Guidance Summary ***************************** Status Command Accepted Rejected Unsupported Unprocessed Total ---------------------------------------------------------------------------- environment : 5 0 0 0 5 mark : 2 0 0 0 2 multiplier : 1 0 0 0 1 reg_constant : 1 0 0 0 1 transformation map : 6 0 0 0 6 tree : 1 0 0 0 1 ungroup : 1 0 0 0 1 uniquify : 1 0 0 0 1 ****************************************************************************例2的匹配结果如下所示可以看出与例1不同的是此时参考设计中没有出现未匹配的触发器这是由于guide_reg_constant命令Formality像Design Compiler那样直接将常量触发器移除了。*********************************** 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 ****************************************************************************************例2的验证结果如下所示可以看出验证成功了。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/constant1 Implementation design: i:/WORK/constant1 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 ****************************************************************************************下面来看看如果在复杂的例2中不使用SVF文件、手动使用set_constant命令和guide_reg_constant命令会发生什么。匹配结果如下所示可以看出与例1不同的是此时Formality未能将这个复杂的常量触发器正确识别。*********************************** 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 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 ****************************************************************************************此时的验证失败总共有两个失败点首先是参考设计中存在未匹配的非常量触发器其次是比较点z_reg失败。********************************* Verification Results ********************************* Verification FAILED ---------------------------------------------------------- Reference design: r:/WORK/constant1 Implementation design: i:/WORK/constant1 1 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 0 0 1 Failing (not equivalent) 0 0 0 0 0 1 0 1 ****************************************************************************************其中比较点z_reg失败的模式如图2所示其中br_r_reg的取值为1与它的正确取值常量0相反。图2 失败的模式