Unique constraint: khác nhau trong một mẫu, không phải qua mọi lần gọi

Ba nhãn khác nhau vẫn có thể lặp lại ở lần sau

Một object chứa ba field nhãn 2 bit: first, second và third. Trong một mẫu, ba nhãn phải đôi một khác nhau. Bốn giá trị có sẵn là 0, 1, 2 và 3; không bắt buộc nhãn nào đứng trước, và luôn có một giá trị không được dùng trong mẫu đó.

unique {first,second,third} mô tả yêu cầu giữa các phần tử trong cùng một lần giải. Nó không lưu lịch sử các bộ đã xuất hiện. Nếu một test cần cấm lặp nguyên bộ qua nhiều call, phải thiết kế và kiểm một cơ chế riêng, thay vì suy điều đó từ từ khóa unique.

Đối chiếu unique với một oracle đôi một

Với ba vị trí, oracle trong testbench kiểm ba cặp: phần tử 0 khác 1, 0 khác 2 và 1 khác 2. Thiếu một cặp có thể cho phép hai vị trí trùng nhau mà một số mẫu khác vẫn trông đúng.

Oracle là hàm procedural riêng, không tái dùng unique constraint để tự chấm nó. Mỗi call thành công còn phải giữ đúng toàn bộ pin được yêu cầu; chỉ nhìn số phần tử hoặc một tổng cộng không đủ phát hiện việc solver bỏ qua một pin.

^[1]

24 bộ có thứ tự trong tổng 64 bộ

Vị trí đầu có 4 lựa chọn, vị trí thứ hai còn 3, vị trí thứ ba còn 2. Có 4*3*2 = 24 bộ hợp lệ. Đổi thứ tự hai nhãn tạo một bộ khác, nên không dùng số tổ hợp chọn 3 trong 4 để đếm ba field có vai trò riêng.

Tổng miền kiểu dữ liệu là 4*4*4 = 64. Main pin đủ 64 bộ: 24 return thành công, 40 return thất bại. Không cần đợi một vòng random dài để tìm được lỗi chấp nhận bộ trùng; kiểm vét cạn đã yêu cầu đúng kết quả cho từng bộ nhỏ.

Năm nhãn 2 bit không thể đều khác nhau

Một class khác có năm field nhưng từng field vẫn chỉ có bốn giá trị. Theo nguyên lý pigeonhole, không có nghiệm nào làm năm vị trí đôi một khác nhau. Thay seed hoặc thử lại nhiều lần không làm miền kiểu dữ liệu lớn hơn.

Bài kiểm một call của class này phải return 0. Nó không dùng những giá trị còn nằm trong các field như một mẫu hợp lệ. Khi định dạng dữ liệu thực cần thêm phần tử unique, phải xem lại độ rộng field hoặc bớt yêu cầu; không bỏ kiểm return code.

64 mẫu hợp lệ buộc phải lặp nguyên bộ

Main tiếp tục tạo 64 mẫu từ class ba nhãn, kiểm từng mẫu với oracle và mã hóa bộ thành một key 0 đến 63. Vì chỉ có 24 bộ hợp lệ, 64 call thành công buộc có ít nhất một key đã xuất hiện.

Đây là một kết luận đếm chắc chắn, không phải kỳ vọng dựa trên xác suất của một seed. Bài chỉ kiểm có lặp, không quy định bộ nào lặp hoặc tần suất cụ thể. Randc của một biến với domain riêng và unique của các phần tử trong một call là hai contract khác nhau.

Return 0 không cung cấp một stimulus mới hợp lệ

Ở nhánh thất bại của vét cạn, main kiểm ba scalar vẫn giữ giá trị đã gán, đồng thời không tiêu thụ chúng làm stimulus mới. Với call thành công, main kiểm lại từng cặp bằng oracle độc lập, thay vì coi return 1 là đủ để bỏ mọi kiểm tra.

Hai probe array được tách riêng khỏi main. Probe thứ nhất gán array thành ba giá trị 2 rồi yêu cầu bộ trùng; trên Verilator 5.050 đã ghi, call return 0 nhưng array đổi thành 2/1/3. Probe thứ hai tạo object mới trước khi sinh tự do; tool return 1 với một mẫu 1/2/1, vi phạm yêu cầu unique. Cả hai probe dừng bằng fatal, được giữ làm bằng chứng giới hạn của tool, không tính vào các claim PASS của main.

