企业官网建设流程全解析

相关阅读

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文件失效时进行调试（不是所有时序变换都会记录在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?spm=1001.2014.3001.5502

三、可能会出现的问题

问题1：guide_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 失败的模式