Case decode: full coverage không phải lời hứa one-hot

Một bảng decode cần cả miền input hợp lệ

Một decoder chỉ được dùng với request one-hot khác với decoder phải xử lý mọi tổ hợp request. Nếu bỏ qua điều kiện ấy, đổi priority logic sang OR các nhánh có thể cho kết quả khác ngay trên input 11. Bài kiểm cả 16 selector 4-state và một điều kiện one-hot-or-zero rất nhỏ có thể liệt kê tay.

Plain case so khớp đủ bốn trạng thái

Plain case của ví dụ liệt kê 00/01/10/11; mọi selector có X/Z rơi vào default 3. Default này là giá trị chức năng của mô hình, không tự báo lỗi input. Một default khác có thể phù hợp yêu cầu khác, nhưng phải được nêu rõ. Không biến X/Z trong case item thành wildcard nếu đang dùng plain case. ^[1]

Casez và casex có thể làm mất dấu unknown

Casez bỏ qua Z/dấu hỏi; casex còn bỏ qua X, kể cả trong selector. Với item 1?, bit thấp chứa X cũng có thể được che bởi dấu hỏi của item. Vì vậy câu “casez luôn để X rơi về default” không đúng cho mọi pattern. TB tính expected từ nhãn 0/1/X/Z của từng bit rồi so output, tránh lấy chính output decoder làm oracle.

One-hot là tiền điều kiện cần có bằng chứng

Trong 00/01/10, priority decode và parallel OR của ví dụ cùng cho 0/1/2. Nhưng 11 cho priority 2 và parallel 3. Nếu contract yêu cầu ưu tiên bit cao, OR song song đã sai; nếu contract chỉ cho phép one-hot, vẫn cần kiểm producer giữ điều kiện đó. Đừng tự gắn assumption rồi xóa input vi phạm khỏi verification mà chưa có yêu cầu.

Full, parallel và unique không tự tạo phần cứng đúng

“Đã gán đủ mọi đường” và “các nhánh loại trừ nhau” là hai thuộc tính khác nhau. Default giúp định nghĩa đường không match, nhưng không chứng minh one-hot. Các keyword/pragmas như unique, full_case hay parallel_case có thể thay đổi kiểm tra hoặc assumption tối ưu tùy flow; bài không thử chúng và không dùng như cách bỏ warning. Nếu sử dụng, phải đối chiếu ngôn ngữ/tool và kiểm cả input vi phạm. ^[2]

16 selector và một phản ví dụ 11

Tính trước chạy: ba selector one-hot-or-zero cùng kết quả; req 11 priority 2/parallel 3. Exact default 3 cho các mã chứa X/Z; wildcard được kiểm cho mọi cặp bốn trạng thái.

`timescale 1ns/1psmodule decoder(input wire [1:0] req, output reg [1:0] exact_value,z_value,x_value, output wire [1:0] parallel_value);  always @* begin    case(req)      2'b00:exact_value=0;      2'b01:exact_value=1;      2'b10,2'b11:exact_value=2;      default:exact_value=3;    endcase    casez(req)      2'b1?:z_value=2;      2'b01:z_value=1;      default:z_value=0;    endcase    casex(req)      2'b1?:x_value=2;      2'b01:x_value=1;      default:x_value=0;    endcase  end  assign parallel_value=(req[1]?2'd2:2'd0)|(req[0]?2'd1:2'd0);endmodule

`timescale 1ns/1psmodule tb_case;  reg [1:0] req;  wire [1:0] exact_value,z_value,x_value,parallel_value;  integer n,hi,lo,e,z,x,onehot_cases=0;  decoder dut(.*);  function automatic reg state4(input integer n);    case(n) 0:state4=0; 1:state4=1; 2:state4=1'bx; default:state4=1'bz; endcase  endfunction  initial begin    for(n=0;n<16;n=n+1) begin      hi=n/4;lo=n%4;req={state4(hi),state4(lo)};      case(n) 0:e=0;1:e=1;4,5:e=2;default:e=3;endcase      z=(hi==1||hi==3)?2:((hi==0&&(lo==1||lo==3))?1:0);      x=(hi!=0)?2:((lo!=0)?1:0);      #1;      if(exact_value!==e[1:0]||z_value!==z[1:0]||x_value!==x[1:0]) $fatal(1,"case mismatch req=%b",req);      if(n==0||n==1||n==4) begin        if(parallel_value!==z_value) $fatal(1,"onehot equivalence mismatch");        onehot_cases=onehot_cases+1;      end      if(n==5) begin        if(z_value!==2||parallel_value!==3) $fatal(1,"overlap mismatch");        $display("CASE OVERLAP req=11 priority=%0d parallel=%0d",z_value,parallel_value);      end    end    if(onehot_cases!=3) $fatal(1,"missing onehot cases");    $display("CASE CHECK selectors=16 onehot_or_zero=%0d",onehot_cases);    $finish;  endendmodule

CASEX là warning dự kiến của module cố ý minh họa rủi ro. Generic synthesis kiểm không FF/latch; không dùng nó để chứng minh hardware có thể phát hiện điện áp unknown. ^[3]

Tự kiểm tra

Định nghĩa domain trước khi tối ưu decoder

Viết rõ mã hợp lệ, điều kiện chồng lấn, ưu tiên và hành vi invalid. Kiểm chúng độc lập trước khi dùng kết luận full/parallel. Bài giữ draft/LRM needs-spec-check, không claim mọi wildcard hoặc pragma synthesis.