[Bài 1] Kiến thức từ cơ bản đến nâng cao về việc kiểm tra equivalence giữa 2 design

Tác giả: TrongTran
Ngày: 29/11/2019
Tài liệu tham khảo: https://www.synopsys.com/content/dam/synopsys/implementation&signoff/datasheets/formality-and-formality-ultra-ds.pdf

https://www.techdesignforums.com/practice/technique/equivalence-checking-eco-arm-core-subsystem-stmicroelectronics/

https://www.techdesignforums.com/practice/technique/using-sequential-equivalence-to-verify-clock-gating-strategies/

https://filebox.ece.vt.edu/~athanas/4514/ledadoc/html/pol_formality.html

Hình ảnh trong bài được lấy từ google image.


Sơ lược.

Trước đây mình có cơ hội để trải nghiệm với quá trình synthesis và debug formality rất nhiều và bài này, mình tham khảo một phần từ những kiến thức trên mạng và kiến thức bản thân. Mình không đi chi tiết mà chỉ tập trung giải thích những điểm trọng tâm. Chi tiết các bạn đọc spec của các tool nhé.


Nói tới việc kiểm tra equivalence chúng ta có 2 loại thông dụng đó là:

• Boolean logic equivalence
• Sequential equivalence

Trong bài này chúng ta sẽ tìm hiểu về loại thứ nhất đó là Boolean logic equivalence. Phương pháp này thường được sử dụng cho việc kiểm tra giữa RTL và gate hoặc giữa gate và gate. Một số tool hỗ trợ là: Formality (Synopsys), Smart LEC (Cadence)…

Các bạn tham khảo hình bên dưới:




Loại thứ hai là sequential equivalence: Thông thường nếu bạn dùng Boolean logic equivalence, nếu có 1 flip flop không thể map thì kết quả của bạn sẽ bị fail. Nghĩa là một số trường hợp không thể verify được bằng phương pháp 1 sẽ sử dụng phương pháp thứ 2, verify bằng sequential equivalence. Phương pháp này được sử dụng rộng rãi cho việc kiểm tra giữa RTL và RTL, tức là 2 model. Bạn có 1 RTL ban đầu, Sau đó bạn muốn optimize nó. Có thể là bạn sử dụng clock gating để tiết kiệm power (Tắt clock cho một số vùng không cần thiết một vài chu kì). Phương pháp 1 không thể kiểm tra cho clock gating hoặc nếu muốn bạn phải thêm constraint bằng thủ công. Lúc này sequential equivalence sẽ kiểm tra liệu output của các block sequential cùng input có tương đương nhau tại các cạnh lên của clock hay không. Chúng ta hay sử dụng tool VC formal cho việc kiểm tra này. Các bạn tham khảo hình bên dưới:





Tìm hiểu về Boolean logic equivalence

Đầu tiên, Để cho dễ hiểu mình nói đến mục đích của việc kiểm tra equivalence giữa hai design. Như hình bên dưới các bạn có thể thấy. Việc simulation cho RTL sẽ tốn rất nhiều thời gian. Sau khi quá trình verify hoàn tất bạn dùng RTL đó để synthesis ra gate net list.

Trong quá trình chuyển đổi từ RTL sang gate, Bạn có thể dùng 1 số tool phổ biến như: DC compiler, Fusion compiler, Physical compiler… Bạn không thể biết chính xác liệu quá trình từ RTL sang gate có bất kì sai sót nào không. Sai sót trong script hoặc sai sót của tool ..v.v.

Có hai cách để bạn biết điều đó:

Chạy simulation lại với gate net list: Việc này tốn rất nhiều thời gian, quá trình debug cũng khó khăn vì waveform của từng cell cũng sẽ được tạo ra (Mỗi cell được xem như là một submodule). Mình từng debug cho gate và phải nói để load 1 waveform mình tốn gần 1 giờ.

Kiểm tra xem function của gate và RTL có tương đương không: Cách này sẽ tốn ít time hơn, ít resource hơn. Các bạn lưu ý là phương pháp này không kiểm tra function đúng/sai nhé. Nó chỉ có tác dụng là kiểm tra tính giống nhau về mặt function của gate và RTL. Tính đúng sai của function đã được kiểm tra trong quá trình chạy simulation.

