Race conditions: một lần chạy đúng chưa đủ

Pass ổn định vẫn có thể giấu race

Một regression chạy trăm lần đều pass có thể chỉ lặp lại cùng một thứ tự thực thi. Nếu code cần thứ tự đó nhưng ngôn ngữ không bảo đảm nó, việc đổi simulator hoặc sửa code xung quanh có thể làm lộ lỗi.

Race là sự phụ thuộc của kết quả vào thứ tự tương đối chưa được bảo đảm, không phải yêu cầu simulator phải ngẫu nhiên đổi kết quả mỗi lượt. Vì vậy ta sẽ suy luận hai thứ tự trước, sau đó mới xem lịch mà Icarus đã chọn trong lần chạy thật. ^[1]

Tìm cặp đọc và ghi cạnh tranh

Hai process đều thức dậy tại posedge clk:

always @(posedge clk) racy_a = 1;
always @(posedge clk) racy_b = racy_a;

racy_a trước cạnh đầu bằng 0. Process thứ nhất ghi racy_a; process thứ hai đọc racy_a để ghi biến khác. Dù mỗi biến chỉ có một writer sau khởi tạo, quan hệ read-after-write giữa hai process vẫn tạo nguy cơ race khi chúng thực hiện blocking trong cùng Active.

Không cần hai process cùng ghi một biến mới có race. Cũng không đủ thấy chúng cùng timestamp để khẳng định race: nếu chỉ đọc dữ liệu ổn định hoặc truy cập biến độc lập thì thứ tự có thể không ảnh hưởng kết quả. ^[2]

Hai thứ tự hợp lệ cho ra hai kết quả

• Writer chạy trước: racy_a nhận 1 rồi reader lấy 1, nên racy_b=1.
• Reader chạy trước: nó lấy racy_a cũ 0, sau đó writer mới ghi 1, nên racy_b=0.

TB xây dựng hai mô hình tuần tự có chủ ý để kiểm phép tính này. Đây là hai reference order, không phải bằng chứng simulator đã chạy hai lịch của cùng đoạn racy code. Lượt mô phỏng thực chỉ in một dòng RACE OBSERVED first_b=... với giá trị nó thật sự gặp.

Thứ tự process trong file không phải cách chọn winner một cách portable. Ngay cả hai initial ghi hai giá trị khác nhau tại t=0 cũng là ví dụ nondeterminism trong nguồn đào tạo. ^[3]

NBA làm thứ tự đọc không còn ảnh hưởng ở đây

Ở pipeline đúng, hai process là stage1 <= data và stage2 <= stage1, cùng posedge. Cả hai đọc RHS trước khi các LHS này được cập nhật ở NBA. Với stage1 cũ 0 và data 1, state sau cạnh đầu phải là stage1=1, stage2=0.

Process nào được chạy trước trong Active không còn làm stage2 nhìn thấy stage1 mới của cạnh này. Đó là điều cần để giữ hai tầng thanh ghi. Nguồn đào tạo giải thích cùng cơ chế; quy tắc đầy đủ vẫn ^[4].

Tuy nhiên, sửa race không tự bảo đảm latency đúng yêu cầu sản phẩm. Nếu yêu cầu cần kết quả tổ hợp trong cùng chu kỳ, bạn phải thiết kế đường dữ liệu phù hợp, không chỉ thêm một tầng rồi gọi là đã sửa. ^[5]

Đổi mọi dấu bằng thành NBA chưa đủ

Lập luận pipeline trên dựa vào một writer cho mỗi stage và data ổn định trước cạnh. Hai process độc lập cùng ghi NBA khác giá trị vào một biến không được giải quyết chỉ bằng dấu <=: bạn vẫn cần xác định quyền sở hữu và ưu tiên.

Nếu TB đổi data bằng blocking đúng posedge DUT lấy mẫu, DUT vẫn có thể đọc dữ liệu trước hoặc sau lần đổi ấy, dù DUT dùng NBA để ghi output. NBA tách lúc cập nhật output; nó không sửa hợp đồng stimulus đầu vào bị vi phạm.

Quy ước phổ biến là NBA cho state tuần tự, blocking cho tính toán tổ hợp và tránh nhiều process cùng sở hữu một biến. Đây là hướng dẫn coding; không nên biến mọi trường hợp trộn assignment thành một phát biểu “cú pháp luôn bất hợp lệ”. ^[6]

Stimulus và checker cũng có hợp đồng thời điểm

Clock TB có posedge tại 5,15,25 ns. Data ban đầu 1, đổi 0 tại 10 ns và 1 tại 20 ns, cách xa các cạnh lấy mẫu. Checker đọc tại 6,16,26 ns, sau NBA của cạnh vừa thử.

Hợp đồng cụ thể này cho chuỗi state dự đoán trước là 10, 01, 10. Thêm một negedge DUT hoặc clock khác có thể làm thời điểm đang an toàn trở thành thời điểm lấy mẫu mới; không áp dụng máy móc “drive ở negedge luôn hết race”.

