近年來，卷積神經網絡（CNN）在圖像處理和計算機視覺領域取得了巨大成功，如人臉識別、姿態估計等。然而，基于CNN的圖像處理單元設計復雜，驗證工作面臨巨大挑戰。傳統的仿真驗證方法難以覆蓋其龐大的配置空間，且耗時費力。本文將介紹一種創新的形式化驗證（Formal Verification, FV）方法，用于高效驗證CNN圖像處理單元。
驗證挑戰
CNN圖像處理單元的配置空間極為龐大（約2Nx1000，N>0），數據處理算法復雜。傳統的仿真驗證方法，無論是定向測試還是約束隨機測試，都難以有效覆蓋如此龐大的配置空間。此外，市場對產品上市時間的要求限制了驗證時間，使得通過仿真驗證完全覆蓋所有配置變得不切實際。
形式化驗證方法
開發幀斷言IP（Frame Assertion IP, AIP）
圖像處理過程中，圖像被分割成多個幀，每個幀又分為多個像素。幀具有以下屬性：
?  SOF（Start of Frame）：幀起始
?  EOF（End of Frame）：幀結束
?  SOL（Start of Line）：行起始
?  EOL（End of Line）：行結束
幀AIP通過斷言確保每個像素的屬性正確，包括：
1.  像素位置與屬性匹配的斷言（如行首像素應有SOL屬性）
2.  幀完整性斷言（如幀起始后必須有幀結束）
3.  幀存在性斷言（如無幀時最終會出現幀）
加速FV測試平