SVF file chính là file lưu lại toàn bộ các tiến trình mà các tool khác thực hiện (Ở đây là DC compiler). Các tiến trình đó là gì ? Đó là thay đổi tên của các instance, module, net…. Cũng có thể là optimize logic, delete logic. Quá trình load file này nhằm giúp các tool kiểm tra equivalence có thể biết được cách match các cặp điểm compare point dễ dàng hơn. Với tool DC compiler các file svf được mã hoá. Nhưng bạn không cần lo. Hầu hết các tool kiểm tra equivalence sau khi load xong đều giãi mã ra một file mà chúng ta dễ dàng đọc hiểu. File giải mả của svf chính là file vsdc (Smart LEC dùng file này cho đầu vào).

Để tạo được file svf hoặc vsdc chỉ cần bạn thêm câu lệnh sau vào script synthesis:

Set_svf ten_file.svf

Set_vsdc ten_file.vsdc

Việc kiểm tra giữa gate to gate được áp dụng tại 2 điểm:

Giữa gate trước optimize hoặc chèn các mạch test và gate kết quả.

Giữa gate ECO và gate ban đầu. Các bạn tham khảo hình bên dưới:






Hiện nay các tool trên thế giới có hai flow chạy phổ biến đó là:

• Flat verification: Nghĩa là các pattern sẽ được đưa vào các input của logic cone và kiểm tra hàng loạt các điểm compare point. Không phân biệt hierarchy.

• Hier verification: Tool sẽ verify cho các submodule nhỏ trước sau đó tiến hành black box chúng và verify cho những submodule lớn hơn. Phương pháp này có nhiều ưu điểm so với phương pháp flat verification bên trên. Giả sử trong 1 submodule ta có nhiều submodule nhỏ hơn cùng cấp. Vậy ta có thể chạy verify song song cho những submodule này. Điều này giúp giảm thời gian verification. Tuy nhiên bạn cần nhiều số core CPU hơn. Chúng ta sẽ có giới hạn số submodule được verify tối đa cho 1 lần chạy song song.

Đồng thời số CPU set cho việc chạy phải lớn hơn số submodule cần verify song song 1 lần để đạt hiệu quả tối đa.









Nhìn hình trên vậy thui chứ nó không đơn giản đâu nhé. Khó nhất là việc truyền tham số từ ngoài vào các submodule đó để verify.

Trong RTL thực tế ta có một module có thể được gọi nhiều lần. Tuy nhiên, Trong gate mỗi module chỉ được gọi 1 lần.


Một số thuật ngữ cần biết.

Để bắt đầu đi vào chi tiết bài này các ạn cần biết một số thuật ngữ bên dưới.

Logic cone:









Logic cone có thể hiểu là 1 mạch bao gồm các phần tử combinational logic hình nón như hình vẽ bên trên.

Các điểm khởi đầu của logic cone là:

• Chân input của module.
• Chân output của flip flop.
• Ngõ ra của black box.

Black box:

Black box là một model rỗng của một module. Hay nói đúng hơn là chúng ta không biết function bên trong khối black box đó và cũng không cần kiểm tra equivalence của nó. Việc kiểm tra đã được verify trong một tiến trình khác hoặc được đảm bảo bởi nhà cung cấp.

Chân input của black box là các điểm cần compare.

Chân output của black box là input của logic cone.

Chân không xác định hướng được xem là inout

Trong thực tế black box có thể là:

• Analog cell.
• RAM
• Module không cần verify. Trường hợp ta không muốn verify cho module nào đó ta có thể set black box cho nó.

Reference design: Là design ban đầu.

Implemetation design: Là design sau khi chỉnh sữa mà bạn cần kiểm tra xem liệu nó có equivalence với design ban đầu không. Lưu ý không nhầm lẫn giữa hai design này nhé.

Có 3 điểm cần verify:

• Giá trị tại input của black box.
• Giá trị ngõ vào của flip flop.
• Giá trị tại chân output của module.

Giả sử điểm check là A trong hình trên, thì các bộ pattern sẽ được đưa vào tại 3 điểm:

• Tại các chân input của module.
• Tại chân output của flip flop.
• Tại chân output của khối black box.

