相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482在Formality中有时会遇到不可读(unread)这个概念本文就将对此进行描述。不可读是一种状态触发器、锁存器、输入端口等许多对象都可能位于这种状态简单来说不可读就是直接或间接没有驱动输出端口。例1是一个RTL描述的不可读触发器的例子。// 例1 module fred (a, b, clk, z); input a, b, clk; output z; reg ar1, ar2; assign z ar1; // Note ar2 does not drive anything always (posedge clk) begin ar1 a; ar2 a b; end endmodule对于Design Compiler来说如果RTL描述中出现了没有负载的触发器则门级描述中会自动将其移除因此例1对应的门级网表如例2所示。// 例2 module fred ( a, b, clk, z ); input a, b, clk; output z; DFFQXL ar1_reg ( .D(a), .CK(clk), .Q(z) ); endmodule如果分别例1/例2作为参考/实现设计进行等价性检查匹配时会提示一个出现一个不匹配的点因为参考设计中没有移除不可读触发器而实现设计中移除了如下所示。*********************************** 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命令即可报告未匹配的不可读点如下所示。************************************************** Report : unmatched_points -status unread Reference : r:/WORK/fred Implementation : i:/WORK/fred Version : O-2018.06-SP1 Date : Wed Jan 22 15:31:44 2025 ************************************************** 1 Unmatched point (1 reference, 0 implementation): Ref DFF r:/WORK/fred/ar2_reg其实还有一对点也是不可读的只是此时匹配成功了它们就是输入端口b。可以使用report_unread_endpoints -all命令报告所有的不可读来源以及不可读的原因如下所示。************************************************** Report : unread_endpoints -all Reference : r:/WORK/fred Implementation : i:/WORK/fred Version : O-2018.06-SP1 Date : Wed Jan 22 15:37:10 2025 ************************************************** Following 2 blocking objects identified in the fanout: (Net ) r:/WORK/fred/ar2 (no reader) (Net ) i:/WORK/fred/b (no reader)不可读点在原理图中会用特殊标识说明图1是参考设计的原理图需要注意由于输入端口b的扇出只有不可读触发器ar2_reg它也被间接认定为不可读状态图2是实现设计的原理图。图1 参考设计图2 实现设计即使不可读的比较点匹配成功它们在默认情况下也会被归为Not Compared类而不进行验证如Formality比较点的验证状态和整体验证状态-CSDN博客一文所说可通过verification_verify_unread_compare_points变量改变。下面展示了使用RTL描述同时作为参考设计和实现设计从而让一对不可读比较点匹配后的验证结果。---------------------------------------------------------------------------------------- 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使用report_not_compared_points命令可以报告所有处于Not Compared类的比较点包括不可读。不可读状态是可能传递的如例3所示RTL描述的触发器链其中最后一个触发器q4_reg没有负载但由于q3_reg的扇出只有不可读触发器q4_reg所以它也为不可读触发器以此类推。// 例3 module dff_chain ( input clk, input d_in, output d_out ); reg q1, q2, q3, q4; always (posedge clk) begin q1 d_in; q2 q1; q3 q2; q4 q3; end endmodule使用例3同时作为参考设计和实现设计时的验证结果如下所示其中四个触发器都因为不可读而没有进行验证。---------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL ---------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 0 0 0 0 Failing (not equivalent) 0 0 0 0 1 0 0 1 Not Compared Unread 0 0 0 0 0 4 0 4使用set_constant命令设置常数值也可能导致不可读以例4来说如果将q4的输出线网d_out设置为常数0则会导致触发器q4_reg不可读从而导致四个触发器都不可读。// 例4 module dff_chain ( input clk, input d_in, output d_out ); reg q1, q2, q3, q4; always (posedge clk) begin q1 d_in; q2 q1; q3 q2; q4 q3; end assign d_out q4; endmodule使用例4同时作为参考设计和实现设计并使用set_constant -type net r:/WORK/dff_chain/d_out 0和set_constant -type net i:/WORK/dff_chain/d_out 0命令设置常数0此时report_unread_endpoints -all命令的结果如下所示。************************************************** Report : unread_endpoints -all Reference : r:/WORK/dff_chain Implementation : i:/WORK/dff_chain Version : O-2018.06-SP1 Date : Wed Jan 22 16:12:04 2025 ************************************************** Following 2 blocking objects identified in the fanout: (Net ) r:/WORK/dff_chain/d_out (blocked by constant) (Net ) i:/WORK/dff_chain/d_out (blocked by constant)报告中清晰地说明了不可读的原因是因为常量阻塞。