Cách tính BW và latency trong 1 hệ thống SoC sử dụng chuẩn giao tiếp AXI protocol

Tác giả: TrongTran
Ngày: 31/12/2019

Nếu bạn nào đang làm về verification cho system performance (ST) thì bài này sẽ bổ ích cho bạn.

Ngày nay performance quyết định một phần rất quan trọng trong một hệ thống SoC nhắm giúp sản phẩm có thể cạnh tranh trên thị trường.

Việc verification hiện tại không chỉ đơn thuần là kiểm tra function của hệ thống mà còn kiểm tra performance của hệ thống. Nghĩa là một hệ thống chạy đúng là chưa đủ mà phải còn chạy nhanh. Mình lấy ví dụ:

Khi bạn sử dụng 3G và 4G thì đâu là sự khác biệt. Bạn không chỉ quan tâm tới sự ổn định của mạng, ít bị lỗi, bảo mật mà còn quan tâm đến tốc độ mạng.

Vì vậy performance đóng một vai trò cực kì quan trọng trong hệ thống SoC.

Hai yếu tố quan trọng nhất để đánh giá performance của hệ thống đó là Bw (Bandwidth) và latency (Độ trễ).

1. Cách tính BW.

Nhiều tài liệu định nghĩa là BW (bandwidth) là số lượng transaction được transfer trong 1 hệ thống trên một đơn vị thời gian.

Tuy nhiên, Theo mình cái này cần làm rõ lại, Giả sử mình có 1 hệ thống SoC gửi và nhận data với chuẩn AXI protocol.

Mình tiến hành đo đạc và thử nghiệm và dưới đây là kết quả:

	(ARLEN)Length = 16	(ARLEN)Length = 1
Số lượng transaction kênh AR	690	1113
Số lượng transaction kênh R	16*690 =11040	1*1113 = 1113
BW	3532.8 Mb/s	356.16 Mb/s
Thời gian chạy	50 us	50 us

Như vậy BW không phụ thuộc vào số lượng transaction kênh AR/AW mà phụ thuộc vào kênh W/R.

	(ARLEN)Length = 16	(ARLEN)Length = 16
ARSIZE	32 bytes	16 bytes
Số lượng transaction kênh AR	690	690
Số lượng transaction kênh R	16*690 =11040	16*690 = 11040
BW	3532.8 Mb/s	1766.4 Mb/s
Thời gian chạy	50 us	50 us

BW còn phụ thuộc vào tín hiệu ARSIZE/AWSIZE nghĩa là số lượng byte được transfer trong 1 transaction.

Tóm lại để tính toán được BW chúng ta cần biết các thông tin sau:

B: số byte transfer trong 1 transaction được tính từ ARSIZE/AWSIZE.

T: Run time

N: Số lượng transaction kênh W/R được transfer trong khoảng thời gian “run time”.



Như vậy công thức tính BW sẽ là:

BW = B*N/T 

Đơn vị đo lường BW thường là MB/s hoặc GB/s

Ví dụ:

Mình có master A có các thông số sau:

• ARSIZE = 4 word (1 word = 32 bit)
• Số lượng transaction kênh AR = 690 transaction
• ARLEN = 16
• Run time = 50 ns

Như vậy ta tính được số transaction kênh R là = 690*16 = 11040 transaction.

Số bit được transfer trong 1 transaction là 4*32 = 128 bit.

Tống số data transfer là 128*11040 = 1413120 bit = 176640 byte = 176.64 KB = 0.17664 MB.

Run time = 50 ns = 0.00005 s.

Vậy BW = 0.17664/0.00005 = 3532.8 MB/s.


Lưu ý:

• Trong tính toàn BW thì 1MB = 1000KB = 1000000 B.
• 1 Byte = 8 bit.
• Gửi transaction với single burst (1 beat) thì BW thấp.
• Gửi transaction với multi burst (> 1 beat) thì BW cao hơn.
• Nguyên nhân là do cùng 1 lượng data nhưng với single burst thì cần gửi nhiều tín hiệu control hơn.
• Cùng số lượng transaction, Data width càng lớn thì BW càng lớn.
• Cùng số lượng transaction, Data width càng nhỏ thì BW càng nhỏ.

