Array randomization: kiểm shape, phần tử và tổng riêng biệt

Một array đúng phần tử nhưng sai chiều dài vẫn là stimulus sai

Một generator cần 1 đến 3 phần tử, mỗi phần tử từ 0 đến 3 và tổng không vượt 6. Kiểm riêng từng giá trị chưa đủ: array rỗng hoặc có thêm một phần tử đều có thể làm testbench gửi sai giao dịch kiểm thử.

Main dùng dynamic array có phần tử int unsigned. Caller chọn requested_count trước mỗi call; pre_randomize cấp phát đúng chiều dài ấy. Đây là thiết kế hai giai đoạn có chủ ý, không claim tool đã đồng thời randomize chiều dài và toàn bộ nội dung theo mọi constraint.

Ràng buộc shape và cách chuẩn bị bộ nhớ

Requested_count là state, không phải field rand trong main. Pre callback cấp phát array mới theo state đó; constraint yêu cầu requested_count trong 1 đến 3 và payload.size bằng requested_count. Việc cấp phát không thay cho phép kiểm shape sau call thành công.

Foreach chỉ đặt yêu cầu cho những index hiện có. Một vòng foreach không tự tạo thêm phần tử, nên không dùng nó để thay một yêu cầu về chiều dài. Nguồn đào tạo có mô hình randomize size và nội dung; scope tool của main được ghi hẹp hơn, còn probe joint-size giữ failure thật.

^[1]

Miền phần tử phải được kiểm trước khi cộng

Constraint domain yêu cầu từng payload[i] từ 0 đến 3. Oracle duyệt từng phần tử sau call thành công, từ chối giá trị ngoài miền rồi mới chuyển kiểu và cộng tổng. Cách làm này tránh để một giá trị lỗi quá lớn bị cast hoặc overflow làm phép kiểm tổng trông hợp lệ.

Ở chế độ pin, caller cung cấp pin_value và yêu cầu mọi phần tử bằng giá trị đó. Ở chế độ tự do, rule pin được tắt; constraint domain và budget vẫn áp dụng cho từng array được sinh ra.

Không suy độ rộng tổng từ số phần tử

Với ba phần tử tối đa 3, tổng toán học có thể là 9. Main dùng phần tử 32 bit và expression sum với cast int; oracle cộng vào int sau khi đã kiểm miền. Trong miền nhỏ này, tổng tối đa 9 không thể overflow int.

Một probe khác dùng phần tử 2 bit và phép reduction có cast rộng hơn. Tool đã ghi lỗi sort ở giao tiếp solver rồi không khớp oracle. Bài giữ probe riêng và không dùng main 32 bit để tuyên bố mọi phép widening trên narrow array đã chạy đúng.

16 trạng thái điều khiển, không phải mọi array có thể có

Test quét requested_count từ 0 đến 3 và pin_value từ 0 đến 3. Count 0 bị loại ở cả bốn pin. Count 1 nhận bốn giá trị; count 2 nhận cả bốn vì tổng tối đa 6; count 3 chỉ nhận 0, 1 hoặc 2, còn ba phần tử 3 có tổng 9.

Kết quả dự kiến là 11 call thành công và 5 call thất bại. Các call thành công chứa 4 + 8 + 9 = 21 phần tử được đối chiếu từng index. Đây là vét cạn 16 cấu hình pin-đồng-giá-trị, không phải vét cạn mọi vector của mọi chiều dài.

Nội dung tự do vẫn cần oracle

Main tắt chế độ pin rồi thực hiện 64 call, caller luân phiên chiều dài 1, 2 và 3. Mỗi call phải thành công và được kiểm size, miền của từng phần tử và tổng không vượt 6. Không giả định generator chọn đều các chiều dài: chiều dài trong đoạn này do caller điều khiển.

