斷言與斷言驗證（SVA）

藏在一萬個週期之外的臭蟲

想像有一家銀行，偵測舞弊的唯一辦法是等到年底，把每個帳戶加總，看帳目是否平衡。如果不平，某處出了錯——但是哪一筆交易？哪一天？哪一家分行？你得花上好幾週把整本帳目倒推回去。傳統測試平台抓臭蟲的方式正是如此：它灌入刺激、讓設計跑上數千個時脈週期，最後把輸出和參考模型比對。當不一致出現在第 84,217 個週期時，真正的錯誤——一個被寫入時其實已經滿了的 FIFO——可能發生在第 31,002 個週期。輸出檢查只是症狀；根本原因埋在上游 53,000 個週期之外。

斷言則是一位持續監看的稽核員，就站在那家分行、那個櫃台前。一旦有人想寫入已滿的 FIFO，稽核員立刻發作——就在第 31,002 個週期、就在那條訊號上、就在那個模組裡。你在源頭除錯，而不是在症狀處除錯。這就是這項技術全部的承諾，也是為什麼一條 SystemVerilog 斷言（SVA）是你能加進 RTL 設計中槓桿最高的東西之一。

兩種口味：立即式 vs 並行式

SVA 有兩種，把它們搞混是初學者最常犯的錯誤。立即式斷言（immediate assertion）其實就是一個寫在程序式（procedural）程式碼裡的 `if` 檢查。當模擬執行到它時就立刻發作，像一個會在你話講到一半時打斷你的朋友。它沒有時脈或時間的概念——它檢查此刻的條件。把它用於 `always` 區塊或測試平台程式碼裡的合理性檢查：「這個索引必須在範圍內」、「這個狀態此刻不是 X」。

// IMMEDIATE — runs inside procedural code, no clock involved
always @(posedge clk) begin
  if (wr_en) begin
    assert (!full)
      else $error("write to FULL fifo at addr %0d", wr_ptr);
  end
end

// CONCURRENT — a standalone temporal contract, sampled every clock
assert property (@(posedge clk) wr_en |-> !full);
//        \____ property ____/    \__ antecedent _/  \_ consequent _/

同一條規則——「絕不寫入已滿的 FIFO」——分別寫成立即式斷言（程序式）與並行式斷言（時序合約）。

並行式斷言（concurrent assertion）才是真正的主角。它是一個獨立、宣告式（declarative）的敘述，存在於程序式程式碼之外，在時脈邊緣被求值，跨越時間地比較數值。線索就是關鍵字 `property` 與一個像 `@(posedge clk)` 的時脈事件。並行式斷言能說出任何 `if` 敘述都說不出的話：「請求必須在 3 個週期內被允許」、「在 `start` 上升之後，`done` 終究必須上升，而在那之前 `error` 必須保持低電位」。它們對事件序列進行推理，而協定正是由事件序列構成的。

序列與性質：一套關於時間的文法

並行式斷言由兩層構成，就像句子由片語組成。序列（sequence）是片語——在連續時脈週期上展開的訊號數值樣式。性質（property）則是完整的句子——它用蘊涵（implication）與邏輯運算子把序列組合起來，陳述一條完整的規則。你先寫片語，再把它們組裝成合約。

// ## DELAY: ##N means "N clocks later"; ##[1:3] is a window
sequence req_then_gnt;
  req ##[1:3] gnt;        // gnt comes 1 to 3 cycles after req
endsequence

// ## REPETITION: [*N] = N times; [->N] = the N-th occurrence
sequence stable_burst;
  valid [*4];            // valid held high for 4 consecutive cycles
endsequence

// ## IMPLICATION builds a property from an antecedent and a consequent
property handshake;
  @(posedge clk) disable iff (rst)
    req |-> ##[1:3] gnt; // if req, THEN gnt within 1..3 cycles
endproperty

assert property (handshake);   // turn the contract into a live check

序列描述跨時間的樣式；性質用蘊涵把它們包起來；assert 把它變成執行期的檢查。

幾乎每條性質的核心都是蘊涵運算子（implication operator）。`a |-> b` 讀作「如果 `a`（前項，antecedent）成立，那麼 `b`（後項，consequent）就必須成立」。重疊形式 `|->` 在前項結束的同一週期就開始檢查後項；非重疊形式 `|=>` 則晚一個週期才開始檢查。蘊涵的美妙之處在於空真（vacuity）：當前項從未發生時，性質就理所當然為真而保持沉默。一條「3 個週期內必須允許」的規則，在沒有請求的週期裡什麼都不做——這正是你要的。

assert · assume · cover——同一條性質，三種工作

