[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.

Phân tích timing violation thông qua một ví dụ cụ thể

Tác giả: TrongTran
Ngày: 15/11/2019
Tài liệu tham khảo: http://www.vlsi-expert.com/, wiki
và các nguồn tư liệu từ internet.

Nếu bạn đang làm về synthesis và các quá trình checker hậu synthesis. Hay nói đúng hơn là bạn đang làm việc với gate net list thì đây là bài tổng quan và rất chi tiết dành cho bạn.

Để phân tích timing có 4 loại path mà bạn cần quan tâm đó là:

• Từ input đến chân D flip flop (IN2REG).
• Từ chân CLK của 1 flip flip đến chân output (REG2OUT).
• Từ chân input đến chân output (IN2OUT).
• Từ chân CLK của flip flip thứ nhất đến chân D của flip flop thứ 2 (2 flip flop liền kề) (REG2REG).

4 loại path này đã được phân tích kĩ ở trang này nên mình sẽ không giải thích lại: 

http://nguyenquanicd.blogspot.com/2018/07/sta-tong-quan-ve-phan-tich-timing-tinh.html

Trong thực tế nếu bạn đang synthesis cho 1 module nhỏ thì bạn chỉ cần quan tâm đến path REG2REG. Những path khác sẽ được check bởi 1 nhóm khác (Nhóm dùng gate net list của bạn để connect đến module khác).

Trong hình trên, Giả sử bạn đang synthesis cho module A. Khi đó, nhiệm vụ ưu tiên của bạn là đảm bảo đường A3 (reg2reg, đường màu đỏ) không bị violate timing. Các đường A0, A1, A2 sự violation chỉ mang tính tương đối. Vì để kiểm tra timing violation cho các đường này bạn cần phải biết chúng connect đến các flip flop nào trong các module khác. Chỉ có team làm top module mới biết được điều này.

Nói như vậy không có nghĩa là bạn muốn để các path A0, A1, A2 violate bao nhiêu tuỳ thích. Bạn sẽ được cung cấp 1 giới hạn. Ví dụ thời gian delay tối đa là bao nhiêu. Điều này đảm bảo không gây khó khăn trong quá trình phân tích và chỉnh sửa timing ở chip top.

Trong kiểm tra timing chúng ta cần kiểm tra 2 loại violation chính đó là:

• Hold violation
• Setup violation

Trước tiên bạn cần hiểu hold violation và setup violation là gì?

Quan sát hình trên ta thấy: 

• Nếu tín hiệu data chưa ổn định trong khoảng thời gian tsu thì ta gọi đó là setup violation. Ngược lại nếu tín hiệu data chưa ổn định trong khoảng thời gian thd thì được gọi là hold violation.
• Nếu data thay đổi trong miền gạch chéo trước tsu thì data không bị delay 1 chu kì. Nếu data thay đổi trong miền gạch chéo sau thd thì data bị delay 1 cycle.

Chú ý tsu là setup time và thd là hold time của 1 flip flop. Với mỗi flip flop khác nhau chúng ta sẽ có tsu và thd khác nhau. Lí giải cho việc này các bạn có thể tham khảo hình bên dưới:

Cấu trúc D flip flop

                                   Cấu trúc jk flip flop. 
Với mỗi flip flop khác nhau, chúng ta sẽ có mạch combinational logic giữa chân clk và D, giữa chân D và Q khác nhau do đó hold time và setup time sẽ khác nhau. Cùng 1 loại D flip flop nhưng nếu được sản xuất bởi các linh kiện bên trong khác nhau sẽ có hold time và setup time khác nhau.


Tiếp theo mình sẽ hướng dẫn bạn cách tính timing violation chi tiết cho một mạch cụ thể.

Ta có một mạch như bên dưới:

Yêu cầu là bạn phải kiểm tra timing violation cho path REG2REG (Nghĩa là từ chân clock của FF1 sang chân D của FF2).

Trước tiên chúng ta xem xét hình bên dưới:

Hold violation

Để kiểm tra hold violation, chúng ta cần biết được timing delay của path:

• Minimum delay của path: A0 -> A1 -> A2 -> A3 -> A4 (1)
• Maximum delay của path: A0 -> A1 -> B1 -> A4 (2)

Nếu hiệu số (1) –(2) > 0 thì mạch không bị hold violation.

(1) = 1 + 9 + 1 + 6 + 1 = 18 ns

(2) = 3 + 9 + 3 + 2 = 17ns

Vì Hold slack = (1) – (2) = 18 – 17 = 1ns > 0. Mạch này không bị Hold violation.

Giả sử hold time = 4ns thay vì 2 ns như đề bài thì ta có

(3) = 3 + 9 + 3 + 4 = 19 ns

Lúc này Hold slack = 18 – 19 = -1 ns < 0

Lúc này mạch sẽ bị hold violation.

Setup violation

Để kiểm tra setup violation, chúng ta cần biết được timing delay của path:

Maximum delay của path: A0 -> A1 -> A2 -> A3 -> A4 (3)

Minimum delay của path: T (Chu kì clock) + A0 -> A1 -> B1 - tsu (setup time) (4)

Nếu hiệu số setup slack = (4) – (3) > 0, mạch của chúng ta không bị setup violation.

Xét mạch trên ta có: (3) = 2 + 11 + 2 + 9 + 2 = 26 ns

(4) = 15 + 2 + 5 + 2 - 4 = 20 ns

Ta thấy setup slack = 20 – 26 = -6 ns < 0 . Do đó mạch của chúng ta bị setup violation.

Trường hợp trên giả sử ta sử dụng clock chậm hơn, nghĩa là T = 22 ns khi đó

(4)= 22 + 2 + 5 + 2 – 4 = 27 ns

Setup slack = 27 – 26 = 1ns > 0 do đó setup violation sẽ không xảy ra.


Như vậy, Chúng ta có 1 số phương pháp để tránh setup violation và hold violation:

• Thay đổi độ dài dây dẫn giữa hai flip flop: Như chúng ta tính toán trong ví dụ trên, Sự delay của dây dẫn cũng có thể gây ra setup violation hoặc hold violation. Nếu mạch của chúng ta bị hold violation chúng ta có thể di chuyển flip flop (Place and route) để delay trên đường data path lớn và delay trên đường clock path nhỏ lại. Thường thời gian delay của wire là không lớn nên phương pháp này được sử dụng để giải quyết các violation nhỏ và số lượng path bị violation không nhiều. Đây là một phương pháp phổ biến được sử dụng nhiều.

• Thay đổi các phần tử trên đường bị violation. Các phần tử được sản xuất bởi các vật liệu khác nhau, cấu trúc khác nhau sẽ có cac thông số delay khác nhau.

• Chèn buffer hoặc cặp inverter: Phương pháp này nhằm đạt được thời gian delay mong muốn. Buffer và cặp inverter sẽ không làm thay đổi giá trị logic của tín hiệu. Khi chúng ta muốn tăng thời gian delay của một số path như mong muốn ta có thể chèn các buffer hoặc cặp inverter vào.

• Nếu timing violation rất lớn và chúng ta không thể giải quyết được bằng các phương pháp trên, thì bắt buộc ta phải thêm 1 flip flop vào giữa 2 flip flop trên. Việc này được thực hiện bởi designer và mang tính rủi ro cao. Lúc này ta phải tiến hành verification lại nhằm đảm bảo việc delay 1 cycle của tín hiệu data không gây fail function.

• Cho module chạy với clock chậm (Tăng chu kì). Phương pháp này ít được sử dụng vì nó đòi hỏi phải thay đổi design rất nhiều. Việc cho module này chạy với clock chậm sau đó dùng mạch async để sync tín hiệu với clock nhanh. Phương pháp này được sử dụng khi mạch chúng ta đang bị setup violation (Xem công thức tính setup violation bên trên).

Nếu bài viết có gì sai sót mong nhận được ý kiến từ bạn đọc. Vui lòng gọi về số: 0339339692 hoặc e-mail trongk10@gmail.com để góp ý.