Không suy scalar PASS thành hỗ trợ mọi array

Main kiểm danh sách ba scalar 2 bit. Nguồn đào tạo cũng mô tả cú pháp unique trên array, nhưng bằng chứng thực nghiệm ở phiên bản tool này không cho phép bài khẳng định cú pháp đó đã chạy đúng. Bỏ assertion array để cho output xanh sẽ che khác biệt quan trọng, nên các probe vẫn giữ nguyên oracle và thất bại quan sát được.

Phần quy tắc ngôn ngữ còn needs-spec-check. Bài không nâng hiện tượng của một tool thành rule chuẩn và không suy mọi tool sẽ có cùng lỗi. Khi kiểm DUT, hãy dùng cả return code lẫn kiểm tính hợp lệ độc lập của stimulus; dừng test nếu generator cho dữ liệu vi phạm hợp đồng.

64 pin và 64 mẫu được kiểm độc lập

Expected tính trước chạy: 24 accept/40 reject, 64 mẫu thành công đều unique, có ít nhất một bộ lặp; class năm vị trí phải thất bại. Warning UNSATCONSTR của các pin không có nghiệm được giữ. Main kiểm scalar; hai capability probe về failure atomicity và tính unique của array thất bại, được báo riêng trong giới hạn của ví dụ.

`timescale 1ns/1ps// Expected before execution: 4*3*2=24 legal ordered triples, 40 rejected.class UniqueTriple;  rand bit[1:0] first,second,third;  constraint distinct_tags {unique {first,second,third};}endclassclass ImpossibleFive;  rand bit[1:0] first,second,third,fourth,fifth;  constraint distinct_tags {unique {first,second,third,fourth,fifth};}endclassmodule tb_unique;  UniqueTriple item;ImpossibleFive too_many;  bit seen[64];bit repeated=0;  int accepted=0,rejected=0,samples=0;  function automatic bit oracle(input int a,b,c);    return a!=b&&a!=c&&b!=c;  endfunction  initial begin    item=new();too_many=new();item.srandom(89);    for(int a=0;a<4;a++)for(int b=0;b<4;b++)for(int c=0;c<4;c++)begin      int result;bit legal;      legal=oracle(a,b,c);item.first=2;item.second=2;item.third=2;      result=item.randomize() with {first==local::a;second==local::b;third==local::c;};      if(result!=int'(legal))$fatal(1,"unique legal-set oracle");      if(result)begin        if(item.first!=a||item.second!=b||item.third!=c)$fatal(1,"unique pins ignored");accepted++;      end else begin        if(item.first!=2||item.second!=2||item.third!=2)$fatal(1,"failed scalar unique call changed fields");rejected++;      end    end    repeat(64)begin      int key;      if(!item.randomize()||!oracle(int'(item.first),int'(item.second),int'(item.third)))$fatal(1,"unique sample failed");      key=16*int'(item.first)+4*int'(item.second)+int'(item.third);      if(seen[key])repeated=1;seen[key]=1;samples++;    end    if(!repeated)$fatal(1,"64 samples cannot fit 24 triples without repeat");    too_many.first=1;too_many.second=1;too_many.third=1;too_many.fourth=1;too_many.fifth=1;    if(too_many.randomize()!=0)$fatal(1,"pigeonhole failure contract");    if(too_many.first!=1||too_many.second!=1||too_many.third!=1||too_many.fourth!=1||too_many.fifth!=1)$fatal(1,"failed scalar pigeonhole call changed fields");    if(accepted!=24||rejected!=40||samples!=64)$fatal(1,"accounting");    $display("UNIQUE CHECK pinned=64 accepted=24 rejected=40 sampled=64 repeated=1 impossible=1");    $finish;  endendmodule

^[2]

Tự kiểm tra

Đếm miền, kiểm cả cặp và chặn dữ liệu thất bại

Xác định có bao nhiêu vị trí và bao nhiêu giá trị trước khi randomize. Phân biệt permutation theo index với tập không có thứ tự. Với miền nhỏ, vét cạn và oracle riêng cho bằng chứng mạnh hơn việc nhìn vài dòng output; với mọi miền, chỉ dùng stimulus của call được xác nhận thành công.