相关阅读Conformal LEChttps://blog.csdn.net/weixin_45791458/category_12993839.html?spm1001.2014.3001.5482本文是对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仿真库.v文件这类库只描述了标准单元的功能信息因此只能用于仿真/形式验证而无法用于综合并可选择使用celldefine与endcelldefine编译指令进行标记第二种是Synopsys Liberty格式的库.lib文件这类库不仅描述了标准单元的功能信息还包含时序、功耗等信息可以用于综合。下面分别展示了这两种格式的库文件。// lib.v celldefine 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 endcelldefine// 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 : AB; } } 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部分时请注意以下信息表示的是额外的关键点(Extra)该端口并未在另一个设计中找到对应的关键点。Revised设计包含三个额外的扫描端口这是可以接受的因为Golden设计是一个非扫描设计而m3104gat和n3104gat的是异常的。主要有以下的产生原因1、后端布局布线后的网表中可能包含额外的POWER和GROUND端口例如VDD和VSS2、DFT插入的额外输入输出端口3、在某些少见情况下冗余触发器也可能被报告为额外的关键点。不映射的关键点使用表示。主要有以下的产生原因1、命名不一致2、触发器的复制或合并3、常量触发器的移除4、在时钟路径上插入时钟门控单元5、冗余触发器的移除。还存在一类未映射关键点被称为不可达关键点(Unreachable)​​​​使用表示不可达指的是其影响无法传播到设计中的任何主输出的关键点。换句话说这些关键点已经不再参与决定设计功能因此在任何其他关键点的比较结果中它们都不会产生影响。因此这类关键点可以在比较过程中被安全地忽略。主要有以下两类产生原因1、从该关键点出发的传播路径被某个逻辑门阻断该门会屏蔽或破坏其值的传播2、该关键点的所有扇出分支在结构上都没有连接到任何主输出。请按照以下步骤将这对因为名称不同导致未映射的关键点手动设置为映射。1、选择Golden设计中的n3104gat关键点此时其将高亮显示。2、右键点击并在弹出菜单中选择Set Target Mapping Point此时n3104gat关键点的文字颜色会从黑色变为红色。3、选择Revised设计中的m3104gat关键点此时其将高亮显示。4、右键点击并在弹出菜单中选择Add Mapping Point-Non-invertConformal 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引脚为01、退出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 -fDofile可以使用Cadence的综合工具RTL Compiler或Genus生成。