Để đánh giá BW cảu hệ thống chúng ta cần quan tâm đến 3 yếu tố:

• BW của master : Được tính tại A (Cho master A) hoặc B (Cho master B) hoặc tại C (Cho master C).
• BW của bus system: bằng tống BW của A + B + C. Lưu ý là BW tối đa của bus system phải lớn hơn tổng các BW của các master gửi tới nó thì hệ thống mới đạ yêu cầu.
• BW của slave (hoặc DDR): Được tính toán tại D.

2. Cách tính latency.

Chúng ta cần phân biệt các khái niệm sau:

• Write latency
• Write data latency
• Read latency

Write data latency

Khoảng thời gian được tính từ sau khi AWVALID & AWREADY = 1 (handshake kênh write address ) cho đến khi WVALID & WREADY & WLAST = 1.


Write latency

Khoảng thời gian được tính từ sau khi AWVALID & AWREADY = 1 (handshake kênh write address ) cho đến khi BVALID & BREADY & BLAST = 1.

Ta luôn có Write latency > Write data latency.



Read latency

Khoảng thời gian được tính từ sau khi ARVALID & ARREADY = 1 (Handshake kênh Read address) cho đến khi RVALID & RREADY & RLAST = 1.



Early response for B channel

BVALID sẽ assert và gửi về slave ngay WVALID & WREADY = 1

Nếu checker đặt tại A thì write latency sẽ nhỏ hơn thực tế


Lưu ý:

• Gửi transaction với random address thì latency sẽ lớn hơn
• Gửi transaction với sequential address thì latency sẽ nhỏ

• Chú ý tới các fifo trong design nó sẽ ảnh hưởng đến latency trong hệ thống.

Bây giờ xét trường hợp ngược lại. giả sử ta có được số latency trung bình của một transaction. Ta có thể tính được run time cần để transafer một số lượng transaction cụ thể không ?

Xét bài toán bên dưới:

• Latency time của 1 transaction L = 500ns
• ARLEN = 1
• Số transaction cần transfer N = 20 transaction.
• Số OS (Outstanding của bus system) OS = 4.

Như vậy thời gian để hệ thống transfer 20 transaction trên là:

T = 5 x 500ns + 7 x ACLK.

ACLK : là chu kì clock.

Nếu chu kì clock là nhỏ so với latency ta có công thức gần đúng là

T = 5*500ns.

Giải đáp vài thắc mắc về AXI protocol

Biên dịch và soạn thảo: TrongTran
Ngày: 23/12/2019

Tài liệu tham khảo: https://community.arm.com/

Mình không giải thích lại về chuẩn giao tiếp AXI. Bạn nào chưa biết thì có thể tham khảo các bài viết của anh Quân Nguyễn tại trang này nhé:

http://nguyenquanicd.blogspot.com/2018/08/busbai-1-giao-thuc-amba-axi.html



Trong bài này mình sẽ giải thích một số điểm corner case trong chuẩn AMBA AXI protocol . Đây cũng là những câu hỏi của hầu hết các diễn đàng ARM trên thế giới mà mình thu thập lại trong quá trình đào sâu về AXI protocol.


Câu 1: WVALID và WREADY có thể được assert trước AWVALID và AWREADY tại phía slave không, Như vậy có violate AXI protocol ? 

Câu trả lời là có. Như chúng ta đã biết để tăng performance cho hệ thống, ARM đã phân chia kênh AW, W và B độc lập nhau như vậy trên đường truyền từ master tới slave qua interconnect (BUS system) thì kênh AW có thể qua nhiều register hơn kênh W. Do đó, kênh AW sẽ bị delay và có thể đến slave sau kênh W.

Mình lấy ví dụ:

Master assert kênh AW trước kênh W một chu kì xung clock. Nhưng kênh AW đi qua 4 flip flop còn kênh W đi qua 2 flip flop lúc này kênh W sẽ đến slave trước kênh AW.



Điều này không violate AXI protocol. Tuy nhiên, xét về mặt hệ thống, việc có chấp nhận điều này (WVALID assert trước AWVALID) hay không là phụ thuộc vào slave. Nếu slave không chấp nhận thì người design interconnect phải sữa lại design để đảm bảo delay giữa hai channel thoã mãn điều kiện. Đặc biệt, Nếu tồn tại bộ decoder trong interconnect (Trường hợp 1 master access nhiều hơn 2 slave). thì đòi hỏi kênh AW phải đến input của bộ decoder trước vì bộ decoder cần biết tín hiệu address để write đến đúng slave mong muốn.


