VericodeRTL · DV · QUIZTìm bài học, kiến thức…Ctrl K
Học để hiểu. Thực hành để vững.

Bind checker: đúng target, đúng tham số và đúng tín hiệu

Khoảng 60 phútMức 2/3Bản nháp: một số khẳng định chưa đối chiếu spec

Tiên quyết

Sau bài này bạn sẽ

  • Chọn module type hoặc instance làm đích gắn checker
  • Truy tham số và tín hiệu về đúng target
  • Phát hiện lỗi mất carry mà không sửa mã logic DUT

Gắn phép kiểm vào thiết kế có sẵn

Bạn nhận một bộ cộng đã dùng ở nhiều nơi. Bạn muốn kiểm kết quả của từng instance, kể cả bit carry, nhưng giữ phép kiểm trong một file riêng để dễ tái sử dụng.

bind cho phép gắn thêm một instance checker vào target đã chọn khi elaboration. DUT giữ phần logic cộng; checker nhận tín hiệu và kiểm điều kiện đúng ở clock quan sát. Đây không phải một task gọi giữa simulation để gắn checker tùy lúc.

Một bit đầu vào vẫn cần hai bit kết quả

Bắt đầu với bộ cộng có hai đầu vào không dấu, mỗi đầu vào rộng 1 bit. Bảng sau dùng giá trị ngay tại cổng DUT; kết quả viết ở dạng nhị phân 2 bit.

a b Tổng đúng Tổng nếu làm mất carry Có vi phạm?
0 0 00 00 Không
0 1 01 01 Không
1 0 01 01 Không
1 1 10 00 Có

Chỉ kiểm bit thấp sẽ bỏ lọt dòng cuối: bit thấp vẫn bằng 0 trong cả hai kết quả. Checker cần so cả kết quả rộng 2 bit.

Với đầu vào rộng W bit, mỗi toán hạng được mở rộng thêm một bit trước phép cộng. Biểu thức so trong checker là sum == ({1'b0,a} + {1'b0,b}), với sum rộng W+1 bit.

Một câu bind, mỗi target một checker

Ví dụ có bốn instance của bind_adder: hai instance rộng 4 bit và hai instance rộng 1 bit. Câu bind theo module type là:

bind bind_adder bound_sum_checker #(.W(W)) type_check(.clk(clk),.a(a),.b(b),.sum(sum));

Đọc từ trái sang phải: bind_adder là loại target, bound_sum_checker là loại module được gắn, type_check là tên instance checker mới. Mỗi target có một type_check riêng; không phải bốn DUT cùng dùng một checker trung tâm.

Bộ ví dụ cần biên dịch đủ rtl.sv, checker.sv và tb.sv. Chỉ lấy câu bind sẽ chưa có định nghĩa DUT và checker.

Độ rộng đi theo target

Trong #(.W(W)), .W bên trái là parameter của checker; W bên phải lấy theo target. Vì vậy checker trong big_good dùng 4, còn checker trong mini_good dùng 1. Hai instance cùng loại module vẫn có thể nhận cấu hình khác nhau.

Các tên a, b, sum và clk ở kết nối cũng phải trỏ về tín hiệu của target tương ứng. Chẳng hạn big_bad nhận a đã đảo bit so với big_good; checker của nó phải kiểm đầu vào đã đảo tại chính cổng DUT.

Nếu viết #(.W(4)) cho mọi target, checker ở DUT nhỏ có thể bị mở rộng đầu vào ngoài ý muốn. Một số giá trị vẫn so đúng nên chỉ nhìn một lần pass chưa đủ phát hiện cấu hình sai. Hãy kiểm parameter thực và độ rộng cổng trước khi tin kết quả.

Khi chỉ muốn kiểm một instance

Nếu chỉ cần kiểm big_bad, dạng bind theo đường dẫn instance chọn riêng target đó. Nó khác bind theo type, vốn chọn cả bốn instance của bind_adder trong ví dụ.

Tên checker mới nằm trong target đã chọn. Nếu chỉ gắn single_check vào big_bad, không thể mặc định big_good cũng có tên ấy.

Dạng theo instance trong bộ ví dụ hiện chỉ được parser chấp nhận; công cụ mô phỏng đã ghim chưa build được. Kết quả của dạng theo type không thay cho bằng chứng chạy dạng theo instance. Source và diagnostic nằm trong phần bằng chứng cuối bài.

Nếu bật cả hai cách gắn vào cùng target, target đó có thể nhận hai checker. Hai báo cáo cho cùng vi phạm chưa chắc là hai lỗi DUT khác nhau.

Quan sát tín hiệu mà không làm đổi DUT

