Simulator, waveform, lint và synthesis: mỗi công cụ trả lời một câu hỏi

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

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

  • Chọn công cụ theo dấu hiệu lỗi cần tìm
  • Đọc một waveform có kết quả đúng và mất carry
  • Phân biệt chạy được, kiểm chức năng đúng và đạt timing

Chạy qua công cụ chưa nói hết thiết kế đúng đến đâu

Một khối có thể không có cảnh báo lint, synthesis thành công, nhưng vẫn cộng sai. Các công cụ kiểm những tính chất khác nhau; cần ghép bằng chứng theo yêu cầu cần xác nhận.

Mục tiêu bài này là biết nên nhìn vào đâu. Bạn chưa cần thuộc các tùy chọn dòng lệnh hay toàn bộ cú pháp HDL.

Chọn câu hỏi trước khi chọn công cụ

Công cụ/hoạt động Câu hỏi điển hình Kết quả cần đọc
Parser/elaborator Source có được chấp nhận và các tên, cấu hình được giải thế nào? Diagnostic, hierarchy và cấu hình được dựng
Lint Có mẫu viết đáng ngờ theo bộ luật đang bật không? Cảnh báo cùng vị trí và ngữ cảnh
Simulator + testbench Với các tình huống đã tạo, đầu ra có đáp ứng điều kiện kiểm không? Kết quả so sánh, thông báo lỗi và diễn biến tín hiệu
Waveform viewer Tín hiệu thay đổi thế nào theo thời gian mô phỏng? Các lane tín hiệu và mốc cần đối chiếu
Synthesis Phần RTL được hỗ trợ biến thành cấu trúc nào? Netlist, cell/tài nguyên và báo cáo liên quan
STA Timing có đạt theo mô hình và constraint không? Slack, đường cần kiểm và constraint liên quan

Waveform viewer giúp nhìn dữ liệu mô phỏng, không tự biết “đúng” nghĩa là gì. Điều kiện mong đợi vẫn phải đến từ đặc tả và cách kiểm.

Hai đầu ra cho cùng một phép cộng

Ví dụ nhận hai số không dấu từ 0 tới 3. Với các bit chỉ nhận 0/1, hai bit giữ được bốn giá trị ấy; tổng tới 6 cần thêm bit cao. Đầu ra good giữ đủ tổng; đầu ra broken cố ý chỉ giữ hai bit thấp rồi mở rộng thêm bit 0.

a b Tổng cần có good broken
0 3 3 3 3
1 3 4 4 0
2 2 4 4 0
3 3 6 6 2

Cả hai cách viết đều biểu diễn được logic tổ hợp. Lint không biết yêu cầu nghiệp vụ là giữ tổng đầy đủ nếu điều đó chưa được diễn đạt thành luật kiểm phù hợp. Synthesis cũng có thể tạo phần cứng cho cả hàm đúng lẫn hàm sai so với yêu cầu ấy.

Ở đây testbench tính tổng tham chiếu từ các số nguyên tạo đầu vào, rồi đối chiếu cả miền 16 cặp. Bản mất carry sai tại 6 cặp có tổng từ 4 trở lên.

Đọc carry trên waveform

Carry đúng và carry bị bỏ mất trên 16 cặp đầu vào

Trích từ mô phỏng Verilator (VCD) của ex.a0.tools, không vẽ tay
0123456789101112131415clkcarry_goodcarry_bad
  • Cột 7: a=1, b=3: tổng đúng là 4, cần carry
  • Cột 15: a=3, b=3: tổng đúng là 6; bản mất carry chỉ giữ 2

Mỗi cột là một mẫu; chỉ số cột bắt đầu từ 0. Testbench đi qua a tăng từ 0 tới 3, với b chạy từ 0 tới 3 cho mỗi giá trị a. Cột 7 vì thế ứng với a bằng 1 và b bằng 3.

Ở cột ấy, carry_good lên 1 còn carry_bad vẫn bằng 0. Đây là dấu hiệu phần bit cao của tổng đã bị bỏ mất. Muốn kiểm trọn phép cộng còn phải đối chiếu các bit còn lại; chỉ nhìn carry chưa đủ.

