Formality：不可读(unread)的概念

相关阅读

Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482https://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)

        报告中清晰地说明了不可读的原因是因为常量阻塞。