形式約束與假設（Formal Constraints & Assumptions）

當你跑形式驗證時，工具被允許餵給設計「任何」它能想出的輸入——包括真實世界永不會產生的圖樣。放任不管，它會興高采烈地找出一堆只在輸入協定被違反時才發生的「臭蟲」，用假性失敗把你淹沒。約束（寫成 `assume` 性質）就是你在輸入空間外圍築起的圍籬：「假設匯流排主控永遠遵守 AXI 握手」。如此一來，工具只在合法輸入下獵蟲——也正是那些真正要緊的臭蟲。

這是「假設—保證（assume-guarantee）」契約的核心。每個區塊保證它的輸出行為良好，「前提是」它的輸入遵守那些假設；相鄰區塊接著把那些保證當成自己的輸入假設。危險在於這把雙面刃：「過度約束」會偷偷禁止合法輸入，可能藏起一個真臭蟲（工具從未探索那個失敗情境），而「約束不足」則放進非法輸入，用一堆假反例淹沒你。把約束拿捏得恰到好處——緊得切合實際、鬆得不漏掉任何東西——是形式驗證中最考驗功力、也最容易出錯的一環。