Câu 2: Trong 1 chu trình write transaction, Khi nào thì BVALID được assert ? 

Nếu WLAST&WVALID&WREADY = 1, thì slave có thể assert BVALID bất chắp AWVALID và AWREADY đã assert hay chưa (Điều này không violate AXI protocol rule).



Câu 3: Một master gửi các thông tin burst size và burst length thông qua các tín hiệu ARSIZE, AWSIZE, ARLEN và AWLEN. Từ các thông tin đó chúng ta có thể tính được số beat trong 1 burst và biết được beat cuối. Tuy nhiên tại sao master và slave lại có thêm tín hiệu WLATS và RLAST để xác định beat cuối trong 1 burst được transfer ? 

Câu trả lời là giúp cho design trở nên đơn giản hơn.

Việc tính toán là hoàn toàn có thể tuy nhiên sẽ làm cho quá trình design cả master và slave trở nên phức tạp hơn và dễ gây bug.



Câu 4: Sự khác biệt giữa AXI4 và AXI3 ?

AXI4 không còn tín hiệu WID. Điều này có nghĩa là kênh W channel sẽ không hỗ trợ out-of-order và write data interleaving. Dữ liệu gửi ra từ kênh W sẽ có cùng thứ tự với dữ liệu gửi ra từ kênh AW (in-order).

Ví dụ:

AWADDR: ADDR_0 -> ADDR1 -> ADDR2

WDATA: DATA_0 -> DATA_1 -> DATA_2

Ngoài ra, Với AXI4, Tín hiệu ARLEN/AWLEN được mở rộng từ 4 bit width thành 8 bit width. Nghĩa là nó có thể hỗ trợ tối đa 256 beat transfer trong 1 burst. Điều này là cần thiết vì công nghệ ngày càng phát triển đòi hỏi tốc độ gửi nhận dữ liệu nhanh hơn. Việc tăng giới hạn số beat trong 1 burst giúp tăng performance của hệ thống vì giảm số transaction kênh AW/AR đi và tăng dữ liệu gửi qua kênh R/W.

Đồng thời tín hiệu AWLOCK/ARLOCK giảm từ 2 bit width xuống còn 1 bit width. 

AXI3

 AXI4

Mình nói 1 chút về tín hiệu này. Giả sử có 1 master A. Trường hợp ARLOCK = 10. Lúc này tín hiệu này sẽ control interconnect để chỉ cho master A đi qua. Các master khác phải đợi cho đến khi ARLOCK của master A = 00 thì mới có thể access. Ta có ARLOCK = 10 , Vậy kênh W có thể access không ? Câu trả lời là có. Nó chỉ block các master khác chứ không block các kênh cùng 1 master.



Câu 5: Tại sao không loại bỏ RID hoặc BID (tương tự như loại bỏ WID trong AXI4) ?

Đó là các channel từ slave gửi về. Nếu chúng ta bỏ nó vô tình lúc này kênh R và B cũng sẽ không support out-of-order. Mình lấy ví dụ:

Gửi 2 request đến 2 slave khác nhau A và B.

Đầu tiên ta phát tín hiệu AR đến slave A sau đó đến slave B. Lúc này nếu không dùng ID thì ta phải đợi slave A response về rồi mới nhận slave B. trường hợp slave A response nhanh thì sẽ không sao, ngược lại nếu slave B response nhanh hơp thì lúc này slave A phải đợi B response về mới được response. Có hai ảnh hưởng:

• Ảnh hưởng performance của hệ thống.
• Phải tạo thêm các constraint giữa các slave. Design sẽ trở nên phức tạp hơn.

Câu 6: Phân biệt out-of-order và write data interleaving ?

Out-of-order:  hỗ trợ cho cả kênh R và kênh W.

Write data interleaving: chỉ hỗ trợ cho W channel.


Giả sử ta có 3 transaction, mỗi transaction có 2 beat. Địa chỉ của transaction A được gửi đầu tiên tới B rồi cuối cùng là C.

