Conformal LEC：官方学习教程-EW帮帮网

本文是对Conformal Equivalence Checking User Guide中附录实验的翻译（有删改），实验文件可见安装目录Conformal/share/cfm/lec/demo/doc_testcase，该目录下还提供了其他案例。

本实验将通过一个小型的案例帮助用户熟悉图形界面(GUI)下Conformal LEC的使用流程，实验内容是验证非扫描门级网表(Golden)与插入扫描链后的门级网表(Revised)的等价性。

启动Conformal

在shell中切换到实验目录并且使用lec命令启动Conformal LEC，如下所示。

$ cd demo/doc_testcase
$ lec

此操作将打开Conformal LEC的图形界面窗口，如图1所示。

图1 LEC的图形界面窗口

读取库文件

由于本实验的Golden和Revised设计都是门级网表，需要读取库文件以确定各标准单元的功能，Conformal LEC支持两种格式的库文件：第一种是Verilog仿真库，即只包含原语的模块定义；第二种是Synopsys Liberty格式的库（.lib文件）。下面分别展示了这两种格式的库文件。

// lib.v
module EXN(A1, A2, X);
input  A1, A2;
output X;
wire  A12;
  xor  (A12, A1, A2);
  not  (X, A12);
endmodule

module EXO(A1, A2, X);
input  A1, A2;
output X;
  xor  (X, A1, A2);
endmodule

module MEXN(A1, A2, X);
input  A1, A2;
output X;
wire  A12;
  xor  (A12, A1, A2);
  not  (X, A12);
endmodule

module MEXO(A1, A2, X);
input  A1, A2;
output X;
  xor  (X, A1, A2);
endmodule

module OB2(OUT, X);
input  OUT;
output X;
  buf  (X, OUT);
endmodule

module OB1(OUT, X);
input  OUT;
output X;
  buf  (X, OUT);
endmodule

module BUF1(A, X);
input  A;
output X;
  buf  (X, A);
endmodule

module IBT(X, IN);
input  X;
output IN;
  buf  (IN, X);
endmodule

// demo.lib
library(lib_demo) {

cell(AN2) {
  area : 2;
  pin(A) {
    direction : input;
    capacitance : 1;
  }
  pin(B) {
    direction : input;
    capacitance : 1;
  }
  pin(Z) {
    direction : output;
    function : "A B";
  }
}
cell(OR2) {
  area : 2;
  pin(A) {
    direction : input;
    capacitance : 1;
  }
  pin(B) {
    direction : input;
    capacitance : 1;
  }
  pin(Z) {
    direction : output;
    function : "A+B";
  }
}
cell(IV) {
  area : 1;
  pin(A) {
    direction : input;
    capacitance : 1;
  }
  pin(Z) {
    direction : output;
    function : "A'";
  }
}
}

本实验使用Verilog仿真库，请按照下面描述的步骤操作进行库文件的读取。

1、在菜单中选择File-Read Library或者点击图标即可打开库读取窗口。

2、保持Format的默认值Verilog，以及Type默认值Both，这代表库文件将同时用于Golden和Revised设计。

3、选择Verilog仿真库文件lib.v。

