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

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

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

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

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