A (A0, A1)

B (B0, B1)

C (C0, C1)


Out-of-order:

A0, A1, C0, C1, B0, B1


In-oder: 

A0, A1, B0, B1, C0, C1


Write data interleaving: A0, B0, B1, A1, C1, C0.


Lưu ý với out-of-order thì transaction đầu tiên phải ứng với address đầu tiên. Tức là WDATA đầu tiên phải tương ứng với ADDRESS đầu tiên phát ra từ master.


Trong AXI4 nếu có nhiều hơn 2 masters cùng access đến 1 slave. Khối nào sẽ control việc merge các data từ 2 master để đảm bảo không bị interleaving.

Interconect sẽ được thiết kế để đảm bảo điều này. Nếu 2 master có cùng ID gửi xuống slave. Interconnect sẽ giải quyết vấn đề này bằng cách chèn thêm một số bit ID ở đầu các tín hiệu ID. Nghĩa là các tín hiệu ID được mở rộng thêm bit width.

Ví dụ: mình có 4 master A (ARID = 11), B (ARID = 11), C (ARID = 11), D (ARID = 11) cùng gửi request đến slave E. Khi đó interconnect sẽ cần chèn thêm 2 bit đầu để phân biệt 4 master đó như sau:

A (ARID = 0011), B (ARID = 0111), C (ARID = 1011), D (ARID = 1111)

Write data interleave xảy ra khi hai AXI master tạo ra sequence ghi vào cùng một slave, nhưng dữ liệu ghi không đến mỗi chu kỳ xung clock. Trong trường hợp này, thay vì đợi một sequence hoàn thành trước khi chuỗi khác bắt đầu, chuẩn AXI cho phép gửi xen kẽ các chuỗi dữ liệu lại với nhau để tránh lãng phí các chu kỳ xung clock trong hệ thống bus.


Câu 7: Khi master access đến 1 slave có thể vừa có in-oder vừa có out-of-order được gửi xen kẽ nhau không?

Nêu một master access đến 1 slave duy nhất. Lúc này ta có thể thấy nếu các burst có ID trùng nhau thì chúng sẽ được transfer in-order. Nếu các burst có ID khác nhau chúng được transfer out-of-order với các burst có ID khác.

Ví dụ:

Có 4 gói: A (ARID = 1), B (ARID = 3), C (ARID = 2), D (ARID = 2).

Khi đó:

 A, B, C có thể được gửi out-of-order với nhau.

A, B, D có thể được gửi out-of-order với nhau.

C, D phải được gửi in-order.

Trường hợp 1 master access đến nhiều slave. Ví dụ mình có master A gửi 1 burst đến slave B có ARID = 2. Sau đó master này gửi tiếp 1 burst đến slave C có ARID = 2 trong khi chưa nhận được response từ slave B . điều này là violate vì khi data trả về master sẽ không phân biệt được đâu là data response từ B và đâu là từ C (trường hợp out-of-order).

Câu 8: Sự khác biệt giữa RRESP và BRESP ?
Mình giả sử có 1 write transaction và 1 read transaction. Mỗi transaction có 4 beat.

Với kênh read, mỗi beat sẽ được thông báo bởi 1 giá trị  RRESP. Error xảy ra cho từng beat khác nhau.

Ví dụ ta có

Với kênh write, cả 4 beat được control bởi chỉ 1 giá trị BRSEP.

Một số câu lệnh cần thiết khi làm việc với gate net list

Tác giả: TrongTran
Ngày: 09/12/2019


Bài này mình sẽ hướng dẫn các bạn một số câu lệnh tcl để làm việc với gate net list (DC compiler.....).

Tuy nó không đủ nhưng mình tin là với bài viết này và nếu bạn chịu khó đọc thêm thì bạn hoàn toàn có thể hiểu được toàn bộ một môi trường synthesis và làm những công việc với gate cực nhanh (ECO).
Thực tế, một số bạn thích dùng phần mềm trực quan để kiểm tra hoặc debug.
Mình thì dùng cả hai và với một design lớn thì mình thích làm việc với command line hơn. Điều này sẽ giúp bạn rút ngắn được thời gian nhiều hơn.

Mình không làm backend nên mình không biết hết tất cả các lệnh. Mình chỉ nêu ra một số lệnh cần thiết và cơ bản nhất.

