如何降低形式驗證的復雜度？
當計數器和內存處于我們所需要證明斷言的邏輯錐中，它們可能是Formal無法完成證明的根本原因。
因為形式分析算法很難適應非常大的狀態空間，而計數器和存儲器都會引入很多的狀態空間和時序深度。針對這個問題，我們可以在不影響驗證完備性的條件下減小計數器和存儲器的大小或者用抽象模型替換。
Formal驗證中優化大計數器的一種流行且有效的方法是將它們替換為小型的狀態機模型（狀態空間小），該模型僅考慮會觸發設計操作的計數器臨界值。例如，假設計數器的值“m”、“n-1”和“n”很關鍵。考慮以下狀態機作為替代：
為了用這個抽象模型替換原始計數器，我們首先繞過真實設計的驅動邏輯（用cutpoint的方式“切割”原始計數器輸出信號，使其變成一個自由隨機變量，然后向其添加約束）
下面是一個計數器示例
這種辦法主要還是用于bug-hunting，而且如果RTL中的其他部分實際就需要計數器延遲特定周期，那么這個優化方法就不適用了，所以說此時就沒法用作formal full prove。
聲明：本文內容及配圖由入駐作者撰寫或者入駐合作網站授權轉載。文章觀點僅代表作者本人，不代表電子發燒友網立場。文章及其配圖僅供工程師學習之用，如有內容侵權或者其他違規問題，請聯系本站處理。
舉報投訴
-
存儲器
+關注
關注
39文章
7739瀏覽量
171674 -
計數器
+關注
關注
32文章
2316瀏覽量
98181 -
RTL
+關注
關注
1文章
394瀏覽量
62656
原文標題：如何降低形式驗證的復雜度——計數器抽象
文章出處：【微信號：芯片驗證工程師，微信公眾號：芯片驗證工程師】歡迎添加關注！文章轉載請注明出處。
發布評論請先 登錄
相關推薦
熱點推薦
PCB與PCBA工藝復雜度的量化評估與應用初探！
， 不知道如何區分普通和復雜的PCB和 PCBA的設計，并采用什么樣的方式來處理。
基于上述考慮， 我們參考了業 界已有的作法， 設計了一個PCB 和 PCBA的工藝復雜度計算公式以解決這 方面
發表于 06-14 11:15
基于紋理復雜度的快速幀內預測算法
為降低幀內預測的運算復雜度,根據不同的模式在宏塊中出現概率的大小不同,在幀內4×4的亮度預測模式中,選取出現概率最大的5種預測模式,作為優先選擇的預測模式。基于像素塊的紋理特性,選擇不具有
發表于 05-06 09:01
如何降低LMS算法的計算復雜度，加快程序在DSP上運行的速度，實現DSP?
基于線性預測的FIR自適應語音濾波器的系統結構由那幾部分組成？如何降低LMS算法的計算復雜度，加快程序在DSP上運行的速度，實現DSP?
發表于 04-12 06:27
時間復雜度是指什么
原理->微機原理->軟件工程，編譯原理，數據庫數據結構1.時間復雜度時間復雜度是指執行算法所需要的計算工作量，因為整個算法的執行時間與基本操作重復執行的...
發表于 07-22 10:01
降低高條件數信道下的球形譯碼算法復雜度的方法
MIMO 系統中，球形譯碼可以在保證接近ML 檢測性能的前提下大大降低檢測復雜度。但當信道矩陣條件數很高時，球形譯碼的復雜度仍然會很高。在分析了這一現象的原因后，本文提出
發表于 11-21 13:52
?8次下載
圖像復雜度對信息隱藏性能影響分析
針對信息隱藏中載體圖像的差異性，提出一種圖像復雜度評價方法，綜合考慮圖像的壓縮特性以及圖像紋理能量作為圖像復雜度指標，并基于閾值劃分準則對栽體圖像進行復雜度分類，以幾種經典的基于直方圖的幾種無損隱藏
發表于 11-14 09:57
?5次下載
商湯聯合提出基于FPGA的Winograd算法：改善FPGA上的CNN性能 降低算法復雜度
商湯科技算法平臺團隊和北京大學高能效實驗室聯合提出一種基于 FPGA 的快速Winograd算法，可以大幅降低算法復雜度，改善 FPGA 上的 CNN 性能。
可以通過降低約束的復雜度來優化Formal的執行效率嗎？
我們可以通過降低約束的復雜度來優化Formal的執行效率，但是這個主要是通過減少Formal驗證空間來實現的，很容易出現過約，導致bug遺漏。
如何計算時間復雜度
1 算法與時間復雜度 算法（Algorithm）是求解一個問題需要遵循的，被清楚指定的簡單指令的集合。 算法一旦確定，那么下一步就要確定該算法將需要多少時間和空間等資源，如果一個算法需要一兩年的時間
降低Transformer復雜度O(N^2)的方法匯總
首先來詳細說明為什么Transformer的計算復雜度是 。將Transformer中標準的Attention稱為Softmax Attention。令 為長度為 的序列, 其維度為 , 。 可看作Softmax Attention的輸入。
工商網監
評論