Các bạn có thể tham khảo hình bên trên.


Pattern là các bộ giá trị [1,0] đưa vào:

• Chân output của black box.
• Chân output của flip flop.
• Chân input của module.

Quá trình kiểm tra equivalence của 2 design được chia thành:

Kiểm tra consistency: Đối với mọi pattern đầu vào, tại điểm so sánh, nếu design reference có kết quả là 1 hoặc 0 thì design implementation phải có cùng kết quả. Nếu design reference có kết quả là x và design implementation có kết quả tại điểm so sánh là 0 hoặc 1 thì quá trình kiểm tra vẫn cho kết quả PASS.

Kiểm tra equality: Quá trình này bao gồm cả quá trình kiểm tra consistency nhưng thêm một vài constraint. Nghĩa là nếu kết quả của design reference là x và design implementation là 0 hoặc 1 thì kết quả là FAIL. Để pass thì kết quả của design implementation cũng phải là x.

Thông thường ta có quy tắc kiểm tra sau:

• RTL với GATE : Consistency

Cú pháp: set verification_passing_mode consistency

• GATE vs GATE : equality

Cú pháp: set verification_passing_mode equality

Nếu chúng ta không set mode verify cho module thì mặc định là kiểm tra consistency.

Lưu ý: Design A consistency với Design B. Tuy nhiên, Design B có thể không consistency với design A.

Design A:

module A (in_0, out_0);

input [1:0] in_0;

output out_0;

reg out_0;

always @(*) begin

case (in_0)

2’b00: out = 1’b0;

2’b01: out = 1’b1;

2’b00: out = 1’b0;

2’b01: out = 1’b1;

endcase

end

endmodule



Design B:

module A (in_0, out_0);

input [1:0] in_0;

output out_0;

reg out_0;

always @(*) begin

case (in_0)

2’b00: out = 1’b0;

2’b01: out = 1’b1;

2’b00: out = 1’b0;

2’b01: out = 1’bx;

endcase

end

endmodule



Nếu design A là reference và design B là implementation thì 2 design consistency với nhau.

Nếu design A là implementation và design B là reference thì 2 design không consistency với nhau.

Design A và design B không equality với nhau bất kể là implementation hay reference.



Để tìm được các cặp 2 flip flop so sánh. Các tool sẽ tiến hành match dựa vào 2 phương pháp chính:

• Match dựa vào name.

Đây là bước ưu tiên trong quá trình match vì nó tốn ít thời gian để tool analyze structure của design.

Tool sẽ tiến hành list ra tất cả:

• Flop flip
• Latch
• Black box

Match dựa vào name được chia làm 3 bước nhỏ:

• Exact name matching: Match dựa vào tên chính xác của các phần tử cần so sánh.

Ví dụ:

• Reference: /WORK/top/FF_0
• Implementation: /WORK/top/FF_0

Hai trường hợp trên tool sẽ match như là 1 cặp cần compare.

• Reference: /WORK/top/FF_0
• Implementation: /WORK/top/FF[0]

Nếu bạn có 2 flip flop tên như trên phương pháp “Exact name matching” không thể match chúng được.

• Match dựa vào net names: Cái này đơn giản chỉ là nếu 2 flip flop khác tên nhau nhưng có các net name cùng tên đi vào thì sẽ được match. Các bạn tham khảo hình bên dưới:

Hai flip flop

• reference: /WORK/top/submodule_0/FF_0

Và

• implementation: /WORK/top/submodule_0/FF_0_1

Có tên không giống nhau nhưng các net name đi vào giống nhau nên sẽ được match để như là 1 cặp để so sánh.

Tuy nhiên, thực tế, trong một design lớn không ai dùng phương pháp match này.

Tên các net name trở nên rất đa dạng trong một design phức tạp và việc trùng net name giữa 2 flip flop không cùng chức năng có thể xảy ra. Việc này dẫn đến việc match sai và kết quả verify không đáng tin.

Một điểm lưu ý nữa là các bạn nên sắp xếp thứ tự các phương pháp match ưu tiên vì flip flop đã match trước đó sẽ không được match trong các rule sau.

• Match với Name filtering