Clocking block là công cụ SystemVerilog để quy định sampling/drive skew rõ hơn; bài hiện tại không mô phỏng nó và không suy ra “bất kỳ skew nào cũng đúng”. Việc chọn đọc state trước hay sau cạnh phải theo yêu cầu scoreboard. ^[7]

Đối chiếu race với ba cạnh pipeline đã sửa

Trước chạy: hai mô hình thứ tự cho b lần lượt 1 và 0; racy observation được phép là một trong hai. Riêng pipeline sửa phải khớp chính xác cả ba cặp state sau NBA.

module tb_races;  timeunit 1ns;  timeprecision 1ps;  reg clk = 0, data = 1;  reg racy_a = 0, racy_b = 0;  reg stage1 = 0, stage2 = 0;  reg model_a, model_b, writer_first, reader_first;  int checked_edges = 0;  always #5 clk = ~clk;   // Deliberately unsafe: a write and a read depend on Active process order.  always @(posedge clk) racy_a = 1;  always @(posedge clk) racy_b = racy_a;   // Two owners, one variable per owner; both RHS use pre-edge state.  always @(posedge clk) stage1 <= data;  always @(posedge clk) stage2 <= stage1;   // This clock has posedges at 5/15/25ns; drive at 10/20ns.  initial begin #10; data = 0; #10; data = 1; end   task automatic check_pipeline(input reg first, input reg second);    if (stage1 !== first || stage2 !== second)      $fatal(1, "pipeline mismatch at=%0d expected=%b%b actual=%b%b",             int'($time), first, second, stage1, stage2);    checked_edges = checked_edges + 1;    $display("SAFE EDGE n=%0d at=%0d stages=%b%b", checked_edges, int'($time), stage1, stage2);  endtask   initial begin    // Two explicit serial reference models, NOT two scheduler observations.    model_a = 0; model_a = 1; model_b = model_a; writer_first = model_b;    model_a = 0; model_b = model_a; model_a = 1; reader_first = model_b;    if (writer_first !== 1 || reader_first !== 0)      $fatal(1, "reference order model mismatch");    $display("ORDER MODELS writer_first=%b reader_first=%b", writer_first, reader_first);    #6; // First posedge and its NBA updates have completed.    if (racy_a !== 1 || (racy_b !== 0 && racy_b !== 1))      $fatal(1, "unexpected racy value outside the two modeled outcomes");    $display("RACE OBSERVED first_b=%b", racy_b);    check_pipeline(1, 0);    #10; check_pipeline(0, 1);    #10; check_pipeline(1, 0);    if (checked_edges != 3) $fatal(1, "missing edge check");    $display("RACE CHECK safe_edges=%0d", checked_edges);    $finish;  endendmodule

TB dùng case inequality để bắt cả X/Z bất ngờ, kiểm đủ ba cạnh và $fatal nếu pipeline sai. Regex chấp nhận 0/1 chỉ dành cho tín hiệu cố ý race. Đặt một expected duy nhất cho tín hiệu đó rồi gọi các simulator khác là sai sẽ làm sai mục tiêu bài học.

Output và assertions xác nhận thí nghiệm đã chạy bằng Icarus. Chúng không chứng minh mọi lịch scheduler, không phải race detector và không claim synthesis. ^[8]

Debug từ quan hệ phụ thuộc, không từ seed may mắn

Khi gặp khác biệt sau nâng tool, làm theo chuỗi kiểm tra:

1. Chỉ rõ output sai ở cạnh nào, yêu cầu cần state cũ hay mới.
2. Liệt kê tất cả writer và reader của biến tại cạnh đó, gồm cả TB.
3. Với mỗi reader, hỏi producer đã cập nhật chắc chắn chưa hay chỉ tình cờ chạy trước.
4. Sửa ownership/sampling/update; lập expected cho độ trễ sau sửa trước khi chạy lại.
5. Kiểm nhiều giá trị đầu vào để tránh pass vì dữ liệu cũ và mới tình cờ giống nhau.

Bài tập suy luận: nếu data luôn 0 và cả hai stage khởi tạo 0, pipeline mất tầng vẫn có thể nhìn đúng trong log. Vì thế TB dùng data 1/0/1. Nếu đổi stage2 thành lấy trực tiếp data, cạnh đầu phải bị assertion bắt vì state thành 11 thay vì 10.

Không dùng #0, đổi thứ tự file hoặc tăng số seed như bằng chứng rằng nguyên nhân race đã được loại bỏ. Những thay đổi ấy có thể giúp quan sát lỗi nhưng không thay lập luận về quan hệ đọc/ghi.

Tự kiểm tra

Loại bỏ sự phụ thuộc vào thứ tự không được hứa

Một tín hiệu cố ý race được quan sát, còn pipeline đã sửa có hợp đồng chính xác để kiểm. Hai việc ấy có mức bằng chứng khác nhau: thấy một kết quả hợp lệ không chứng minh chỉ có kết quả đó.

Tìm đúng cặp đọc/ghi, đặt một writer cho mỗi state và xác định thời điểm stimulus/checker. Bài giữ draft/needs-spec-check với LRM dù code đã có kiểm chứng thực nghiệm.