防止Formal證明假PASS的辦法是什么
在FPV過程中，我們尤其需要注意假PASS，你以為完成了FPV full proven，實際上排除了很多合理的場景，最后得出的full proven是沒有意義的。
也就是說，
FPV主要分成2個部分，assert的證明以及思考我們是否已經覆蓋了所有合法的狀態空間。
工程師相互檢視是一個不錯的辦法，不過說實話，人太靈活，不夠靠譜。我們應該具有更加安全可靠的辦法來保證fpv cover和assume的正確性。
除了人為檢視之外，最常用的防止Formal證明假PASS的辦法就是將Formal環境中的所有assume和assert都集成在Simulation仿真驗證環境中。
如果某個子模塊能夠用Formal進行Sign off,那么不建議再開發一個EDA simulation驗證環境。但是不可避免地我們會有一個更高level的驗證環境，將這些formal assume和assert集成到這個high-level的驗證環境即可。
對于Formal驗證環境自身，最好的防止formal假PASS的方式還是多次強調的cover，只有Formal cover覆蓋到所有你關心的corner case，你才有足夠的交付信心。
使用formal進行交付，需要再次明確的是，sva cover比sva assert更加重要。
審核編輯：劉清
聲明：本文內容及配圖由入駐作者撰寫或者入駐合作網站授權轉載。文章觀點僅代表作者本人，不代表電子發燒友網立場。文章及其配圖僅供工程師學習之用，如有內容侵權或者其他違規問題，請聯系本站處理。
舉報投訴
-
eda
+關注
關注
71文章
2792瀏覽量
173969 -
FPV
+關注
關注
0文章
16瀏覽量
4522
原文標題：如何防止FPV Formal假PASS
文章出處：【微信號：芯片驗證工程師，微信公眾號：芯片驗證工程師】歡迎添加關注！文章轉載請注明出處。
發布評論請先 登錄
相關推薦
ADMV8505: 225 MHz to 520 MHz, Digitally Tunable, Band-Pass Filter Data Sheet adi
電子發燒友網為你提供ADI(ADI)ADMV8505: 225 MHz to 520 MHz, Digitally Tunable, Band-Pass Filter Data Sheet相關產品
發表于 01-15 18:54
常見墊圈故障及解決辦法 防漏墊圈的設計與應用
常見墊圈故障及解決辦法 1. 墊圈老化 故障現象： 墊圈因長時間使用而老化，失去彈性，導致密封性能下降。 解決辦法： 定期檢查墊圈的老化情況，及時更換新的墊圈。 2. 墊圈變形 故障現象： 由于安裝
常見MCU故障及解決辦法
微控制器單元（MCU）是現代電子設備中的核心組件，負責處理和控制各種功能。然而，由于各種原因，MCU可能會出現故障。以下是一些常見的MCU故障及其解決辦法： 1. 電源問題 故障現象： MCU無法
有什么辦法可以防止和解決運放的自激問題？
我經常會碰到當設計一些放大倍數很高的放大電路的時候，經過多級放大處理的話會直接導致，運放系統輸出進入飽和區，加了一些衰減之后還是處于自激的狀態，能夠有什么辦法可以防止和解決運放的自激問題
發表于 09-26 08:10
示波器統計曲線和故障分析pass/fail測試
虛擬示波器可以應用在工業自動化檢測中，除了常規的檢測波形和測量值參數以外，由多個行業客戶定制和驗證的統計曲線和故障分析（pass/fail）功能也為工業自動化檢測帶來極大的便利。（一）故障分析
發表于 08-30 10:19
LOTO示波器統計曲線和故障分析pass/fail測試
虛擬示波器可以應用在工業自動化檢測中，除了常規的檢測波形和測量值參數以外，由多個行業客戶定制和驗證的統計曲線和故障分析（pass/fail）功能也為工業自動化檢測帶來極大的便利。（一）故障分析
上電后，GPIO輸出會瞬間脈沖高電平，有沒有辦法防止這種情況發生？
上電后，GPIO輸出會瞬間脈沖高電平。有沒有辦法防止這種情況發生。從GPIO輸出所連接的電路中獲得大量浪涌電流.....謝謝
發表于 07-19 07:55
鴻蒙開發：Universal Keystore Kit密鑰管理服務 密鑰證明介紹及算法規格
HUKS為密鑰提供合法性證明能力，主要應用于非對稱密鑰的公鑰的證明。
gpio0有沒有辦法切換復位以防止獲取時鐘輸出？
我發現在原型設計情況下，gpio0 輸出 26Mhz 時鐘這一事實可能會導致相當多的噪聲問題。電纜等由于 gpio0 必須被拉高或拉低才能控制引導模式，因此它必須連接到編程器，通常通過電纜。有沒有辦法
發表于 07-08 06:45
使用sample code編譯程序pass,，cm0mdk腳本編譯fail怎么解決？
使用sample code 編譯程序pass, 更換project&quot;backup_fw&quot; 中bootloadable
發表于 06-03 07:06
I2C boot使用ARM GCC編譯pass, 改用ARM MDK編譯報錯怎么解決？
I2C boot 使用ARM GCC 編譯pass, 改用ARM MDK 編譯報錯如下, 怎么解決，謝謝！
cannot open source input file "
發表于 06-03 06:06
請問如何從4BF控制器中的ADC PASS0_CH_RANGEVIO_TR_OUT觸發TCPWM？
必須根據 ADC 范圍違規檢測觸發 TCPWM。 請問如何從 4BF 控制器中的 ADC PASS0_CH_RANGEVIO_TR_OUT 觸發 TCPWM。
發表于 05-21 07:50
造成虛焊、假焊的原因有哪些?如何預防虛焊假焊
虛焊 假焊 是在SMT貼片加工 中經常出現的不良現象，今天小編就給大家講講什么是虛焊、假焊?造成虛焊、假焊的原因有哪些?該如何預防虛焊假焊。 一、什么是虛焊、
假焊現象為什么會發生？如何處理？
假焊現象在生產過程中比較容易發生，許多商家對此非常苦惱。今天佳金源錫膏廠家就為大家詳細的介紹一下無鉛免洗錫膏假焊現象為什么會發生，在發生之后應該做出哪些對策進行處理：產生原因：無鉛免洗錫膏印刷過程中
工商網監
評論