Clock trong hình là mốc lấy mẫu của testbench. DUT ở ví dụ không có cổng clock hay thanh ghi; việc thêm mốc quan sát không biến bộ cộng tổ hợp thành bộ cộng có độ trễ một chu kỳ.

Từ source tới một lượt mô phỏng có ý nghĩa

Trước hết công cụ đọc source và dựng mô hình theo module top, file và parameter được chọn. Sau đó testbench tạo đầu vào, mô hình tính đầu ra và các phép kiểm đối chiếu kết quả.

Nếu chọn sai top hoặc thiếu file, chưa thể dùng một cửa sổ waveform trống để kết luận thiết kế đúng. Nếu có tín hiệu nhưng thiếu phép so, cũng chưa xác nhận yêu cầu đã được đáp ứng.

Giữ ba thứ cạnh nhau khi debug: tình huống đầu vào, thời điểm cần kiểm và kết quả mong đợi. Đọc lỗi đầu tiên có ý nghĩa trước khi lần theo các lỗi phát sinh sau nó.

Đừng lấy một báo cáo thay cho mọi báo cáo

  • Không có cảnh báo lint chưa có nghĩa đã đúng đặc tả.
  • Có netlist chưa có nghĩa đã đạt timing trên một công nghệ cụ thể.
  • Waveform trông hợp lý chưa có nghĩa đã thử đủ tình huống biên.
  • Một lượt kiểm đúng không xác nhận một phiên bản source hoặc cấu hình khác.

Với ví dụ nhỏ, có thể vét cạn mọi đầu vào đã nêu. Với hệ thống lớn, cần kế hoạch kiểm, mô hình tham chiếu, coverage và các phương pháp bổ sung; chỉ tăng số lần chạy chưa chắc lấp đúng chỗ thiếu.

Lần từ triệu chứng tới bằng chứng

  1. Nếu chỉ thử các cặp có tổng không vượt 3, lỗi nào trong ví dụ sẽ bị bỏ qua?
  2. Bạn thấy lint không có cảnh báo nhưng 1 cộng 3 ra 0. Bước tiếp theo nên là gì?
  3. Một waveform cho thấy đầu ra đúng tại vài mẫu. Nó đã thay cho báo cáo STA chưa?
  4. Tại cột 15, hai đầu vào bằng bao nhiêu và vì sao cần giữ bit cao?

Kiểm tra

Tự kiểm tra: Dùng đúng công cụ

  1. Lint sạch có tự bảo đảm bộ cộng trả đúng tổng yêu cầu không?
  2. Tại cột 7, a bằng 1 và b bằng 3. Carry của tổng đúng phải bằng bao nhiêu?
  3. Yosys tổng hợp generic được ví dụ. Kết luận nào phù hợp?
  4. Waveform viewer tự biết một đầu ra đang sai đặc tả không?

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

Expected tính trước chạy: A0 TOOL CHECK vectors=16 correct=16 lost_carry=6 mask=60544 time_ns=170. Các vector mất carry có chỉ số 7, 10, 11, 13, 14, 15; cộng các bit tương ứng được mask 60544.

Bộ cộng đúng và mất carry: lint, simulation và synthesis trả lời khác nhau

Expected trước chạy: 16 cặp đầu vào 0–3; bản đúng khớp đủ 16, bản mất carry sai ở 6 cặp, mask=60544. Kết thúc 170 ns sau 17 cạnh lấy mẫu cho 16 cột VCD.