Checker của bài chỉ có input port, không assign hoặc force tín hiệu DUT. Nó đếm mẫu và vi phạm bằng biến nội bộ. Đó là lựa chọn thiết kế của checker này; từ khóa bind không tự bảo đảm mọi module được gắn đều chỉ đọc.

Bộ cộng là logic tổ hợp. Clock chỉ chọn lúc quan sát, không biến nó thành bộ cộng có thanh ghi. Testbench đổi đầu vào ở cạnh xuống rồi checker lấy mẫu ở cạnh lên, sau khi logic có thời gian ổn định.

Hai nhóm DUT có clock riêng và checker riêng. Việc này chưa minh họa một property chuyển từ clock này sang clock khác.

Bốn lỗi khi gắn checker

  • Chọn một instance trong khi yêu cầu cần kiểm mọi instance của một loại module.
  • Gán cứng độ rộng checker thay vì dùng cấu hình của target.
  • Nối nhầm tín hiệu hoặc clock dù công thức so sánh đúng.
  • Chỉ kiểm bit thấp và bỏ qua carry, hoặc vô tình làm checker drive DUT.

Khi chưa thấy vi phạm, kiểm checker đã được tạo và đã lấy mẫu chưa. Giữ một tình huống DUT sai có chủ đích để biết phép kiểm thực sự hoạt động.

Tự lần theo target, cổng và clock

  1. Với bốn DUT trong ví dụ, bind theo type tạo bao nhiêu checker? Mỗi checker có parameter W nào?
  2. Với DUT rộng 1 bit, vì sao so riêng bit thấp vẫn cho qua phép cộng sai ở dòng cuối bảng?
  3. Nếu big_bad nhận a đã đảo bit nhưng checker nhận a chưa đảo, phép so đang kiểm điều gì?
  4. Nếu chỉ bind vào big_bad, tên single_check có tồn tại trong big_good không?
  5. Nếu sửa DUT cố ý sai thành đúng, số vi phạm dự kiến của bài thực hành cần thay đổi thế nào?

Kiểm tra

Bind đúng target và checker

  1. Ví dụ có bốn instance của bind_adder. Bind theo type trong lab phải tạo type_check ở bao nhiêu target?
  2. mini_good dùng W=1. Parameter W thực của checker được bind vào target này phải là bao nhiêu?
  3. Thay so sánh sum đầy đủ bằng chỉ so W bit thấp có giữ được khả năng phát hiện mất carry không?
  4. Instance-specific example được pyslang chấp nhận nhưng Verilator build từ chối. Kết luận nào đúng cho scope đã kiểm?
  5. Vì sao checker của bài là observer đối với các tín hiệu chức năng DUT?

Bằng chứng kiểm chứng

Expected tính trước chạy: BIND TYPE CHECK targets=4 type_samples4=256 type_samples1=4 good4=0 bad4=120 good1=0 bad1=1 mini_end_ns=40 time_ns=2560.

Module-type binding with target-local widths and ports

Expected tính trước chạy: BIND TYPE CHECK targets=4 type_samples4=256 type_samples1=4 good4=0 bad4=120 good1=0 bad1=1 mini_end_ns=40 time_ns=2560