Trong bài này mình quy định màu đỏ là cú pháp câu lệnh. Màu xanh là option của câu lệnh và màu đen là phần người dùng điền vào (Có thể là tên biến, key word tìm kiếm ....).


Lệnh đầu tiên mình muốn nói là:

• read_verilog design.v
• current_design /current_block /current_lib
• close_lib design.v

3 lệnh trên có chức năng là:

• Load file Verilog design.v
• Kiểm tra design hiện tại đang được load.
• Đóng file Verilog design.v

get_cell tên_cell

get_cells -[option] tên_cell


Hai câu lệnh trên là nhầm lấy các cell trong một design dựa vào key word trong đã biết.

Ví dụ: bạn muốn lấy 1 cell có chứa key word “AND” bạn dùng lệnh:

get_cells -hierarchical *AND*

Điểm khác biệt giữa get_cells và get_cell là get_cell không dùng được với option còn get_cells thì có.

Một điểm lưu ý nữa là khi bạn có link đầy đủ của 1 cell thì bạn có thể dùng lệnh

get_cells top/AND (Nhớ là không dùng option –hierarchical nhé).

Còn khi bạn chưa biết link instance đầy đủ hoặc cần lấy tất cả các cell chứa key word nào đó bạn dùng lệnh:

get_cells –hierarchical *AND*




get_net tên_net

get_nets –[option] tên_net

Hai câu lệnh này nhầm lấy net name trong design dựa vào key word đã biết. Cách dùng tương tự hai câu lệnh get_cell bên trên.

Để tạo ra một bộ collection của các phần tử (cell, net, port, ….) bạn dùng cặp lệnh:

set NET_COL {}

set NET_COL [add_to_collection $NET_COL [get_nets -hierarchical "AND"]]

Dòng đầu là để khai báo bộ collection tên NET_COL.

Dòng thứ hai là để tìm tất cả các net chứa key word “AND” và lưu vào collection NET_COL.

set NET_TARGET {}

set NET_REMOVE{}

set NET_TARGET [add_to_collection $NET_TARGET [get_nets -hierarchical "AND"]]

set NET_REMOVE [add_to_collection $NET_REMOVE [get_nets -hierarchical "2"]]

set NET_TARGET [remove_from_collection ${NET_TARGET} ${NET_REMOVE}]

Giả sử bạn tìm được các net chứa key word “AND”. Bây giờ bạn cần loại bỏ các net chứa key word số “2” trong bộ collection trên. Tập lệnh bên trên sẽ giúp bạn.

if {[sizeof_collection $NET_TARGET] != 0} {

}