4、点击Add Selected将库文件添加到File List中(或者双击文件）。

5、点击OK，读取库文件，库读取窗口将关闭，主窗口中会显示已成功读取库的提示信息。

Warning: (VLG5.5) Internal primitive is recognized (occurrence:6)

这是由于Verilog仿真库中除了使用了Verilog标准门级原语外，还使用了MUX、DFF等Conformal LEC内部原语，可以忽略这个警告。

读取设计文件

非扫描门级网表是Golden设计，插入扫描链后的门级网表是Revised设计，请按照下面描述的步骤操作进行设计文件的读取。

1、在菜单中选择File-Read Design或者点击图标即可打开设计读取窗口。

2、保持Format的默认值Verilog，以及Type默认值Golden，这代表设计文件将作为Golden设计。

3、选择设计文件golden.v。

4、点击Add Selected将设计文件添加到File List中(或者双击文件）。

5、点击OK，读取库文件，设计读取窗口将关闭，主窗口中会显示已成功读取设计的提示信息。

6、以相同的方法读取revised.v作为Revised设计，注意需要将Type设置为Revised。

切换系统模式

对于这个小型案例，假设没有需要指定的约束，直接点击右上角的图标切换系统模式为LEC，此时Conformal LEC将对设计进行建模(Model)和关键点(Key Point)映射。映射完成后，主窗口中会显示警告信息和已映射和未映射的关键点汇总表，在之后的步骤中，会检查这些结果。

查看未映射和已映射的关键点

要查看关键点的详细信息，请选择Tools-Mapping Manager或者点击图标，此时Mapping Manager窗口将打开，如图2所示。

图2 Mapping Manager窗口

当查看Mapping Manager中的Unmapped Points部分时，请注意以下信息：

表示的是额外的输入/输出端口，该端口并未在另一个设计中找到对应的映射点。
Revised设计包含三个额外的扫描端口，这是可以接受的，因为Golden设计是一个非扫描设计。
Golden和Revised设计都多了一个额外的输出端口，因为它们的名称不同，Golden设计中的端口名称是n3104gat，而Revised设计中的端口名称是m3104gat。

请按照以下步骤将这对因为名称不同导致未映射的关键点手动设置为映射。

1、选择Golden设计中的n3104gat关键点，此时其将高亮显示。

2、右键点击，并在弹出菜单中选择Set Target Mapping Point，此时n3104gat关键点的文字颜色会从黑色变为红色。

3、选择Revised设计中的m3104gat关键点，此时其将高亮显示。

4、右键点击，并在弹出菜单中选择Add Mapping Point-Non-invert，Conformal LEC会将这两个关键点从Unmapped Points部分移除，并将它们显示在Mapped Points部分列表的底部，如图3所示。

图3 Mapped Points列表

在之后的步骤中，将对所有已映射的关键点进行比较，以确定它们是等价还是不等价。

进行比较验证

1、在Mapping Manager仍然打开的情况下的Mapped Points部分，点击图标将所有已映射的关键点添加为比较点。比较点现在显示在Compared Points部分，如图4所示，每对比较点前的图标表示比较点尚未进行验证。

图4 Compared Points列表

2、点击图标开始比较，主窗口中的状态栏会显示比较的进度（以百分比形式）。验证完成后，每对等价的比较点会用绿色圆圈标记，不等价的比较点会用红色圆圈标记。

3、向下滚动Compared Points列表以查找不等价的比较点，或在Compared Points部分点击图标，并在弹出菜单中取消勾选Equivalent复选框，仅查看不等价的比较点，如图5所示。

图5 查看不等价的比较点

诊断不等价的比较点

在此步骤中，将诊断一对不等价的比较点，以了解它们为何不等价。当比较完成后，用户可以查看不等价点的诊断信息，例如逻辑锥(logic cone)及其支持点(support)。

1、在Mapping Manager中，选择任意一对不等价的比较点（比如Golden设计中的U100/DF和Revised设计中的U100/DFSCAN这对比较点）。

2、右键点击，并在弹出菜单中选择Diagnose，打开Diagnosis Manager，如图6所示。

图6 Diagnosis Manager窗口

Diagnosis Manager显示之前步骤中选择的不等价的比较点相关的信息。该信息分为两列Golden和Revised。在Diagnosis Manager中，找到以下部分：

Compared Point

显示之前步骤中选择的不等价的比较点。

Diagnosis Point (active)

显示诊断点（一般为比较点的输入）及其仿真值。请注意，Golden设计和Revised设计的仿真值（在括号中显示）并不相同，Golden设计的值为0，而Revised设计的仿真值为1。

Corresponding Support

此部分显示诊断点的逻辑锥中对应的支持点（即作为逻辑锥输入的关键点）及其仿真值（在括号中显示）。

Non-corresponding Support

此部分列出了只出现在某一个设计诊断点的逻辑锥中的支持点。例如，scan_en输入端口是Revised设计诊断点的逻辑锥中的未映射关键点，不存在Golden设计诊断点的逻辑锥中对应的关键点。Revised设计诊断点的逻辑锥中的U99/DFFSCAN是一个已映射的关键点，但其对应的Golden设计中的U99/DF却不是该逻辑锥的支持点。

对于Corresponding Support和Non-corresponding Support，支持点可以有多种颜色：绿色表示支持点也进行了比较并证明为与其对应关键点是等价的，例如Golden设计中的U149/DF与Revised设计中的U149/DF进行了比较并且是等价的；红表示支持点也进行了比较并证明为与其对应关键点是不等价的，例如Golden设计中的U147/DF与Revised设计中的U149/DFSCAN进行了比较并且是不等价的；黑色表示支持点尚未进行比较或者不能比较（比如其是未映射的，或者其是输入端口），例如Revised设计中scan_en即是未映射的，也是输入端口。

Error Pattern

此部分列出了导致不等价的Pattern，它们证明了Golden和Revised诊断点仿真值之间的差异。每个错误Pattern的仿真值与支持点（不管是对应或不对应）相关联，当选择一个支持点时，Pattern中的关联列用粉色高亮显示，例如当选择n3100gat时，Pattern窗口的第一列变成粉色，如图7所示。

图7 选择支持点

可以看出有两列用红色或绿色标出来了，这红色列表示在列出的所有Pattern中都为1，红色列表示在列出的所有Pattern中都为0，这很可能是错误的来源。

请按照以下步骤查看诊断点的仿真值差异：

1、点击列表中的任意错误模式。

2、再点击另一个错误模式，比较对应支持点仿真值的变化（在括号中显示）。

Error Candidate

此部分列出了导致错误的原语门候选项及其加权百分比，例如反相器和选择器，这表示最有可能导致诊断点仿真值差异的原因。

查看原理图

要查看电路图表示，请在Diagnosis Manager中，点击顶部工具栏中的图标，原理图查看器会分别为Golden设计和Revised设计的逻辑锥打开两个单独的窗口，如图8和图9所示。

图8 Golden设计的原理图

图9 Revised设计的原理图

在图8和图9中，比较点用蓝色表示，诊断点用青色表示，错误候选项用红色表示，支持点用紫色表示。逻辑锥中各处的仿真值用数字1或0列在图中表示，每当切换pattern时，这些仿真值也会相应切换。

在Revised设计的原理图中可以看出，由于scan_en输入端口位1，导致进入了扫描模式，触发器的输入直接连接到另一个触发器的输出了，必须将scan_en信号约束为逻辑0，以便MUX门的功能路径生效。

添加引脚约束

为了添加约束，执行以下步骤，将系统模式切换为Setup模式，并添加约束来使Revised设计中的scan_en引脚为0：

1、退出Diagnosis Manager窗口并直接点击右上角的图标切换系统模式为SETUP。

2、在菜单中选择Setup-Pin Constraints打开Pin Constraints窗口。

3、点击Revised设计。

4、选择scan_en输入端口，右键点击，在弹出菜单中选择Add Constraint 0，如图10所示。

图10 设置端口约束

重新进行比较验证

重新按照之前的步骤进行比较验证，此时的结果如图11所示，可以看出不存在不等价的比较点了。

图11 重新查看不等价的比较点

退出

现在已经确认Golden设计和Revised设计是等价的，可以按照以下步骤退出Conformal结束本次实验了。

1、选择File-Exit。

2、在弹出的确认对话框中点击Yes。

Do脚本

下面的Dofile可以完成本实验的相同操作，相比于使用GUI进行验证，使用脚本更加高效。

read library lib.v -both
read design golden.v -verilog -golden
read design revised.v -verilog -revised
set system mode lec
add mapped points n3104gat m3104gat
add compare points -all
compare
diagnose /U100/DF -golden
set system mode setup
add pin constraint 0 scan_en -revised
set system mode lec
add mapped points n3104gat m3104gat
add compare point -all
compare
exit -f

Dofile可以使用Cadence的综合工具RTL Compiler或Genus生成。

Conformal LEC：官方学习教程