Solve-before: cùng tập nghiệm, khác cách chọn mẫu

Hiếm vì ít nghiệm, hay vì generator chưa kiểm đúng?

Một generator có bit gate và chỉ số item 3 bit. Khi gate bằng 1, item phải là 6 hoặc 7; khi gate bằng 0, cả tám chỉ số đều được phép. Người viết test muốn quan sát nhánh gate bằng 1 thường xuyên hơn, nhưng vẫn phải giữ những cặp hợp lệ của nhánh còn lại.

Đây là hai câu hỏi khác nhau: những cặp nào được dùng làm stimulus, và generator có xu hướng chọn chúng theo tỷ lệ nào. Thêm điều kiện để cấm nhánh gate bằng 0 sẽ thay bài toán; hướng giải biến bằng solve ... before phục vụ một mục đích khác.

Quan hệ được xét từ cả hai phía

Rule trong thí nghiệm là gate -> item inside {6,7}. Khi pin item bằng 0, solver chỉ còn gate bằng 0. Khi pin gate bằng 1, item còn hai lựa chọn 6 và 7. Sự suy luận từ phía item không biến implication thành equivalence: item bằng 6 với gate bằng 0 vẫn hợp lệ.

“Bidirectional” ở đây mô tả việc giải các biến có quan hệ, không phải chạy hai lệnh gán, một thứ tự thời gian hoặc hai hướng của một bus. Muốn kiểm chiều suy luận, hãy pin phía được xem là đầu vào của tình huống và đối chiếu tập giá trị còn lại.

Tính 10 nghiệm trước khi xem bất kỳ mẫu ngẫu nhiên nào

Có 16 cặp trong miền kiểu dữ liệu. Gate bằng 0 cho tám cặp, gate bằng 1 cho hai cặp; tổng cộng 10 hợp lệ và 6 bị loại. Hai class trong ví dụ dùng đúng cùng quan hệ; một class thêm solve gate before item.

Testbench pin đủ 16 cặp cho từng class. Kỳ vọng là 32 lần giải, 20 thành công và 12 thất bại. Việc class có solve-before cùng chấp nhận 10 cặp không chứng minh solver có phân phối mong muốn; nó chỉ kiểm rằng thí nghiệm không vô tình làm đổi tính hợp lệ.

Hai phép tính xác suất với giả định khác nhau

Để hiểu động cơ, xét hai mô hình toán học sau, không xem chúng là kết quả đo của một seed:

• Nếu chọn đều trong 10 cặp hợp lệ, nhánh gate bằng 1 chiếm 2/10 = 1/5. Mỗi cặp có trọng số 1/10.
• Nếu chọn gate đều trước, rồi chọn đều item hợp lệ với gate ấy, gate bằng 1 có trọng số 1/2. Tám cặp của gate bằng 0 có trọng số 1/16 mỗi cặp; hai cặp của gate bằng 1 có trọng số 1/4 mỗi cặp.

Cả hai mô hình cộng thành 1 và có cùng 10 cặp. Nguồn đào tạo dùng cách so sánh này để giải thích solve-before. Không lấy 64 mẫu trong testbench làm bằng chứng mọi simulator thực hiện chính xác các tỷ lệ trên; phần quy tắc ngôn ngữ vẫn cần đối chiếu LRM.

Thứ tự giải không thêm một điều kiện cấm

Trong class có thứ tự, solve gate before item nêu quan hệ ưu tiên giải giữa hai biến random. Nó không yêu cầu gate bằng 1 và cũng không bỏ rule hiện có. Vì thế pin gate bằng 1 cùng item bằng 2 vẫn phải thất bại.

Nếu cần một test chỉ sinh nhánh đặc biệt, pin gate bằng 1 là cách biểu đạt yêu cầu cụ thể. Nếu cần giữ cả hai nhánh mà điều chỉnh cách chọn, đó là câu chuyện về phân phối. Đừng thay một yêu cầu bằng cái còn lại chỉ vì histogram ngắn trông thuận mắt.

Tách phép kiểm tập nghiệm khỏi phép đo tần suất

Testbench có một hàm oracle thường: gate bằng 0 đi với item từ 0 đến 7; gate bằng 1 chỉ đi với 6 hoặc 7. Oracle không gọi constraint của class. Mỗi lần pin phải khớp return code; với call thành công, cả hai field phải đúng giá trị được pin.

