Formality：不可读(unread)的概念
相关阅读
Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
https://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.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)
beginar1 <= a;ar2 <= a & b;
endendmodule对于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 name0 Compare points matched by signature analysis0 Compare points matched by topology2 Matched primary inputs, black-box outputs0(0) Unmatched reference(implementation) compare points0(0) Unmatched reference(implementation) primary inputs, black-box outputs1(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 ComparedUnread 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) beginq1 <= d_in; q2 <= q1; q3 <= q2; q4 <= q3; endendmodule使用例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 ComparedUnread 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) beginq1 <= d_in; q2 <= q1; q3 <= q2; q4 <= q3; endassign 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)报告中清晰地说明了不可读的原因是因为常量阻塞。