斷言（assertion）
想像在你的設計裡接了一個煙霧警報器。你只需把規則宣告一次——"這個警報永遠不能響"，或者"每個請求都必須在三個時脈節拍內得到回應"——從那以後就有一個小小的看守者守在那裡，睜大眼睛，每個週期都核對這條規則。一旦現實違反了規則，它就尖叫起來，並逕直指向出問題的地方。斷言正是如此：它是一種嵌入設計內部的檢查，一旦被宣告的屬性遭到違反就立即觸發。於是你不必再盯著成千上萬個波形週期苦苦猜測哪裡出了錯，模擬器會直接把你帶到規則第一次被打破的那個確切時刻和訊號上。
更確切地說，斷言是關於硬體必須如何行為的一種意圖陳述，它的寫法讓工具能夠持續地監視它。最常見的形式是 SystemVerilog 斷言（SVA），分為兩種風格。立即斷言在程序碼中的某一時刻檢查一個簡單條件，就像一句守衛語句。並行斷言則描述一種隨時間針對時脈而展開的關係——"如果 grant 拉高，那麼在兩個週期內 busy 必須隨之而來"——它在每個時脈邊緣都被求值，並在邊緣到來之前就取樣它的訊號，因此讀取的是穩定的值，而不會與這些訊號競爭。由於規則就緊貼在 RTL 旁邊，它以一種永遠不會悄悄過時的形式記錄下設計者的假設：一旦設計不再遵守這條假設，斷言就會失敗。
好處有兩方面。在模擬中，斷言把那些悄無聲息、波及深遠的錯誤，變成在源頭就被抓住的響亮失敗——這是"輸出錯了"與"漏洞就在這裡，在這條訊號上、在這個週期"之間的區別。而且因為它們是關於意圖的精確數學陳述，同一批斷言可以交給形式化工具，由它嘗試對所有合法輸入證明這些斷言為真，而不僅僅是你的測試平台碰巧嘗試過的那些激勵。覆蓋率工具還能追蹤每條斷言中那些有意思的情形究竟被觸發了多少次，於是你了解到的不只是"什麼都沒出錯"，還有你是否真的曾經測試過這條規則。
// If req is asserted, ack must arrive within 1 to 3 cycles. property p_req_ack; @(posedge clk) req |-> ##[1:3] ack; endproperty assert property (p_req_ack);
一條並行斷言：在每次 `req` 之後，工具檢查 `ack` 是否在一到三個時脈週期內隨之而來——一旦沒有，它立刻報錯。
這裡的"斷言"是設計做出的一種承諾，而不是用於除錯的 `print`。一條通過的斷言會在整個執行過程中默默無聲、毫無存在感；只有當出了問題時你才會聽到它的動靜——這正是為什麼一套周全的斷言是硬體設計中最廉價的保險之一。