相关阅读

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文件失效时进行调试。

        本文将详细阐述时序变换中的寄存器复制。

二、寄存器复制

        如图1所示，在某些情况下，Design Compiler可能为了性能而复制寄存器（可通过set_register_replication命令或compile_register_replication变量（对于拓扑模式）设置），随后在SVF文件中添加guide_reg_duplication命令；当Formality处理SVF文件时，将会确认guide_reg_duplication命令的有效性，如果有效（这里指的是命名相关的有效性，而不是功能相关）则将指定的寄存器进行复制。 

三、可能会出现的问题

        问题1：guide_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) begina_r1 <= a;end
endmodule// 实现设计（需要使用compiler_ultra命令）
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 name0 Compare points matched by signature analysis0 Compare points matched by topology2 Matched primary inputs, black-box outputs0(1) Unmatched reference(implementation) compare points0(0) Unmatched reference(implementation) primary inputs, black-box outputs
----------------------------------------------------------------------------------------
Unmatched Objects                                                        REF        IMPL
----------------------------------------------------------------------------------------Registers                                                                 0           1DFF                                                                     0           1
****************************************************************************************

        此时的验证失败， 被复制的寄存器驱动的输出端口z2验证失败，如下所示。

********************************* Verification Results *********************************
Verification FAILED
-------------------Reference design: r:/WORK/duplicationImplementation design: i:/WORK/duplication2 Passing compare points1 Failing compare points0 Aborted compare points0 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/duplicationImplementation design: i:/WORK/duplication4 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
****************************************************************************************