搜索歷史

清空
搜索熱詞
      0
      • 聊天消息
      • 系統(tǒng)消息
      • 評論與回復(fù)
      VIP于 到期 續(xù)費
      登錄后你可以
      • 下載海量資料
      • 學(xué)習(xí)在線課程
      • 觀看技術(shù)視頻
      • 寫文章/發(fā)帖/加入社區(qū)
      會員中心
      創(chuàng)作中心
      發(fā)布
      創(chuàng)作活動

      完善資料讓更多小伙伴認(rèn)識你，還能領(lǐng)取20積分哦，立即完善>

      3天內(nèi)不再提示

      如何降低形式驗證的復(fù)雜度？

      芯片驗證工程師 ? 來源：芯片驗證工程師 ? 2023-02-22 09:48 ? 次閱讀

      當(dāng)計數(shù)器和內(nèi)存處于我們所需要證明斷言的邏輯錐中，它們可能是Formal無法完成證明的根本原因。

      因為形式分析算法很難適應(yīng)非常大的狀態(tài)空間，而計數(shù)器和存儲器都會引入很多的狀態(tài)空間和時序深度。針對這個問題，我們可以在不影響驗證完備性的條件下減小計數(shù)器和存儲器的大小或者用抽象模型替換。

      Formal驗證中優(yōu)化大計數(shù)器的一種流行且有效的方法是將它們替換為小型的狀態(tài)機模型（狀態(tài)空間?。?/strong>，該模型僅考慮會觸發(fā)設(shè)計操作的計數(shù)器臨界值。例如，假設(shè)計數(shù)器的值“m”、“n-1”和“n”很關(guān)鍵。考慮以下狀態(tài)機作為替代：

      c616d47a-b23c-11ed-bfe3-dac502259ad0.png

      為了用這個抽象模型替換原始計數(shù)器，我們首先繞過真實設(shè)計的驅(qū)動邏輯（用cutpoint的方式“切割”原始計數(shù)器輸出信號，使其變成一個自由隨機變量，然后向其添加約束）

      下面是一個計數(shù)器示例

      c641c43c-b23c-11ed-bfe3-dac502259ad0.png

      這種辦法主要還是用于bug-hunting，而且如果RTL中的其他部分實際就需要計數(shù)器延遲特定周期，那么這個優(yōu)化方法就不適用了，所以說此時就沒法用作formal full prove。





      聲明：本文內(nèi)容及配圖由入駐作者撰寫或者入駐合作網(wǎng)站授權(quán)轉(zhuǎn)載。文章觀點僅代表作者本人，不代表電子發(fā)燒友網(wǎng)立場。文章及其配圖僅供工程師學(xué)習(xí)之用，如有內(nèi)容侵權(quán)或者其他違規(guī)問題，請聯(lián)系本站處理。 舉報投訴
      • 存儲器
        +關(guān)注

        關(guān)注

        38

        文章

        7376

        瀏覽量

        163143
      • 計數(shù)器
        +關(guān)注

        關(guān)注

        32

        文章

        2242

        瀏覽量

        94018
      • RTL
        RTL
        +關(guān)注

        關(guān)注

        1

        文章

        384

        瀏覽量

        59534

      原文標(biāo)題：如何降低形式驗證的復(fù)雜度——計數(shù)器抽象

      文章出處：【微信號：芯片驗證工程師，微信公眾號：芯片驗證工程師】歡迎添加關(guān)注！文章轉(zhuǎn)載請注明出處。

      收藏 人收藏

        評論

        相關(guān)推薦

        PCB與PCBA工藝復(fù)雜度的量化評估與應(yīng)用初探！

        ， 不知道如何區(qū)分普通和復(fù)雜的PCB和 PCBA的設(shè)計，并采用什么樣的方式來處理。 基于上述考慮， 我們參考了業(yè) 界已有的作法， 設(shè)計了一個PCB 和 PCBA的工藝復(fù)雜度計算公式以解決這 方面
        發(fā)表于 06-14 11:15

        基于紋理復(fù)雜度的快速幀內(nèi)預(yù)測算法

        為降低幀內(nèi)預(yù)測的運算復(fù)雜度,根據(jù)不同的模式在宏塊中出現(xiàn)概率的大小不同,在幀內(nèi)4×4的亮度預(yù)測模式中,選取出現(xiàn)概率最大的5種預(yù)測模式,作為優(yōu)先選擇的預(yù)測模式?；谙袼貕K的紋理特性,選擇不具有
        發(fā)表于 05-06 09:01

        JEM軟件復(fù)雜度的增加情況

        這篇文檔展示了幾個機構(gòu)關(guān)于JEM軟件復(fù)雜度的增加情況的看法，特別提出來創(chuàng)立一個新的Ad-hoc組，研究降低軟件一般性復(fù)雜度的可能方法。
        發(fā)表于 07-19 08:25

        如何降低LMS算法的計算復(fù)雜度，加快程序在DSP上運行的速度，實現(xiàn)DSP?

        基于線性預(yù)測的FIR自適應(yīng)語音濾波器的系統(tǒng)結(jié)構(gòu)由那幾部分組成？如何降低LMS算法的計算復(fù)雜度，加快程序在DSP上運行的速度，實現(xiàn)DSP?
        發(fā)表于 04-12 06:27

        時間復(fù)雜度是指什么

        原理->微機原理->軟件工程，編譯原理，數(shù)據(jù)庫數(shù)據(jù)結(jié)構(gòu)1.時間復(fù)雜度時間復(fù)雜度是指執(zhí)行算法所需要的計算工作量，因為整個算法的執(zhí)行時間與基本操作重復(fù)執(zhí)行的...
        發(fā)表于 07-22 10:01

        降低高條件數(shù)信道下的球形譯碼算法復(fù)雜度的方法

        MIMO 系統(tǒng)中，球形譯碼可以在保證接近ML 檢測性能的前提下大大降低檢測復(fù)雜度。但當(dāng)信道矩陣條件數(shù)很高時，球形譯碼的復(fù)雜度仍然會很高。在分析了這一現(xiàn)象的原因后，本文提出
        發(fā)表于 11-21 13:52 ?8次下載

        圖像復(fù)雜度對信息隱藏性能影響分析

        針對信息隱藏中載體圖像的差異性，提出一種圖像復(fù)雜度評價方法，綜合考慮圖像的壓縮特性以及圖像紋理能量作為圖像復(fù)雜度指標(biāo)，并基于閾值劃分準(zhǔn)則對栽體圖像進(jìn)行復(fù)雜度分類，以幾種經(jīng)典的基于直方圖的幾種無損隱藏
        發(fā)表于 11-14 09:57 ?5次下載

        商湯聯(lián)合提出基于FPGA的Winograd算法：改善FPGA上的CNN性能 降低算法復(fù)雜度

        商湯科技算法平臺團隊和北京大學(xué)高能效實驗室聯(lián)合提出一種基于 FPGA 的快速Winograd算法，可以大幅降低算法復(fù)雜度，改善 FPGA 上的 CNN 性能。
        的頭像 發(fā)表于 02-07 11:52 ?9035次閱讀
        商湯聯(lián)合提出基于FPGA的Winograd算法：改善FPGA上的CNN性能 <b class='flag-5'>降低</b>算法<b class='flag-5'>復(fù)雜度</b>

        深度剖析時間復(fù)雜度

        相信每一位錄友都接觸過時間復(fù)雜度，但又對時間復(fù)雜度的認(rèn)識處于一種朦朧的狀態(tài)，所以是時候?qū)r間復(fù)雜度來一個深度的剖析了。
        的頭像 發(fā)表于 03-18 10:18 ?1796次閱讀

        如何求遞歸算法的時間復(fù)雜度

        相信很多同學(xué)對遞歸算法的時間復(fù)雜度都很模糊，那么這篇Carl來給大家通透的講一講。
        的頭像 發(fā)表于 07-13 11:33 ?1526次閱讀

        算法之空間復(fù)雜度

        算法之空間復(fù)雜度：衡量一個算法運行需要開辟的額外空間
        的頭像 發(fā)表于 08-31 10:29 ?1514次閱讀

        可以通過降低約束的復(fù)雜度來優(yōu)化Formal的執(zhí)行效率嗎？

        我們可以通過降低約束的復(fù)雜度來優(yōu)化Formal的執(zhí)行效率，但是這個主要是通過減少Formal驗證空間來實現(xiàn)的，很容易出現(xiàn)過約，導(dǎo)致bug遺漏。
        的頭像 發(fā)表于 02-15 15:14 ?784次閱讀

        如何計算時間復(fù)雜度

        1 算法與時間復(fù)雜度 算法（Algorithm）是求解一個問題需要遵循的，被清楚指定的簡單指令的集合。 算法一旦確定，那么下一步就要確定該算法將需要多少時間和空間等資源，如果一個算法需要一兩年的時間
        的頭像 發(fā)表于 10-13 11:19 ?2333次閱讀
        如何計算時間<b class='flag-5'>復(fù)雜度</b>

        如何降低SigmaDSP音頻系統(tǒng)復(fù)雜度的情形

        電子發(fā)燒友網(wǎng)站提供《如何降低SigmaDSP音頻系統(tǒng)復(fù)雜度的情形.pdf》資料免費下載
        發(fā)表于 11-29 11:13 ?0次下載
        如何<b class='flag-5'>降低</b>SigmaDSP音頻系統(tǒng)<b class='flag-5'>復(fù)雜度</b>的情形

        降低Transformer復(fù)雜度O(N^2)的方法匯總

        首先來詳細(xì)說明為什么Transformer的計算復(fù)雜度是 。將Transformer中標(biāo)準(zhǔn)的Attention稱為Softmax Attention。令 為長度為 的序列, 其維度為 , 。 可看作Softmax Attention的輸入。
        的頭像 發(fā)表于 12-04 15:31 ?911次閱讀
        <b class='flag-5'>降低</b>Transformer<b class='flag-5'>復(fù)雜度</b>O(N^2)的方法匯總