形式驗證（formal verification）
想像你造了一把數位鎖，你想確認：沒有正確的密碼，它絕不可能打開。用模擬，你會輸入幾千個錯誤密碼，每次都看著它保持鎖閉，於是感覺挺踏實——但你只檢查了恰好試過的那些密碼。形式驗證走的是相反的路：它不去測試若干例子，而是用數學證明——證明任何可能的輸入、以任何順序，都絕不可能把這把鎖打開。一份滴水不漏的證明，頂得上無窮多次試驗。
具體來說，形式工具會接收你的設計（即 RTL）外加一條你寫下的屬性——一句精確的斷言，比如「授權訊號絕不會同時對兩個主裝置置位」——並把整個電路當作一個數學結構，對它全部可達的狀態空間進行推理。如果該屬性在每一種合法的輸入序列下都成立，工具就回傳已證明。如果不成立，工具會交給你一個具體的反例：一段精確的波形，逐步展示是什麼破壞了它。你再也不必為「測試寫夠了沒？」而焦慮，因為這種搜尋從構造上就是窮盡式的。這也使它成為斷言的天然搭檔——斷言正是你用來陳述這些屬性的語法結構，通常以 SystemVerilog 斷言（SVA）寫成。
玄機就藏在「窮盡」這個詞裡。它只對你陳述的那條屬性、以及你所指向的那個設計模組成立——形式驗證完整地證明了那條主張，卻並不證明你的晶片整體正確。而且可達狀態空間會爆炸式成長，因此較大的模組可能撐爆記憶體或時間上限，迫使你去約束輸入、分解問題，或者接受一個只在 N 個時脈週期內成立的有界證明。形式驗證在控制邏輯、仲裁器和協定檢查上鋒利無比；但它不適合用來驗證一個寬位的資料路徑乘法器，那種場合約束隨機模擬仍然大有用武之地。
// At every clock edge (outside reset), at most one grant is asserted.
property p_grant_mutex;
@(posedge clk) disable iff (rst)
$onehot0(grant);
endproperty
a_grant_mutex: assert property (p_grant_mutex);上面那條「兩個主裝置」屬性，寫成一條廠商中立的 SystemVerilog 並行斷言，表達的是 grant 至多是獨熱（one-hot）的——在任意時脈下至多有一位被置位。形式工具要麼回傳已證明——任何可達狀態都不會同時拉高兩個 grant——要麼給出一段反例波形，精確展示兩個主裝置是如何同時被授權的。
「形式驗證」和「模型檢查」常被當作同義詞混用，但模型檢查其實只是形式驗證大傘下的一種技術（與等價性檢查、定理證明並列）。它們共同的內核是：保證來自對所有情形的數學證明，而不是來自跑幾個例子。