Cú pháp: name_match_filter_chars ‘~!@#$%^&*()_+= |\{}[]”:;<>?,./

Câu lệnh này phải đi kèm với câu lệnh bật tắt chế độ match filter:

Cú pháp: name_match_use_filter true/false

Với cách match này hai instance bên dưới được match với nhau

Reference: /WORK/top/submodule_0/FF_0

Implementation: /WORK/top/submodule_0/FF[0]



Nếu bạn đang synthesis với một số tool như DC compiler, Fusion compiler, Physical compier…

Phương pháp này nên được sử dụng thường xuyên.



Phương pháp thứ hai đó là match dựa vào topological equivalence. Phương pháp này tốn nhiều thời gian để tool phân tích structure của design.


Debug

Một số tool sẽ lưu lại session để giúp cho việc debug.

Để debug. Có 2 cách phổ biến:

Cách 1: Debug dựa vào log file. Bạn kiểm tra log file để xem các điểm fail nằm trong submodule nào. Bạn phải xác định được level của submodule đó.

Ví dụ: fail tại submodule top/sub_0/sub_1

Thì submodule sub_1 thuộc level 2

Sau đó trong script chạy bạn thêm dòng lệnh sau trước quá trình maching và verify:

write_hierarchical_verification_script -level 2 file_name –replace

Và dòng lệnh dưới sau quá trình matching và verify:

source file_name.tcl

Bạn chạy lại quá trình verify. Sau khi chạy xong bạn sẽ thấy được một file là: file_name.tcl

Bạn kiểm tra file file_name.tcl. File này là file giúp chạy verify cho từng submodule nhỏ để tìm lỗi bên trong.

Bạn tiến hành kiểm tra file kết quả: fm_file_name.log

Sau đó bạn mở file file_name.tcl lên tìm submodule bị fail và xem các tham số port đầu vào có truyền đúng không vì nguyên nhân fail có thể từ những submodule khác và truyền tham số qua sai.

Phương pháp này khá là phức tạp và tốn thời gian.



Cách 2: Dùng GUI.

Nếu trong script của bạn có lệnh save_session thì bạn có thể dùng output của lệnh này để debug. Nếu không bạn phải thêm lệnh bên dưới và cuối script chạy của bạn:

save_session –replace name_session

Output của file này là file name_session.

Để dùng GUI debug bạn phải vào chế độ command line của tool.

Để load file session bạn chạy lệnh:

restore_session name_session

và chạy lệnh start_gui để mở chế độ GUI mode lên.

Sau khi chế độ GUI được mở. Cửa sổ các điểm compare point hiện lên bạn dùng lệnh :

report_unmatched_points

hoặc

report_failing_points

Để in ra các điểm fail hoặc các điểm không match. Từ các điểm fail này bạn tìm trong list tương ứng và click chuột phải chọn “Show logic cone”

Trace theo các logic bạn sẽ dễ tìm ra điểm fail hơn.







Các bạn lưu ý: Mấu chốt của việc debug là bạn phải tìm ra các flip flop hoặc các output hoặc black box unmatched. Đây là các điểm dễ gây fail nhất. Vì sao? Mình lấy ví dụ:

Các bộ pattern sẽ được đưa vào :

• Output của khối black box.
• Output của flip flop (Chân Q).
• Input của module.

Giả sử ta có hai module như bên dưới: 

Giả sử ta chỉ sử dụng phương pháp match bằng tên chính xác. Như vậy chỉ có cặp flip flop

r:/WORK/FF1

i:/WORK/FF1

là match với nhau. Còn flip flop FF2 và FF3 không match vì không giống tên nhau.

Nguyên tắc đưa pattern vào đó là nếu 2 điểm match với nhau thì giá trị đưa vào là giống nhau. Trường hợp pattern đưa vào tại 1 và 3 là giống nhau cùng bằng 1 hoặc 0.

Còn giá trị tại 2 và 4 có thễ khác nhau điều này dẫn đến kết quả so sánh bị sai. Các bạn tham khảo hình bên trên.

Nếu có bất kì sai sót nào, mong nhận được phản hồi từ bạn đọc.

Trong bài 2 mình sẽ trình bày về 1 số điểm fail phổ biến.