rtl.sv RTL
`timescale 1ns/1psmodule bind_adder #(parameter int W=4, parameter bit BROKEN=0)  (input bit clk, input bit [W-1:0] a,b, output logic [W:0] sum);  if (BROKEN) assign sum={1'b0,W'(a+b)};  else assign sum={1'b0,a}+{1'b0,b};endmodule
checker.sv testbench
`timescale 1ns/1psmodule bound_sum_checker #(parameter int W=4)  (input bit clk, input bit [W-1:0] a,b, input logic [W:0] sum);  int samples=0,failures=0;  always @(posedge clk)samples++;  A_sum:assert property(@(posedge clk)sum==({1'b0,a}+{1'b0,b}))else failures++;endmodule
tb.sv testbench
`timescale 1ns/1ps// Expected before execution: W4 all256 pairs,120 lose carry; W1 all4 pairs,1 loses carry.// Four type-bound checkers only. Checker W values must be4/4/1/1.// Bad-instance inputs are complemented to exercise target-local port resolution.// Instance-specific forms remain separate failed probes.bind bind_adder bound_sum_checker #(.W(W)) type_check(.clk(clk),.a(a),.b(b),.sum(sum));module tb_bind;  bit clk4=0,clk1=0;  bit [3:0] a4=0,b4=0;  bit a1=0,b1=0;  wire [4:0] good4,bad4;  wire [1:0] good1,bad1;  time mini_end=0;  bind_adder #(.W(4)) big_good(.clk(clk4),.a(a4),.b(b4),.sum(good4));  bind_adder #(.W(4),.BROKEN(1)) big_bad(.clk(clk4),.a(~a4),.b(b4),.sum(bad4));  bind_adder #(.W(1)) mini_good(.clk(clk1),.a(a1),.b(b1),.sum(good1));  bind_adder #(.W(1),.BROKEN(1)) mini_bad(.clk(clk1),.a(~a1),.b(b1),.sum(bad1));  always #5 clk4=~clk4;  initial repeat(8) #5 clk1=~clk1;  initial begin    fork      begin        for(int i=0;i<256;i++)begin          if(i>0)@(negedge clk4);          a4=i[7:4];b4=i[3:0];        end        @(negedge clk4);      end      begin        for(int i=0;i<4;i++)begin          if(i>0)@(negedge clk1);          a1=i[1];b1=i[0];        end        @(negedge clk1);mini_end=$time;      end    join    if($time!=2560||mini_end!=40||       big_good.type_check.W!=4||big_bad.type_check.W!=4||       mini_good.type_check.W!=1||mini_bad.type_check.W!=1||       big_good.type_check.samples!=256||big_good.type_check.failures!=0||       big_bad.type_check.samples!=256||big_bad.type_check.failures!=120||       mini_good.type_check.samples!=4||mini_good.type_check.failures!=0||       mini_bad.type_check.samples!=4||mini_bad.type_check.failures!=1)      $fatal(1,"bind target parameter and carry oracle");    $display("BIND TYPE CHECK targets=4 type_samples4=256 type_samples1=4 good4=0 bad4=120 good1=0 bad1=1 mini_end_ns=40 time_ns=%0d",$time);    $finish;  endendmodule

Đã kiểm chứng thế nào

  • Phân tích và elaborate theo LRM (pyslang 12.1.0)
  • Mô phỏng, exit 0 và output khớp kỳ vọng tính tay (Verilator 5.050, 2-state)

Output phải khớp: BIND TYPE CHECK targets=4 type_samples4=256 type_samples1=4 good4=0 bad4=120 good1=0 bad1=1 mini_end_ns=40 time_ns=2560

Verilator 2 state, module-type bind only, W=1/W=4 targets and finite exhaustive domains. Four target-local checker widths are guarded explicitly.

Independent checker clocks are not one multiclocked property. Instance-path/list probes remain build failures; no simulation claim for those forms.

Các kiểm tra chạy lúc xây dựng nội dung (2026-11-06), không chạy trong trình duyệt. Kỳ vọng được tính tay trước khi chạy.

Main type-bind quét toàn bộ 256 cặp đầu vào ở W=4 và 4 cặp ở W=1. DUT bad giữ W bit thấp rồi mở rộng 0, cố ý làm mất carry. Với W=4, số cặp overflow là 1+2+...+15=120; với W=1 chỉ có 1+1. Đảo a chỉ hoán vị miền đầu vào nên không đổi số trường hợp này.

Target W thực của checker Số mẫu Số vi phạm dự kiến
big_good 4 256 0
big_bad 4 256 120
mini_good 1 4 0
mini_bad 1 4 1

Guard kiểm trực tiếp cả bốn parameter, sample/failure counter và thời gian thật. Nhóm nhỏ dừng ở 40 ns, toàn bộ bài chạy tới 2560 ns. Tắt checker làm counter của DUT bad sai kỳ vọng và oracle phải từ chối; không lấy zero failure làm bằng chứng checker hoạt động.

Bốn mutant parse/build được rồi bị bắt ở runtime: ép mọi checker về W=4, đảo predicate bằng thành khác, chỉ so bit thấp, hoặc sửa DUT bad thành đúng nhưng giữ kỳ vọng cũ của lab. Mutant cuối kiểm tính nhất quán của lab; không nói rằng sửa lỗi DUT là lỗi sản phẩm.

Instance-specific bind source: parsed only

Pyslang accepts the instance-specific source. Original five-checker/count oracle is retained; no executable simulation PASS is claimed.

tb.sv testbench
`timescale 1ns/1ps// Expected before execution: W4 all256 pairs,120 lose carry; W1 all4 pairs,1 loses carry.// Four type-bound checkers; an additional instance-bound checker observes big_bad only.module bind_adder #(parameter int W=4, parameter bit BROKEN=0)  (input bit clk, input bit [W-1:0] a,b, output logic [W:0] sum);  if (BROKEN) assign sum={1'b0,W'(a+b)};  else assign sum={1'b0,a}+{1'b0,b};endmodulemodule bound_sum_checker #(parameter int W=4)  (input bit clk, input bit [W-1:0] a,b, input logic [W:0] sum);  int samples=0,failures=0;  always @(posedge clk)samples++;  A_sum:assert property(@(posedge clk)sum==({1'b0,a}+{1'b0,b}))else failures++;endmodulebind bind_adder bound_sum_checker #(.W(W)) type_check(.clk(clk),.a(a),.b(b),.sum(sum));bind tb_bind.big_bad bound_sum_checker #(.W(4)) single_check(.clk(clk),.a(a),.b(b),.sum(sum));module tb_bind;  bit clk4=0,clk1=0;  bit [3:0] a4=0,b4=0;  bit a1=0,b1=0;  wire [4:0] good4,bad4;  wire [1:0] good1,bad1;  time mini_end=0;  bind_adder #(.W(4)) big_good(.clk(clk4),.a(a4),.b(b4),.sum(good4));  bind_adder #(.W(4),.BROKEN(1)) big_bad(.clk(clk4),.a(a4),.b(b4),.sum(bad4));  bind_adder #(.W(1)) mini_good(.clk(clk1),.a(a1),.b(b1),.sum(good1));  bind_adder #(.W(1),.BROKEN(1)) mini_bad(.clk(clk1),.a(a1),.b(b1),.sum(bad1));  always #5 clk4=~clk4;  initial repeat(8) #5 clk1=~clk1;  initial begin    fork      begin        for(int i=0;i<256;i++)begin          if(i>0)@(negedge clk4);          a4=i[7:4];b4=i[3:0];        end        @(negedge clk4);      end      begin        for(int i=0;i<4;i++)begin          if(i>0)@(negedge clk1);          a1=i[1];b1=i[0];        end        @(negedge clk1);mini_end=$time;      end    join    if($time!=2560||mini_end!=40||       big_good.type_check.samples!=256||big_good.type_check.failures!=0||       big_bad.type_check.samples!=256||big_bad.type_check.failures!=120||       mini_good.type_check.samples!=4||mini_good.type_check.failures!=0||       mini_bad.type_check.samples!=4||mini_bad.type_check.failures!=1||       big_bad.single_check.samples!=256||big_bad.single_check.failures!=120)      $fatal(1,"bind target parameter and carry oracle");    $display("BIND CHECK targets=4 type_samples4=256 type_samples1=4 good4=0 bad4=120 good1=0 bad1=1 single_bad4=120 mini_end_ns=40 time_ns=%0d",$time);    $finish;  endendmodule

