相关阅读
Formality
https://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
一般情况下，verify命令会对参考设计和实现设计所有匹配的比较点各自进行验证，但有些时候为了调试，可能需要验证参考设计和实现设计的逻辑锥中两个线网的等价性，这时就有两种选择：第一种方法是在使用set_cutpoint命令设置一对线网为cut-point，实际上这创建了一对新的比较点，并改变了原本逻辑锥的顶点和底点，有时候还需要用户使用set_user_match命令显式匹配这对比较点；第二种方法是使用GUI界面或set_probe_points命令在一对线网上设置探针，这不会影响逻辑锥结构，因为它是一个类似监视器的被动探针，本文就将详细阐述探针的设置与使用。
本文将以一个简单的例子进行说明，其中为了简便使用了RTL作为实现设计（一般情况下，实现设计是综合后的网表）。
// 参考设计
module probe(a, b, c, clk, z1, z2);input a, b, c, clk;output reg z1, z2;always @ (posedge clk)beginz1 <= a & b;z2 <= a | c;end
endmodule// 实现设计
module probe1(a, b, c, clk, z1, z2);input a, b, c, clk;output reg z1, z2;always @ (posedge clk)beginz1 <= a & b & c;z2 <= a | c;end
endmodule下面的图1是参考设计的原理图，图2是实现设计的原理图。
图1 参考设计的原理图
图2 实现设计的原理图
实现设计和参考设计的区别显而易见：参考设计中的z1寄存器由输入端口a、b驱动，而实现设计中的z2寄存器由输入端口a、b、c驱动。
验证结果失败，如下所示，这符合预期。
********************************* Verification Results *********************************
Verification FAILED
-------------------Reference design: r:/WORK/probeImplementation design: i:/WORK/probe13 Passing compare points1 Failing compare points0 Aborted compare points0 Unverified compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 2 1 0 3
Failing (not equivalent) 0 0 0 0 0 1 0 1
****************************************************************************************探针一般用于隔离错误，假设在如图3所示的位置设置了探针，如果探针验证通过，则问题更可能出现在逻辑锥中的Logic2部分，如果探针验证失败，则问题更可能出现在逻辑锥中的Logic1部分。
图3 一种可能的调试情况
在逻辑锥视图中，可以很方便的设置探针，只需要同时选中参考设计和实现设计中的一对线网，同时在Edit ToolBar中点击Set Probe按钮
即可（如果找不到Edit ToolBar，可以在ToolBar右键查看是否隐藏了Edit ToolBar，如图4所示），当然直接使用set_probe_points命令也是可以的。
图4 在GUI界面设置探针
假设在GUI界面设置了图5所示的探针。
图5 在GUI界面设置探针
在基于流程的工具栏上，点击6. Debug，在Probe Points列表中可以看到已设置的探针，如图6所示。
图6 查看已设置的探针
点击Verify按钮，或者右键并点击Verify Probes即可验证所有探针，当然直接使用verify -probe命令也是可以的，此时验证结果成功，如下所示。
***************************** Probe Verification Results *******************************
Probe Verification SUCCEEDED
----------------------------Reference design: r:/WORK/probeImplementation design: i:/WORK/probe11 Passing probe points
****************************************************************************************探针验证后，甚至可以像比较点那样，打开探针的逻辑锥视图和模式窗口，如图7所示。
图7 探针的逻辑锥视图和模式窗口
由此分析可得，问题应该出在探针右侧，唯一有可能出错的就是实现设计中多出的C1与门，调试结束。
