SV scheduling: một time slot có thể cần nhiều lượt Active và NBA

Ba thay đổi không nhất thiết là ba nanosecond

A đổi làm process khác cập nhật B; B đổi lại làm process thứ ba cập nhật C. Nếu đều không có delay dương, chuỗi này có thể ổn định trong cùng một time slot dù scheduler cần xử lý nhiều sự kiện. Đọc dòng log cùng timestamp chưa đủ biết process nào đọc state trước hay sau cập nhật.

Bài A7 đã giới thiệu Active/Inactive/NBA. Ở đây mở rộng cách đọc sang sơ đồ SV có sampling/assertion/program nhưng không giả vờ một ví dụ nhỏ đã chạy mọi region. Main tập trung chuỗi NBA re-entry và đối chiếu #0 với Postponed trên Icarus 4-state.

Sơ đồ bảy vùng là bản đồ rút gọn

Preponed phục vụ sampling đầu time slot; nhóm Active/Inactive/NBA chứa nhiều hoạt động module; Observed dùng đánh giá concurrent assertion trên mẫu đã lấy; nhóm Reactive dành cho hoạt động testbench như program; Postponed dùng quan sát cuối time slot như $strobe. Đây là các mốc định hướng, không phải danh sách đầy đủ mọi vùng PLI và re-region.

Không coi scheduler như chuyến tàu chỉ qua mỗi ga một lần. Một cập nhật NBA có thể làm process thuộc Active được đánh thức; hoạt động mới lại đặt NBA tiếp. Các chi tiết chuẩn vẫn cần đối chiếu LRM, còn ví dụ dưới chỉ đo tập con được nêu rõ.

^[1]

#0 không có nghĩa đợi mọi NBA xong

Main ở 5 ns lên lịch a<=1 rồi kiểm a vẫn 0 trong process module đang chạy. Tiếp theo #0 đưa phần tiếp tục vào Inactive của cùng time slot; khi đọc lại, a vẫn 0 vì NBA tương ứng chưa cập nhật. Cả hai phép kiểm nằm trong hợp đồng đã chủ động sắp xếp, không dựa vào thứ tự tùy ý giữa hai writer.

Chèn nhiều #0 để thử “đợi đủ lâu” không tạo một cạnh clock, không phải delay vật lý và không bảo đảm đã đi qua điểm ổn định bạn cần. Nếu cần mẫu cuối time slot để in log, dùng cơ chế phù hợp như $strobe; nếu cần checker synchronous, xác định đúng sample/clocking contract.

NBA của a đánh thức process tạo NBA của b

Các tín hiệu ban đầu 0. Khi a nhận 1, process theo @(a) lên lịch b<=1. Khi b nhận 1, process theo @(b) lên lịch c<=1. Mỗi thay đổi được đếm ở process tương ứng; c lên 1 cho tổng ba change. Các khởi tạo 0 không được đếm như ba lần chuyển lên 1.

Không có #delay dương trên đường a→b→c. Sau khi scheduler giải hết công việc ở 5 ns, state cuối là 111. Đây là quan hệ sự kiện trong mô phỏng, không phải ba flip-flop nhận ba cạnh clock và cũng không mô tả propagation delay của ba cổng silicon.

Strobe nhìn state cuối, không phải checkpoint cho process khác

Main gọi $strobe ở 5 ns để in SV POSTPONED a=1 b=1 c=1 time_ns=5. Giá trị được quan sát ở Postponed sau chuỗi cập nhật của time slot ấy. Checker có thêm một điểm ở 6 ns kiểm 111 và changes=3, nên không chỉ dựa vào một dòng log đẹp.

Gọi $strobe không khiến các statement tiếp theo của process tự chờ đến Postponed. Nó lập lịch việc in; phần tiếp tục vẫn tuân theo control của process. Cũng không dùng một action log để suy concurrent assertion đã sample cùng giá trị raw mà log thấy sau NBA.

^[2]

NBA không tự làm mọi nguồn dữ liệu ổn định

RHS của NBA được lấy khi statement thực thi. Nếu input đang bị một process khác ghi bằng blocking ở cùng Active event, giá trị RHS vẫn có thể phụ thuộc thứ tự hai process. Không dùng câu “mọi RHS luôn là pre-edge” mà bỏ điều kiện nguồn ổn định và ownership.

Main có một nguồn cập nhật khởi phát và hai process theo thay đổi, không có hai writer tranh a/b/c. Vì vậy nó chứng minh chuỗi đã sắp xếp của riêng ví dụ; nó không tái hiện mọi nondeterminism hoặc đảm bảo mọi simulator chọn nhiều thứ tự trong một lần chạy. Bài A7.races giữ hai reference order để giải thích vấn đề đó.

Chọn engine theo semantic cần kiểm

Main dùng Icarus 11.0 để thực thi #0 và chuỗi event. Verilator có các giới hạn liên quan delay/scheduling; không chuyển engine chỉ vì một tool chạy nhanh hơn rồi coi mọi ngữ nghĩa được giữ nguyên. Bằng chứng ghi rõ engine thay vì chỉ nói “mô phỏng PASS”.

Main không có concurrent assertion, action block hoặc program. Probe Reactive trong bài program có failure riêng trên Verilator; không dùng state 111 của bài này để gọi probe ấy đã sửa. Nhãn parsed/simulated áp dụng đúng source/engine trong verification.json.

Giữ timestamp 5 ns qua ba cập nhật

Expected trước chạy gồm dòng Postponed 111 tại 5 ns và summary SV REGIONS CHECK inactive_a=0 chained_updates=3 final=111 time_ns=6. Pipeline yêu cầu cả hai dòng, exit 0 và mọi oracle nội bộ.

`timescale 1ns/1ps// Expected at5ns: Active/Inactive see a0; three NBA-triggered updates settle111, time remains5.module tb_sv_regions; bit a=0,b=0,c=0; int changes=0,inactive_a=-1; always @(a)if(a)begin b<=1;changes++;end always @(b)if(b)begin c<=1;changes++;end always @(c)if(c)changes++; initial begin  #5;a<=1;  if(a!==0)$fatal(1,"SV Active old-a oracle");  #0;inactive_a=int'(a);  if(inactive_a!=0||$time!=5)$fatal(1,"SV Inactive before-NBA oracle");  $strobe("SV POSTPONED a=%0b b=%0b c=%0b time_ns=%0d",a,b,c,$time);  #1;  if(a!==1||b!==1||c!==1||changes!=3||$time!=6)$fatal(1,"SV NBA re-entry oracle");  $display("SV REGIONS CHECK inactive_a=0 chained_updates=3 final=111 time_ns=6");$finish; endendmodule

Hai mutant giữ nguyên checker: đổi a<=1 thành blocking assignment và chặn b lên 1. Chúng bị bắt ở oracle Active và oracle NBA re-entry. Không đếm mutant lỗi như main mô phỏng đạt.

^[3]

Tự kiểm tra

Theo event, region và state thay vì chỉ timestamp

Khi debug một time slot, ghi statement nào đọc RHS, statement nào lên lịch update và update nào đánh thức process tiếp. Phân biệt Inactive với Postponed, sampled value với raw value và simulation event với chu kỳ phần cứng. Một sơ đồ ngắn giúp định hướng, nhưng expected cụ thể và tool thật mới xác nhận ví dụ của bạn.