Debug randomization: khoanh vùng xung đột trước khi đổi seed

Return 0 là tín hiệu cần điều tra, không phải một mẫu khác

Một generator có value 3 bit, ceiling bằng 5, rule chẵn và allowed_codes gồm 2, 4, 6. Khi một request thất bại, đừng bỏ qua return code rồi dùng giá trị đang nằm trong object. Nó chưa được xác nhận là stimulus hợp lệ cho request ấy.

Đổi seed không làm hai hard rule mâu thuẫn trở nên tương thích. Trước tiên phải xác định type domain, state đang giữ, inline pin và tất cả constraint có liên quan; sau đó mới xem cơ chế lấy mẫu hoặc khả năng của tool.

Tính giao tập nghiệm bằng tay

Miền kiểu dữ liệu là 0 đến 7. Ceiling 5 giữ 0 đến 5. Rule chẵn giữ 0, 2, 4, 6. Allowed_codes giữ 2, 4, 6. Giao cuối cùng chỉ có 2 và 4.

Main pin từng giá trị 0 đến 7. Kỳ vọng là 2 accept và 6 reject; giá trị được pin không được tự đổi thành một giá trị khác rồi báo thành công. Bảng miền nhỏ là oracle đầu tiên để phân biệt generator sai với request không thể thỏa.

Field bị giữ vẫn tham gia bài toán

Test đặt value bằng 3 rồi tắt rand_mode của field. Khi đó randomize không được chọn lại value để cứu request. Ceiling vẫn cho phép 3, nhưng rule chẵn và allowed_codes đều không cho phép.

Call phải trả 0. Đó là một request vô nghiệm theo contract hiện tại, không phải bằng chứng seed xấu. State được giữ và mode phải được ghi vào log tái hiện, cùng cấu hình tool và phiên bản source.

Tắt một rule chưa chắc đã gỡ hết xung đột

Test tắt riêng even_value; call vẫn phải thất bại vì allowed_codes còn loại 3. Sau đó tắt allowed_codes; giờ chỉ ceiling đang áp dụng cho value bị giữ, nên call có thể thành công và giữ 3.

Ba mốc fail, fail, success giúp khoanh vùng hai ràng buộc cùng gây xung đột. Nó không biến 3 thành stimulus hợp lệ của generator gốc. Việc tắt mode ở đây là thí nghiệm chẩn đoán, không phải cách sửa specification.

^[1]

Khôi phục contract trước khi tiếp tục test DUT

Main bật lại hai constraint và rand_mode, rồi thực hiện 32 call tự do. Mỗi call phải thành công và value phải thuộc tập 2 hoặc 4. Bỏ sót bước khôi phục có thể làm những ca kiểm sau âm thầm kiểm một miền khác.

Khi dùng helper debug trong một testbench lớn, hãy ghi nhận trạng thái ban đầu và có đường khôi phục ngay cả khi bước chẩn đoán phát hiện lỗi. Main ở đây là chuỗi nhỏ cố định; nó không mô phỏng cơ chế exception hoặc mọi kiểu cleanup của một framework.

Phân phối không thay việc tính miền hợp lệ

Dist gắn trọng số cho giá trị; cú pháp := và :/ xử lý trọng số của range khác nhau theo nguồn đào tạo. Tính trọng số trong một mô hình phải được tách khỏi phép kiểm field có hợp lệ với các hard rule khác hay không.

Một probe riêng kết hợp dist, cận trên và inline pin không khớp return-code oracle trên Verilator 5.050 đã ghi. Main của bài dùng membership tường minh để kiểm luồng debug; nó không claim dist+inline hoặc một tỷ lệ xác suất đã được engine thực hiện đúng.

^[2]

Tách ba loại bằng chứng

Request có giao tập rỗng là lỗi cấu hình hay kỳ vọng của test. Một mẫu return 1 nhưng sai oracle là khác biệt thực thi cần điều tra ở code/tool. Cuối cùng, một miền hợp lệ chưa được hit đủ là câu chuyện về coverage và lấy mẫu; hai vấn đề trước không được sửa bằng cách chỉ chạy thêm seed.

Các diagnostic UNSAT cho pin cố ý vô nghiệm được giữ. Lỗi giao tiếp solver, parse/build fail hoặc assertion bị bắt trong capability probe được ghi đúng loại, không đổi expected để gọi là simulation pass.

8 pin, 3 mốc chẩn đoán và 32 call sau khôi phục

Expected tính trước chạy: 2 accept/6 reject trong 8 pin; ba mốc chẩn đoán; 32 call sau khôi phục đều thuộc 2 hoặc 4. Mẫu tạm cho phép 3 không được dùng làm bằng chứng generator gốc hợp lệ.

`timescale 1ns/1ps// Explicit membership excludes0; upper bound5 excludes6. Legal pins are2 and4.class DebugChoice;  rand bit[2:0] value;  bit[2:0] ceiling=5;  constraint upper {value<=ceiling;}  constraint even_value {value[0]==0;}  constraint allowed_codes {value inside {2,4,6};}endclassmodule tb_debug;  DebugChoice item;  int accepted=0,rejected=0,samples=0,triage=0;  initial begin    item=new();item.srandom(113);    for(int pin=0;pin<8;pin++)begin      int result;bit legal;      legal=(pin==2||pin==4);      result=item.randomize() with {value==local::pin;};      if(result!=int'(legal))$fatal(1,"debug legal-set oracle");      if(result)begin if(item.value!=pin)$fatal(1,"debug pin ignored");accepted++;end      else rejected++;    end    item.value=3;item.value.rand_mode(0);    if(item.randomize()!=0)$fatal(1,"held odd value accepted");triage++;    item.even_value.constraint_mode(0);    if(item.randomize()!=0)$fatal(1,"membership conflict ignored");triage++;    item.allowed_codes.constraint_mode(0);    if(!item.randomize()||item.value!=3)$fatal(1,"triage release failed");triage++;    item.even_value.constraint_mode(1);item.allowed_codes.constraint_mode(1);item.value.rand_mode(1);    repeat(32)begin      if(!item.randomize()||!(item.value inside {2,4}))$fatal(1,"restored debug oracle");samples++;    end    if(accepted!=2||rejected!=6||samples!=32||triage!=3)$fatal(1,"debug accounting");    $display("DEBUG CHECK pinned=8 accepted=2 rejected=6 sampled=32 triage=3 restored=1");    $finish;  endendmodule

^[3]

Tự kiểm tra

Repro nhỏ phải giữ cả state và oracle

Lưu source, tool, seed, state trước call và mode đang bật. Thu nhỏ miền để tính nghiệm bằng tay, kiểm return code trước khi đọc dữ liệu, rồi đối chiếu mẫu thành công với oracle độc lập. Một bộ test xanh chỉ có nghĩa trong phạm vi các assertion đã thực sự được chạy.