Sau vét cạn, 64 call tự do cho mỗi class được kiểm tính hợp lệ, tổng 128 mẫu. Hai call riêng kiểm suy luận item bằng 0 ép gate bằng 0 và gate bằng 1 giới hạn item ở 6 hoặc 7. Mọi mẫu đều được kiểm sau khi xác nhận randomize thành công.

Đừng kết luận phân phối từ một vài lần in display

Một seed phục vụ tái hiện trong cấu hình tool đã ghi; nó không là một sequence portable giữa các simulator. Tỷ lệ gate bằng 1 trong 64 call có thể lệch khỏi một xác suất lý tưởng. Ngược lại, một histogram trông cân bằng cũng chưa chứng minh generator giữ tất cả nghiệm cần thiết.

Mutation của bài sẽ làm mất một giá trị hợp lệ ở nhánh gate bằng 1. Checker vét cạn phải bắt được ngay, thay vì đợi một mẫu ngẫu nhiên tình cờ đi vào nhánh đó. Thí nghiệm không đo độ đồng đều hay claim solve-before trên randc, array hoặc thứ tự giải vòng.

Đối chiếu 32 pin và 128 mẫu tự do

Expected tính trước chạy: 20 accept, 12 reject, 128 mẫu hợp lệ và 2 phép kiểm suy luận. UNSATCONSTR tại những pin bị loại là diagnostic dự kiến; chúng không phải các call thành công.

`timescale 1ns/1ps// Expected before execution: 16 pins per class; 10 legal and 6 illegal each.// No sampled frequency is treated as a proof of a probability distribution.class JointChoice;  rand bit gate;  rand bit[2:0] item;  constraint legal {gate -> item inside {6,7};}endclassclass OrderedChoice;  rand bit gate;  rand bit[2:0] item;  constraint legal {gate -> item inside {6,7}; solve gate before item;}endclassmodule tb_solve_before;  JointChoice joint; OrderedChoice ordered;  int accepted=0,rejected=0,samples=0;  function automatic bit oracle(input int g,v);    return (g==0 && v>=0 && v<=7)||(g==1 && (v==6||v==7));  endfunction  initial begin    joint=new();ordered=new();joint.srandom(71);ordered.srandom(73);    for(int g=0;g<2;g++)for(int v=0;v<8;v++)begin      int r1,r2;bit expected_ok;      expected_ok=oracle(g,v);joint.gate=1;joint.item=2;ordered.gate=1;ordered.item=2;      r1=joint.randomize() with {gate==local::g;item==local::v;};      r2=ordered.randomize() with {gate==local::g;item==local::v;};      if(r1!=int'(expected_ok)||r2!=int'(expected_ok))$fatal(1,"solve-before legal-set oracle");      if(r1)begin        if(joint.gate!=g||joint.item!=v||ordered.gate!=g||ordered.item!=v)$fatal(1,"pin ignored");        accepted+=2;      end else begin        if(joint.gate!=1||joint.item!=2||ordered.gate!=1||ordered.item!=2)$fatal(1,"failed call changed fields");        rejected+=2;      end    end    repeat(64)begin      if(!joint.randomize()||!ordered.randomize())$fatal(1,"sample failed");      if(!oracle(int'(joint.gate),int'(joint.item))||!oracle(int'(ordered.gate),int'(ordered.item)))$fatal(1,"sample illegal");      samples+=2;    end    // One-way implication, but solving the relation is bidirectional.    if(!ordered.randomize() with {item==0;} || ordered.gate!=0)$fatal(1,"reverse inference failed");    if(!ordered.randomize() with {gate==1;} || !(ordered.item inside {6,7}))$fatal(1,"forward inference failed");    if(accepted!=20||rejected!=12||samples!=128)$fatal(1,"accounting");    $display("SOLVE CHECK pinned=32 accepted=20 rejected=12 sampled=128 inferred=2");    $finish;  endendmodule

^[1]

Tự kiểm tra

Hợp lệ trước, trọng số sau

Bắt đầu từ miền kiểu dữ liệu và liệt kê tập nghiệm. Sau đó nói rõ yêu cầu của test là ép tình huống, đổi cách lấy mẫu hay đo mức phủ. Mỗi yêu cầu cần phép kiểm riêng; không dùng một biểu đồ tần suất để thay cho oracle tính hợp lệ.

^[2]