這裡是會在第 8 階得到回報的優雅之處。一旦你寫好一條性質，你可以用三個關鍵字把它導向三種不同用途——而性質本文完全不需要改動。這就是模擬與形式驗證之間的橋樑。

assert——檢查它。工具必須證明（在形式驗證中）或永遠不能觀察到（在模擬中）這條性質被違反。這是你的義務：「我主張這永遠為真；若不是，就抓住我。」
assume——信任它。這條性質描述對輸入的約束——一個關於環境如何行為的承諾。在模擬中它是一個檢查；在形式驗證中它限制了合法的輸入空間，讓證明器只探索符合現實的情境。「匯流排主控端絕不會在未等到允許前就送出兩次請求。」
cover——量測它。它問的是「這個有趣的情境到底有沒有真的發生過？」它永遠不會失敗——它要嘛成立，要嘛從未觸發。一個對 `req ##[1:3] gnt` 的 `cover` 會告訴你，你的刺激到底有沒有真的演練過那個你費心檢查的交握。

// One property text → three uses
property p_no_overflow;
  @(posedge clk) disable iff (rst) wr_en |-> !full;
endproperty

assert property (p_no_overflow);   // DUT must obey this
assume property (p_bus_legal);     // environment promises this (constrains inputs)
cover  property (p_no_overflow);   // did we ever even write near-full? did the case occur?

assert／assume／cover 是套在同一個名詞上的三個動詞。assert＝義務，assume＝環境合約，cover＝有沒有被演練到。

把斷言驗證當作一種方法論

灑幾條 assert 只是個小技巧。斷言驗證（assertion-based verification，ABV）則是一種方法論——一種刻意的實踐：把設計意圖捕捉成一張密集的斷言之網，及早寫下，並永遠活在程式碼裡。回報會複利累積。斷言只寫一次，卻會在你回歸測試（regression）中的每一個測試上、全天候、零額外刺激地檢查。它們把一個只檢查輸出的被動測試平台，變成數千個內部監看器，在每一個週期檢查每一個協定、每一個 FIFO、每一個交握。

這些斷言有兩個歸宿。白箱（white-box）斷言住在 RTL 內部，由那位知道 `wr_ptr` 絕不該越過 `rd_ptr` 的設計者撰寫——它們在內部錯誤發生的瞬間就抓到它。黑箱（black-box，即介面）斷言則坐落在模組邊界與標準協定上。供應商會提供預先封裝好的斷言 IP——例如一整套 AMBA AXI 檢查器——讓你把上百條經過手工驗證的協定規則綁定到你的介面上，而一條都不必自己寫。許多設計者會重用 UVM 監看器用來標記非法交易所依賴的那同一套檢查。

看門狗到底有沒有醒過？斷言覆蓋率

這裡有個連強隊伍都會中招的陷阱。一條從不失敗的性質感覺像是好消息——但一條前項從未成立的性質，同樣也是一條從未做過任何事的性質。如果在你所有測試裡 `req` 都沒被拉高過，那麼 `req |-> gnt` 在每一次執行中都通過，卻什麼也沒證明。一面全部通過的綠色儀表板，可能完全是空心的。

這正是第 6 階的覆蓋率思維，如今對準了檢查本身。斷言覆蓋率（assertion coverage）量測每一條斷言是否真的被演練過——具體來說，是它的前項有沒有曾經成立，讓後項真的被測試到。它是你早已在設計上追蹤的功能覆蓋率的天然夥伴，也是 RTL 結構性程式碼覆蓋率的天然夥伴。設計的覆蓋率告訴你 DUT 做了什麼；斷言覆蓋率告訴你你的檢查有沒有在看它。

ASSERTION REPORT                attempts  pass  fail  vacuous
--------------------------------------------------------------
p_no_overflow  (wr_en |-> !full)    8421   8421     0        0   <- good: real checks happened
p_handshake    (req   |-> gnt)         0      0     0        0   <- ALARM: never exercised!
p_no_x_on_bus  (!$isunknown(data))  152k   152k     0      14k   <- 14k vacuous: antecedent rarely true

一份斷言覆蓋率報告。p_handshake 的嘗試次數為零，代表刺激有破口，而非設計健康——那條檢查在睡覺。

這裡就是通往第 8 階的優雅橋樑。你為模擬寫的那同一條性質，正是性質檢查（property checking）工具讀進去、嘗試做數學證明的輸入——窮舉式地、對每一個合法輸入、完全不需要任何刺激。在模擬中，一條斷言的好壞，全看有沒有測試去絆倒它；在形式驗證中，工具會自己嘗試每一條路徑。你的 `assume` 敘述變成形式約束，你的 `assert` 敘述變成證明義務，你的 `cover` 敘述變成可達性目標。光是練習有紀律的 ABV，你就已經寫好了 90% 的形式驗證設定。