Implication, if-else và foreach: ràng buộc quan hệ thay vì chạy lệnh gán

Điều kiện không phải một timeline thực thi

Choice có enabled, value và flag được solver chọn cùng nhau. If/implication trong constraint mô tả quan hệ giữa các giá trị, không phải chạy enabled trước rồi gán value sau. Đừng mang cách nghĩ về procedural if hoặc SVA temporal implication vào bài toán này.

If-else đặt yêu cầu cho cả hai nhánh

Enabled 0 yêu cầu value 0..3; enabled 1 yêu cầu value 4..7. Cả hai là một phần hợp đồng. Nếu bỏ else, phần disabled không tự mang điều kiện ngược; các constraint khác vẫn áp dụng theo cách riêng.

^[1]

Value 7 yêu cầu flag 1, không phải hai điều kiện tương đương

Rule (value==7)->(flag==1) loại value 7/flag 0. Khi value khác 7, riêng rule này không cấm flag 1. Main pin cả enabled 0/value 0/flag 1 và enabled 1/value 4/flag 1 như những ca hợp lệ để bắt lỗi đảo chiều hoặc thêm equivalence ngoài ý muốn.

Foreach đặt quan hệ cho từng phần tử array

Lanes có ba element 4 bit; mỗi lanes[i] bằng value+i trong expression đã widen sang int. Đây là ba ràng buộc được xét cùng các rule khác, không phải một vòng procedural sửa array sau solver. Với value 7, các element phải 7/8/9, vẫn nằm trong 4 bit.

Tính số nghiệm của ba field điều khiển

Enabled 0 có bốn value và hai flag, được 8 cặp value/flag. Enabled 1 có value 4/5/6 với hai flag, được 6; value 7 chỉ flag 1, thêm 1. Tổng 15 cấu hình trong 32 pin; còn 17 vô nghiệm. Mỗi cấu hình hợp lệ quy định cả ba lanes, không nhân thêm số nghiệm tùy ý cho array.

Kiểm trạng thái thành công trước khi đọc lanes

Main quét hai enabled, tám value và hai flag. Return phải khớp oracle; chỉ 15 call thành công mới được kiểm các field và 45 element. Khi fail, TB không giả định array mới được sinh hoặc tiếp tục dùng dữ liệu như stimulus hợp lệ.

Đảo implication làm thay tập nghiệm

Mutation (flag==1)->(value==7) không tương đương rule gốc. Checker pinning bắt symptom conditional/implication legal set; không chữa bằng đổi expected theo những mẫu solver tình cờ trả về. Foreach cũng phải kiểm từng index, không chỉ tổng có thể triệt tiêu lỗi.

32 pin và 45 element được kiểm

Expected tính trước chạy: 15 accept/17 reject,45 lane check,giá trị lớn nhất 9. UNSATCONSTR của các pin vô nghiệm là diagnostic dự kiến; process chỉ exit 0 khi tất cả return/output/accounting đúng. Không tắt warning hoặc gọi các call return 0 là randomization success.

`timescale 1ns/1psclass Choice;  rand bit enabled,flag;  rand bit[2:0] value;  rand bit[3:0] lanes[3];  constraint branches {    if(enabled)value inside {[4:7]};else value inside {[0:3]};    (value==7)->(flag==1);    foreach(lanes[i])int'(lanes[i])==int'(value)+i;  }endclassmodule tb_implication;  Choice choice;  int en,v,f,result,accepted=0,rejected=0,lane_checks=0,max_lane=0;  bit legal;  initial begin    choice=new();choice.srandom(71);    for(en=0;en<2;en++)for(v=0;v<8;v++)for(f=0;f<2;f++)begin      legal=((en==0&&v<4)||(en==1&&v>=4))&&(v!=7||f==1);      result=choice.randomize() with {enabled==local::en;value==local::v;flag==local::f;};      if(result!=int'(legal))$fatal(1,"conditional/implication legal set en=%0d v=%0d f=%0d",en,v,f);      if(result)begin        if(int'(choice.enabled)!=en||int'(choice.value)!=v||int'(choice.flag)!=f)$fatal(1,"conditional inline pins ignored");        foreach(choice.lanes[i])begin          if(int'(choice.lanes[i])!=v+i)$fatal(1,"foreach constraint lane=%0d",i);          if(int'(choice.lanes[i])>max_lane)max_lane=int'(choice.lanes[i]);lane_checks++;        end        accepted++;      end else rejected++;    end    if(accepted!=15||rejected!=17||lane_checks!=45||max_lane!=9)$fatal(1,"conditional accounting");    $display("IMPLICATION CHECK pinned=32 accepted=15 rejected=17 lane_checks=45 max_lane=9");    $finish;  endendmodule

^[2]

Tự kiểm tra

Viết bảng hợp lệ trước rồi mới chọn cú pháp

Xác định antecedent, consequent và những gì vẫn tự do theo riêng rule đó. Với if-else hãy kiểm cả hai phía; với foreach hãy kiểm shape và width từng element. Dùng pinning cho miền nhỏ và seed cho tái hiện, không suy phân phối từ 15 cấu hình đúng.