Conformal LEC：官方學習教程

相關閱讀

Conformal LEChttps://blog.csdn.net/weixin_45791458/category_12993839.html?spm=1001.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仿真庫，即只包含原語的模塊定義；第二種是Synopsys?Liberty格式的庫（.lib文件）。下面分別展示了這兩種格式的庫文件。

// lib.v
module EXN(A1, A2, X);
input  A1, A2;
output X;
wire  A12;xor  (A12, A1, A2);not  (X, A12);
endmodulemodule EXO(A1, A2, X);
input  A1, A2;
output X;xor  (X, A1, A2);
endmodulemodule MEXN(A1, A2, X);
input  A1, A2;
output X;
wire  A12;xor  (A12, A1, A2);not  (X, A12);
endmodulemodule MEXO(A1, A2, X);
input  A1, A2;
output X;xor  (X, A1, A2);
endmodulemodule OB2(OUT, X);
input  OUT;
output X;buf  (X, OUT);
endmodulemodule OB1(OUT, X);
input  OUT;
output X;buf  (X, OUT);
endmodulemodule BUF1(A, X);
input  A;
output X;buf  (X, A);
endmodulemodule 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生成。