相关阅读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)。本文将详细阐述时序变换中的不可读触发器的移除将简单介绍不可读触发器的概念有关不可读概念的详细介绍参考下面的这篇博客。Formality不可读(unread)的概念https://chenzhang.blog.csdn.net/article/details/145242304二、不可读触发器移除图1 不可读触发器的综合如图1所示当Design Compiler或HDL Compiler识别到不可读触发器后它会将其从设计中移除可通过compile_delete_unloaded_sequential_cells变量或set_unloaded_register_removal、set_compile_directives命令改变Formality将自动识别不可读触发器无需使用SVF文件和用户设置一般情况下参考设计中会存在未匹配的不可读触发器即使不可读触发器匹配成功了默认情况下也不会进行验证可通过verification_verify_unread_compare_points变量改变。关于Design Compiler中不可读触发器移除的更多细节可以参考下面的博客。Design Compiler不可读单元的移除https://chenzhang.blog.csdn.net/article/details/157099538?spm1001.2014.3001.5502关于HDL Compiler中不可读触发器移除的更多细节可以参考下面的博客。HDL Compilerhdlin_preserve_sequential变量和preserve_sequential综合指令的使用https://blog.csdn.net/weixin_45791458/article/details/158042894?sharetypeblogdetailsharerId158042894sharereferPCsharesourceweixin_45791458spm1011.2480.3001.8118三、示例例1 不可读触发器// 参考设计 module unread(input a, b, clk, output z); reg a_r1, a_r2; assign z a_r1; always(posedge clk) begin a_r1 a; a_r2 a b; // 没有负载 end endmodule // 实现设计 module unread( a, b, clk, z ); input a, b, clk; output z; DFFQXL a_r1_reg ( .D(a), .CK(clk), .Q(z) ); endmodule下面的图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 1(0) Unmatched reference(implementation) unread points ****************************************************************************************使用report_unmatched_points -status unread可以显示该点的详细信息可以看出不匹配的点就是被Design Compiler移除的不可读触发器如下所示。************************************************** Report : unmatched_points -status unread Reference : r:/WORK/unread Implementation : i:/WORK/unread Version : O-2018.06-SP1 Date : Thu Jan 23 22:32:31 2025 ************************************************** 1 Unmatched point (1 reference, 0 implementation): Ref DFF r:/WORK/unread/a_r2_reg例1的验证结果如下所示可以看到即使参考设计中出现了未匹配的触发器但由于其被识别为不可读触发器因此验证成功。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/unread Implementation design: i:/WORK/unread 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 ****************************************************************************************假设使用RTL描述同时作为参考设计和实现设计不可读触发器能够匹配成功如下所示。*********************************** 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 ****************************************************************************************验证结果如下所示可以看出不可读的比较点默认情况下会被归为Not Compared类而不进行验证。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/unread Implementation design: i:/WORK/unread 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 Not Compared Unread 0 0 0 0 0 1 0 1 ****************************************************************************************如果将verification_verify_unread_compare_points变量设置为true则会对成功匹配的不可读比较点进行验证如下所示。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/unread Implementation design: i:/WORK/unread 3 Passing compare points ---------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL ---------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 1 2 0 3 Failing (not equivalent) 0 0 0 0 0 0 0 0 **************************************************************************************** 
长河君 · 2026/9/17 9:41:01 · 阅读 1.2k 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)。本文将详细阐述时序变换中的不可读触发器的移除将简单介绍不可读触发器的概念有关不可读概念的详细介绍参考下面的这篇博客。Formality不可读(unread)的概念https://chenzhang.blog.csdn.net/article/details/145242304二、不可读触发器移除图1 不可读触发器的综合如图1所示当Design Compiler或HDL Compiler识别到不可读触发器后它会将其从设计中移除可通过compile_delete_unloaded_sequential_cells变量或set_unloaded_register_removal、set_compile_directives命令改变Formality将自动识别不可读触发器无需使用SVF文件和用户设置一般情况下参考设计中会存在未匹配的不可读触发器即使不可读触发器匹配成功了默认情况下也不会进行验证可通过verification_verify_unread_compare_points变量改变。关于Design Compiler中不可读触发器移除的更多细节可以参考下面的博客。Design Compiler不可读单元的移除https://chenzhang.blog.csdn.net/article/details/157099538?spm1001.2014.3001.5502关于HDL Compiler中不可读触发器移除的更多细节可以参考下面的博客。HDL Compilerhdlin_preserve_sequential变量和preserve_sequential综合指令的使用https://blog.csdn.net/weixin_45791458/article/details/158042894?sharetypeblogdetailsharerId158042894sharereferPCsharesourceweixin_45791458spm1011.2480.3001.8118三、示例例1 不可读触发器// 参考设计 module unread(input a, b, clk, output z); reg a_r1, a_r2; assign z a_r1; always(posedge clk) begin a_r1 a; a_r2 a b; // 没有负载 end endmodule // 实现设计 module unread( a, b, clk, z ); input a, b, clk; output z; DFFQXL a_r1_reg ( .D(a), .CK(clk), .Q(z) ); endmodule下面的图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 1(0) Unmatched reference(implementation) unread points ****************************************************************************************使用report_unmatched_points -status unread可以显示该点的详细信息可以看出不匹配的点就是被Design Compiler移除的不可读触发器如下所示。************************************************** Report : unmatched_points -status unread Reference : r:/WORK/unread Implementation : i:/WORK/unread Version : O-2018.06-SP1 Date : Thu Jan 23 22:32:31 2025 ************************************************** 1 Unmatched point (1 reference, 0 implementation): Ref DFF r:/WORK/unread/a_r2_reg例1的验证结果如下所示可以看到即使参考设计中出现了未匹配的触发器但由于其被识别为不可读触发器因此验证成功。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/unread Implementation design: i:/WORK/unread 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 ****************************************************************************************假设使用RTL描述同时作为参考设计和实现设计不可读触发器能够匹配成功如下所示。*********************************** 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 ****************************************************************************************验证结果如下所示可以看出不可读的比较点默认情况下会被归为Not Compared类而不进行验证。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/unread Implementation design: i:/WORK/unread 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 Not Compared Unread 0 0 0 0 0 1 0 1 ****************************************************************************************如果将verification_verify_unread_compare_points变量设置为true则会对成功匹配的不可读比较点进行验证如下所示。********************************* Verification Results ********************************* Verification SUCCEEDED ---------------------- Reference design: r:/WORK/unread Implementation design: i:/WORK/unread 3 Passing compare points ---------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL ---------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 1 2 0 3 Failing (not equivalent) 0 0 0 0 0 0 0 0 ****************************************************************************************