Formality:时序变换(五)(寄存器复制)
相关阅读
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 寄存器复制
如图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) begin
a_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 name
0 Compare points matched by signature analysis
0 Compare points matched by topology
2 Matched primary inputs, black-box outputs
0(1) Unmatched reference(implementation) compare points
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Registers 0 1
DFF 0 1
****************************************************************************************
此时的验证失败, 被复制的寄存器驱动的输出端口z2验证失败,如下所示。
********************************* Verification Results *********************************
Verification FAILED
-------------------
Reference design: r:/WORK/duplication
Implementation design: i:/WORK/duplication
2 Passing compare points
1 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
****************************************************************************************
其中比较点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/duplication
Implementation design: i:/WORK/duplication
4 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
****************************************************************************************