Đã kiểm chứng thế nào

  • Phân tích và elaborate theo LRM (pyslang 12.1.0)

Verilator 5.050 rejects the instance-path form at the dot; the alternative instance-list probe is explicitly unsupported.

Source includes both type and instance bind for parser/elaboration study. Parsed does not replace simulation; original counter expectations are not relaxed.

Các kiểm tra chạy lúc xây dựng nội dung (2026-11-06), không chạy trong trình duyệt. Kỳ vọng được tính tay trước khi chạy.

Source instance-specific giữ nguyên kỳ vọng của cả năm checker. Pyslang chấp nhận source; probe đọc nhầm single_check ở target không được chọn bị từ chối khi giải hierarchy. Verilator 5.050 từ chối đường dẫn instance tại dấu chấm và báo unsupported với dạng instance-list. Không xóa assertion hay hạ kỳ vọng để gọi source này đã simulated PASS.

Giới hạn: type-bind chỉ chạy trên mô hình 2-state và hai độ rộng W=1/W=4; vét cạn hữu hạn không chứng minh mọi cấu hình. Hai clock của các checker độc lập không phải một multiclocked property. Nguồn training có mô tả DFF chưa rõ timing/reset nên không sao chép property demo; checker cộng và phép kiểm trong bài được viết riêng. IEEE vẫn chờ đối chiếu.

[2] [3]

Bài liên quan

Nguồn và mức độ đối chiếu

  1. IEEE 1800-2023 SystemVerilog LRM, Bind directives, elaboration and scope resolution — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. Binding with Assertions — bản chụp resources.zip, Binding with Assertions; Why Bind Assertions?; bind example; Selecting the Bind Target; Where to Place the Bind Statement. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. Thí nghiệm nguyên bản B8.bind, Module-type binding across W1/W4 targets, four runtime mutants and retained instance-binding failures. Trích dẫn; nguồn đã đọc toàn văn.
  4. IEEE 1800-2023 SystemVerilog LRM, Bind directives and target scope — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  5. IEEE 1800-2023 SystemVerilog LRM, Instance-specific bind syntax/scope — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).