形式驗證

佇咧電腦硬體（特別是積體電路）佮軟體系統的設計過程當中，形式驗證的含義是根據某一个抑是某寡形式規範或者是屬性，使用數學的方法證明其正確性抑是無正確性。

解說

軟體測試無法證明系統不存在缺陷，嘛袂當證明講伊符合一定的屬性。只有形式化驗證的過程會當證明一个系統無存在某一个缺陷或者是符合某一个或者是某一寡屬性。系統無法度予證明抑是測試做無缺陷，這是因為無可能形式地規定啥物是「無缺陷」。所有會當做的，就是證明一个系統無任何會當想著的缺陷，並且滿足所有的使系統符合功能要求的佮有用的屬性。

佇積體電路設計中，形式驗證是一款積體電路設計的驗證方法，伊的主要思想是通過使用形式證明的方式來驗證一个設計的功能是毋是正確。形式驗證會當分做三大類：抽象來解說（Abstract Interpretation）、形式模型檢查（Formal Model Checking，嘛予人號做特性檢查）佮定理證明（Theory Prover）。

等價性檢查的驗證用於驗證暫存器傳輸級設計和門級網表之間、門級網表佮門級網表之間敢有一致。咧進行掃描鏈重排、時鐘樹綜合等過程中，攏會當用等價性檢查保證網表的一致性。等價性檢查已經融入積體電路標準設計流程中。等價性檢查咧檢查 ECO 不止仔有效。比如講，設計者咧修改門級網表的時陣，因為手誤，毋著將一个抑是門寫做抑是非門，等價性檢查工具通過較暫存器傳輸級設計佮門級網表，會用得真容易發現這種錯誤。

模型檢查用時態邏輯來描述規範，通過有效的搜尋方法來檢查予定的系統敢有滿足規範咧。模型檢查是目前研究的熱點，毋過驗證的電路規模受限制這一問題猶無得著誠好的解決。

定理證明共系統佮規範攏表示成數學邏輯公式，對公理出發尋求咧講。定理證明驗證的電路模型無受限制，毋過需要使用者的人工干預佮較濟背景智識。

解說

相關條目