adder_pair.sv RTL
`timescale 1ns/1psmodule adder_pair(  input logic [1:0] a,b,  output logic [2:0] good,broken);  wire [1:0] low=2'(a+b);  assign good={1'b0,a}+{1'b0,b};  assign broken={1'b0,low};endmodule
tb.sv testbench
`timescale 1ns/1ps// Expected BEFORE execution: 16 input pairs, all good sums match.// Lost carry at vector indexes 7,10,11,13,14,15: 6 cases, mask 60544.// 17th sampling edge bounds the last of 16 VCD columns; finish at 170 ns.module tb_a0_tools;  bit clk=0;  logic [1:0] a=0,b=0;  wire [2:0] good,broken;  wire carry_good=good[2],carry_bad=broken[2];  logic [2:0] reference_sum;  int checks=0,bugs=0,bad_mask=0;  adder_pair dut(.a(a),.b(b),.good(good),.broken(broken));  always #5 clk=~clk;  initial begin    $dumpfile("trace.vcd");$dumpvars(0,tb_a0_tools);    for(int i=0;i<16;i++)begin      if(i>0)@(negedge clk);      a=i[3:2];b=i[1:0];      @(posedge clk);#1;      reference_sum=3'((i/4)+(i%4));checks++;      if(good!==reference_sum)$fatal(1,"good adder mismatch at vector %0d",i);      if(broken!==reference_sum)begin bugs++;bad_mask|=1<<i;end    end    @(negedge clk);@(posedge clk);@(negedge clk);    if(checks!=16||bugs!=6||bad_mask!=60544||$time!=170)      $fatal(1,"A0 tool experiment contract checks=%0d bugs=%0d mask=%0d",checks,bugs,bad_mask);    $display("A0 TOOL CHECK vectors=16 correct=16 lost_carry=6 mask=60544 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)
  • Lint -Wall (Verilator 5.050)
  • Mô phỏng, exit 0 và output khớp kỳ vọng tính tay (Verilator 5.050, 2-state)
  • Waveform trích từ VCD của lần mô phỏng
  • Tổng hợp, số cell khớp kỳ vọng (Yosys 0.70)

Output phải khớp: A0 TOOL CHECK vectors=16 correct=16 lost_carry=6 mask=60544 time_ns=170

Kỳ vọng sau tổng hợp: adder_pair: $_*DFF* = 0adder_pair: $_*LATCH* = 0

Verilator 5.050 is two-state. The finite exhaustive domain is the 16 known unsigned input pairs; no X/Z behavior claim.

Clock belongs to the testbench only. The DUT is combinational; VCD columns sample stable values between rising edges, not physical delay or timing sign-off.

Both output functions pass RTL lint and generic Yosys synthesis. Only the good output satisfies addition; no mapped PDK, STA, PPA or silicon claim.

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

Testbench kiểm kết quả good với tham chiếu số nguyên từ chỉ số đầu vào, kiểm số mẫu, số lỗi, mask của broken và thời gian thật. Bản broken là đối chứng sai có chủ đích; bỏ phép kiểm hoặc sửa kỳ vọng không phải cách xác nhận công cụ hoạt động.

Wave được trích từ VCD của chính lần mô phỏng, 16 cột giữa các cạnh lấy mẫu. Giữ thêm cạnh lên thứ 17 để chặn biên cột cuối, rồi kết thúc tại 170 ns. Vét cạn chỉ áp dụng 16 cặp số không dấu xác định; Verilator đang dùng là mô hình 2-state, chưa kiểm X/Z.

Lint kiểm file RTL không có cảnh báo theo cấu hình đã ghi. Yosys tổng hợp generic cả hai hàm và kiểm không có flip-flop/latch. Đó là bằng chứng chấp nhận/cấu trúc, không phải chứng minh hàm broken đúng, hay kết quả mapping PDK, STA, PPA hoặc silicon.

[2] [3]

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

  1. IEEE 1800-2023 SystemVerilog LRM, Combinational expression widths and simulation timing — chưa đối chiếu LRM. Chưa đối chiếu với văn bản nguồn (chưa mở).
  2. Simulation & Synthesis Tools — bản chụp resources.zip, Understanding What Simulation Does; Yosys; Vivado; RTL Elaboration; Understanding Synthesis Results; Waveform Viewers; Learning Path: From Beginner to Advanced; Making the Most of Simulation. Trích dẫn; nguồn đã đọc các mục liên quan.
  3. Thí nghiệm nguyên bản A0.tools, Sixteen addition vectors, lint and generic synthesis, VCD carry comparison and runtime faults. Trích dẫn; nguồn đã đọc toàn văn.