基于SystemC的時態(tài)邏輯屬性驗證方法研究.pdf

1、系統(tǒng)復雜性繼續(xù)按照摩爾定律增加，而功能復雜性的增加速度則更加迅猛。為解決復雜性增加的問題，EDA行業(yè)提出了通過自動化來實現(xiàn)設(shè)計抽象（Design Abstraction）的概念。由于設(shè)計生產(chǎn)率的提升速度低于系統(tǒng)復雜性的增速，此時與設(shè)計相關(guān)的瓶頸已并非設(shè)計時間，而是驗證時間，即驗證瓶頸。為此，人們創(chuàng)建了能夠在不同抽象級別上對復雜系統(tǒng)設(shè)計進行驗證的新型驗證語言，例如，高級驗證語言SystemC。實踐證明SystemC是一種優(yōu)秀的系統(tǒng)設(shè)計描述

2、驗證語言，它能夠完成從系統(tǒng)級到門級、從軟件到硬件、從設(shè)計到驗證的全部描述。 本文闡述了基于SystemC的主要驗證方法和相關(guān)理論，以及時態(tài)邏輯理論和在驗證領(lǐng)域中的應(yīng)用，一方面分析了在動態(tài)仿真中已有的基于SystemC時態(tài)邏輯屬性驗證方法存在的不足，改進了動態(tài)仿真中時態(tài)邏輯屬性描述方法，并在此基礎(chǔ)上提出了一種屬性化簡方案，提高了仿真性能；另一方面實現(xiàn)了SystemC電路的可達性分析，及基于可達性分析的時態(tài)邏輯屬性驗證算法，并通過實

3、驗證實了文中提出的屬性驗證方法的有效性。本文的主要貢獻如下： 1．從動態(tài)仿真的角度來驗證時態(tài)邏輯屬性，本文在R．Dechsler等人提出的基于SystemC屬性檢查器驗證方法的基礎(chǔ)上進一步研究，分析了已有屬性描述方法的不足，提出了一種改進的屬性化簡的描述方法，并通過實驗驗證了改進方案的有效性。 2．從可達性分析的角度來驗證時序電路的時態(tài)邏輯屬性，針對基于SystemC描述的門級電路，提出了時序電路可達性分析的實現(xiàn)方案。主

4、要包括門級時序電路信息提取方法和時序狀態(tài)轉(zhuǎn)移函數(shù)構(gòu)建方法的實現(xiàn)，其中時序狀態(tài)轉(zhuǎn)移函數(shù)通過bdd來構(gòu)造，然后通過對狀態(tài)轉(zhuǎn)移函數(shù)的bdd表示進行求解來獲取狀態(tài)間的轉(zhuǎn)移關(guān)系。最后通過4個基本時序電路實例來說明可達性分析方案的可行性。 3．在可達性分析的基礎(chǔ)上，進一步驗證時序電路的時態(tài)邏輯屬性。時態(tài)邏輯屬性仍然采取前面提到的動態(tài)仿真方法中屬性描述方法。結(jié)合屬性描述方法，提出了一種時態(tài)屬性驗證方案并實現(xiàn)了該算法，并將該屬性驗證算法應(yīng)用于基