Dòng code trên đang tiến hành kiểm tra xem liệu bộ collection NET_TARGET có chứa phần tử nào không (size # 0), nếu có thì tiến hành các lệnh bên trong dấu ngoặc {}.

foreach_in_collection port_gnd_0 $NET_TARGET {

}

Dòng code trên nhầm lấy từng phần tử trong bộ sưu tập NET_TARGET ra để tiếp tục xử lí bên trong cặp dấu {}. Cái này giống câu lệnh foreach trong cshell nhé.


Lúc bạn lưu net name vào bộ sưu tập NET_COL, các giá trị sẽ lưu dạng 1 phần tử trong design chứ không phải dạng chuỗi.

Nếu bạn muốn chuyển phần tử đó sang dạng chuỗi nhầm dễ xử lí hãy dùng câu lệnh:

set name_2 [get_object_name $port_gnd_0]

Trước khi thực hiện câu lệnh này, bạn phải thực hiện câu lệnh bên trên nhầm chuyển phần tử sang chuỗi nhé. Giả sử trong bộ collection đó, bạn chỉ muốn thao tác với một vài phần tử có chứa key word cụ thể. Bạn nên dùng lệnh bên dưới, Câu lệnh này được dùng thường xuyên luôn nhé, hãy ghi nhớ thật kĩ:

if {[regexp "sync" $name_2]} {

}

Hoặc

if {[regexp {A|B} $name_2]} {

}

Hoặc

if {[regexp {A&B} $name_2]} {

}

Câu lệnh số 2 là nếu chứa key word A hoặc B.

Câu lệnh số 3 là nếu chứa key word A và B.


Bạn đang có 1 collection của các port. Bây giờ bạn muốn chỉ xử lí chỉ các port output. Câu lệnh bên dưới sẽ giúp bạn. Tương tự cho các port input nhé (Thay “out bằng “in”).

if {[get_attribute ${port} direction] == "out"} {

}

Để kiểm tra xem port /net cụ thể có bao nhiêu phân nhánh mình có câu lệnh bên dưới:

set fanout_name [sizeof_collection [all_fanout -from [get_ports “AND”]]]

Câu lệnh để kiểm tra xem có tồn tại thư mục với tên nào đó không. Ta có câu lệnh sau:

if { [file exists $FOLDER] && [file isdirectory $FOLDER] } {

}

In ra một chuỗi, Bạn có lệnh sau:

puts “Hello world”

Để chạy 1 script viết bằng ngôn ngữ khác trong file tcl, Bạn có câu lệnh sau:

exec ./run.pl

Đễ chạy 1 câu lệnh cshell trong file tcl bạn chạy lệnh như bên dưới:

sh mkdir folder

Khi bạn có 1 link của instance name và bạn muốn biết module name của instance này là gì trong design hãy dùng câu lệnh sau:

get_attribute top/sub_0/sub_1 ref_name

Câu lệnh get_attribute rất mạnh nhé. Hãy vào chế độ command line của các tool và chạy lệnh:

man get_attribute

Để biết được hướng dẫn của chúng.

Nếu bạn còn có câu lệnh nào chưa biết hãy gửi mail hoặc comment góp ý với mình nhé.

Thảo luận 1 lỗi mismatch bit width trong thiết kế verilog rất khó được phát hiện

Tác giả: TrongTran
Ngày: 05/12/2019

Trước đây mình có trình bày về 1 issue liên quan đến lỗi 2 output được connect vào 1 port.
Trong bài này, Đây là 1 bug mới mà một anh trong công ty mình tạo ra. Với hầu hết các lỗi liên quan đến mismatch bit width thì các tool sẽ phát hiện được. Nhưng lỗi này, Mình đã tiến hành kiểm tra bằng nhiều loại tool và kết quả là không phát hiện được.

Mình xét ví dụ nhỏ:

Trong ví dụ trên mình muốn các bạn đặt sự tập trung vào dòng nằm trong hình chữ nhật đỏ bên trên.

Function của module này cơ bản chỉ là:

• 2 input XOR với nhau sau đó đi qua mạch 2 flip flop. 

Tuy nhiên, ở đây mình cố tình khai báo biến reg async_ff có 1 bit width. Điều này sẽ dẫn đến mismatch bit width vì biến result là 1 signal có 2 bit data. Như vậy mismatch bit width sẽ diễn ra tại dòng 31 và 32 trong hình trên.

Điều gì sẽ xảy ra?

Mình đã chạy hàng loạt các tool để kiểm chứng kết quả là:

• VCS không warning cũng không error.
• Cadence incisive không warning cũng không error.
• Cadence xcelium không warining cũng không error.
• Synthesis  không warning không error và formality vẫn pass.

Mọi thứ quá hoàn hảo để không phát hiện được issue này.

Bây giờ hãy thử kiểm tra function nhé:

Mình có 1 test bench như bên dưới:

module tb();

  

  reg [1:0] in_0;

  reg [1:0] in_1;

  wire [1:0] out;

  reg clk;

  

  

  initial begin

     clk = 1;

     forever #10 clk = ~clk;

  end

  

  top top_0 (.clk(clk), .in_0(in_0), .in_1(in_1), .out(out));

  

  initial begin

    #20;

    in_0 = 2'b00;

    in_1 = 2'b11;

    #20;

    in_0 = 2'b00;

    in_1 = 2'b00;

    #20;

    in_0 = 2'b11;

    in_1 = 2'b11;

    #20;

    in_0 = 2'b10;

    in_1 = 2'b11;

    #20;

    in_0 = 2'b10;

    in_1 = 2'b01;

    #20;

    $finish();

  end

    initial begin

         $dumpfile("dump.vcd");

          $dumpvars(0, tb);

     end  

endmodule

Và đây là waveform:

Vì kết quả bị delay 2 chu kì nên vòng xanh thứ nhất là input

in_0 = 2'b00;

in_1 = 2'b11;

Nếu in_0 ^ in_1 = 2'b11;

Thực tế kết quả là 2'b01.

Biến mismatch đã được fix giá trị 0.

Các bạn có thấy lạ không. Vì rõ ràng là biến result tại dòng 13 đã được gán 

result = in_0 ^ in_1;

nên giá trị phải là 1 chứ nhỉ ? và giá trị out[1] không bị delay 2 chu kì như out[0] vì out[1] không qua 2 flip flop do mismatch bit width ?

Không phải nhé, Thực ra giá trị out[1] = 0 là chính xác đấy. Lí do chỉ có out[0] được gán tại dòng 32, còn out[1] không được gán giá trị nên sẽm ang giá trị 0. Biến result khác out nhé.

Như vậy check function sẽ phát hiện được lỗi này.

Thế nhưng bạn có chắc bạn check đủ case cho nó. Mình vừa đối mặt issue này bởi signal sai là signal STROBE trong kênh W channel.

Thường thì chúng ta không verify đủ case của tín hiệu này. Ví dụ: 

WDATA có 64 bit bạn phải check đủ các case cho tín hiệu 0f, ff.....

Hãy thận trọng.

Gate netlist cũng sẽ fix 0 cho tín hiệu gán thiếu như bên dưới:

module top (clk, in_0, in_1, out) ;

    input  clk ;

    input  [1:0] in_0 ;

    input  [1:0] in_1 ;

    output [1:0] out ;

    wire net_2 ;

    wire net_1 ;

    wire result ;

    wire FLT_1 ;

    wire FLT_2 ;

    sub_top_0 sub_0 (.clk(clk), .result({FLT, result}), .out({FLT, net_1}));

    XOR2 xor_0 (.A1(in_0[0]), .A2(in_1[0]), .Z(result));

    BUFF buf_1 (.I(1'b0), .Z(net_2));

    BUFF buf_2 (.I(net_2), .Z(out[1]));

    BUFF buf_3 (.I(net_1), .Z(out[0]));

endmodule

module sub_top_0 (clk, result, out);

    input  clk;

    input  [1:0] result;

    output [1:0] out;

    wire [0:0] async_ff;

    DFF dff_1 (.D(async_ff[0]), .CP(clk), .Q(out[0]));

    DFF dff_2 (.D(result[0]), .CP(clk), .Q(async_ff[0]));

endmodule

Thế thì spyglass có phát hiện lỗi này. Câu trả lời là có mà là WARNING ???????

Bạn sẽ nhận được mã sau:

RP_UnmatchWidth    4.4.1(3)       Warning     top.v    31      10    Bit width of LHS does not match with RHS on the assignment

RP_UnmatchWidth    4.4.1(3)       Warning     top.v    32      10    Bit width of LHS does not match with RHS on the assignment

Nhưng với một design lớn. Có hàng ngàn mã lỗi như vậy. Vì sao? Một số case như sau:

wire [3:0] b;

assign b = 0;

Vâng, Cái này nó cũng warning y như cái trên đấy. Còn một vài case nữa nhưng mình ko tiện nêu ra. Do đó không phải dễ để tìm ra lỗi này. Hãy thận trọng confirm tất cả error dạng này nhé.

Qua 2 issue mình nêu bạn sẽ thấy sức mạnh của tool spyglass từ synopsys mạnh như thế nào. Hãy tận dụng nó một cách có hiệu quả, bạn sẽ tránh được các issue không đáng có.

Mọi góp ý về issue này hãy call cho mình nhé: 0339339692.

Code ví dụ cho bạn nào muốn trial lại:

module top (clk, in_0, in_1, out);

    input [1:0] in_0;

    input [1:0] in_1;

    output [1:0] out;

    input clk;

    wire [1:0] out;

    wire [1:0] result;

    sub sub_0 (.clk(clk), .result(result), .out(out));

    assign result = in_1 ^ in_0;

endmodule

module sub (clk, result, out);

   input clk;

   input [1:0] result;

   output[1:0] out;

   reg [0:0] async_ff;

   reg [1:0] out;

   always @(posedge clk) begin

         async_ff <= result;

         out <= async_ff;

   end

endmodule

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