Khi một call thất bại, main không tiêu thụ array của call ấy. Pre callback có cấp phát state trước việc giải, nên không gán ý nghĩa “array cũ còn nguyên” nếu chưa có bằng chứng riêng.

Phân biệt bài toán, phép mã hóa và khả năng tool

Hai probe được giữ: mô hình joint random count/array với inline pin không giữ được shape theo oracle; mô hình narrow-array sum có lỗi kiểu bit-vector ở solver. Chúng không bị bỏ assertion để nhập vào danh sách PASS.

Main dùng count có sẵn, preallocation và phần tử int unsigned với miền nhỏ. Không suy từ đây sang array dài tùy ý, mọi queue, unique array hoặc resize đồng thời nhiều biến. Khi chuyển simulator, cần chạy lại cả main lẫn probe trước khi thay phạm vi bằng chứng.

21 phần tử pin và 64 mẫu nội dung tự do

Expected tính trước chạy: 16 cấu hình điều khiển, 11 accept, 5 reject và 21 phần tử pin. Thêm 64 call thành công được kiểm độc lập. Hai capability failure không được tính là thành công mô phỏng của main.

`timescale 1ns/1ps// Caller chooses count; pre_randomize allocates before content solving.// Uniform-value pin controls: count1 accepts4, count2 accepts4, count3 accepts3 =11/16.class ArrayShape;  int requested_count,pin_value;  bit pin_enabled;  rand int unsigned payload[];  constraint shape {requested_count inside {[1:3]};payload.size()==requested_count;}  constraint domain_values {foreach(payload[i]) payload[i] inside {[0:3]};}  constraint pins {if(pin_enabled)foreach(payload[i]) int'(payload[i])==pin_value;}  constraint budget {payload.sum() with (int'(item))<=6;}  function void pre_randomize();payload=new[requested_count];endfunctionendclassmodule tb_arrays;  ArrayShape item;  int accepted=0,rejected=0,samples=0,pinned_elements=0;  function automatic bit oracle(input int n,v);    return (n==1&&v>=0&&v<=3)||(n==2&&v>=0&&v<=3)||(n==3&&v>=0&&v<=2);  endfunction  task automatic check_sample(input int n,v,input bit pinned);    int total;    if(item.payload.size()!=n)$fatal(1,"array size oracle");    total=0;    foreach(item.payload[i])begin      if(item.payload[i]>3)$fatal(1,"array element range oracle");      if(pinned&&int'(item.payload[i])!=v)$fatal(1,"array element oracle");      total+=int'(item.payload[i]);    end    if(total>6)$fatal(1,"array widened sum oracle");  endtask  initial begin    item=new();item.srandom(107);item.pin_enabled=1;    for(int n=0;n<4;n++)for(int v=0;v<4;v++)begin      int result;bit legal;      item.requested_count=n;item.pin_value=v;legal=oracle(n,v);      result=item.randomize();      if(result!=int'(legal))$fatal(1,"array control legal-set oracle");      if(result)begin check_sample(n,v,1);accepted++;pinned_elements+=n;end      else rejected++;    end    item.pin_enabled=0;    for(int k=0;k<64;k++)begin      item.requested_count=k%3+1;      if(!item.randomize())$fatal(1,"array free call failed");      check_sample(item.requested_count,0,0);samples++;    end    if(accepted!=11||rejected!=5||samples!=64||pinned_elements!=21)$fatal(1,"array accounting");    $display("ARRAY CHECK controls=16 accepted=11 rejected=5 pinned_elements=21 sampled=64");    $finish;  endendmodule

^[2]

Tự kiểm tra

Kiểm theo thứ tự shape, domain rồi quan hệ

Viết rõ ai chọn chiều dài, khi nào cấp phát và những field nào được solver chọn. Kiểm shape trước khi dùng index, kiểm domain trước khi cộng, rồi kiểm quan hệ như tổng hoặc khác nhau. Tách giới hạn quan sát được của tool khỏi contract mong muốn của dữ liệu.