【摘要】：隨著多核體系結(jié)構(gòu)的出現(xiàn)和普及,片上總線逐漸成為影響片上系統(tǒng)功能和性能的關(guān)鍵部件.因此,片上總線的驗證成為片上系統(tǒng)設(shè)計中一個重要組成部分.模型檢測作為一種主流的形式化驗證方法,可以自動化窮舉搜索系統(tǒng)行為以決定片上系統(tǒng)的設(shè)計是否滿足設(shè)計規(guī)范.然而,模型檢測受制于狀態(tài)空間爆炸問題,且現(xiàn)有規(guī)范語言如計算樹邏輯和線性時序邏輯等的描述能力有限.提出了一種基于命題投影時序邏輯的WISHBONE片上總線符號模型檢測方法.該方法將以Verilog硬件描述語言實現(xiàn)的WISHBONE總線轉(zhuǎn)化為以NuSMV模型檢測工具的建模語言SMV描述的系統(tǒng)模型,使用命題投影時序邏輯描述WISHBONE總線期望的性質(zhì),通過PLSMC工具驗證系統(tǒng)模型是否滿足期望的性質(zhì).實驗結(jié)果表明該方法能夠有效驗證WISHBONE片上總線的定性性質(zhì),以及時間敏感和迭代性等定量性質(zhì).
[Abstract]:With the emergence and popularization of multi-core architecture, on-chip bus has become a key component affecting the function and performance of on-chip system. Therefore, the verification of on-chip bus becomes an important part in the design of on-chip system. As a mainstream formal verification method, model checking can automate the behavior of search system to determine whether the design of on-chip system meets the design specification or not. However, model detection is constrained by the state space explosion problem, and the existing specification languages, such as computational tree logic and linear temporal logic, have limited description ability. In this paper, a method for detecting the symbol model of WISHBONE on-chip bus based on propositional projection temporal logic is proposed. In this method, the WISHBONE bus realized by Verilog hardware description language is transformed into the system model described by SMV, the modeling language of NuSMV model checking tool, and the expected properties of WISHBONE bus are described by propositional projective temporal logic. The PLSMC tool is used to verify whether the system model meets the desired properties. The experimental results show that this method can effectively verify the qualitative properties of the WISHBONE on-chip bus, as well as the quantitative properties such as time sensitivity and iteration.
【作者單位】： 西安電子科技大學計算理論與技術(shù)研究所;
【基金】：國家“九七三”重點基礎(chǔ)研究發(fā)展計劃基金項目(2010CB328102) 國家自然科學基金項目(61003078,61272117,61133001,61272118,91218301,61322202,61202038)
【分類號】：TP336

【參考文獻】

相關(guān)期刊論文 前3條

1 楊志;馬光勝;張曙;;基于多項式符號代數(shù)方法的高層次數(shù)據(jù)通路的等價驗證[J];計算機研究與發(fā)展;2009年03期

2 張立明;歐陽丹彤;白洪濤;;基于半擴展規(guī)則的定理證明方法[J];計算機研究與發(fā)展;2010年09期

3 逄濤;段振華;劉曉芳;;Verilog程序的命題投影時序邏輯符號模型檢測[J];西安電子科技大學學報;2014年02期

【共引文獻】

相關(guān)期刊論文 前10條

1 朱維軍;鄧淼磊;周清雷;張海賓;;擴展命題區(qū)間時序邏輯公式可滿足性判定算法[J];電子科技大學學報;2011年05期

2 朱維軍;張海賓;周清雷;;離散時間區(qū)間時序邏輯可滿足性的判定[J];電子學報;2010年05期

3 黃羿;馬新強;劉友緣;羅萬成;;時序邏輯的語法語義比較分析[J];重慶文理學院學報(社會科學版);2014年05期

4 朱維軍;周清雷;張海賓;;擴展Tempura語言統(tǒng)一模型檢測算法[J];華南理工大學學報(自然科學版);2011年07期

5 朱維軍;張海賓;周清雷;;命題投影時序邏輯并發(fā)建模與自動驗證[J];華中科技大學學報(自然科學版);2010年08期

6 王小兵;段振華;;時序邏輯程序的模型檢測[J];計算機科學;2009年10期

7 陳建輝;王文義;朱維軍;;一種基于并發(fā)命題投影時序邏輯模型檢測的入侵檢測方法[J];計算機科學;2010年10期

8 朱維軍;翟萍;周清雷;;一種改進的RC(3,7)安全協(xié)議[J];華中科技大學學報(自然科學版);2012年09期

9 門鵬;;基于PPTL的著色Petri網(wǎng)的模型檢測方法[J];科學技術(shù)與工程;2013年05期

10 崔沛東;蔡靜;魏亮;張偉;;GPU加速模擬混合自旋的Ising模型[J];科學技術(shù)與工程;2013年26期

相關(guān)博士學位論文 前10條

1 楊琛;打結(jié)不變的命題投影時序邏輯與模型檢測[D];西安電子科技大學;2010年

2 舒新峰;投影時序邏輯的完備公理系統(tǒng)與形式驗證[D];西安電子科技大學;2010年

3 田聰;命題投影時序邏輯的判定性、復雜性、表達性及模型檢測[D];西安電子科技大學;2010年

4 朱維軍;時間區(qū)間時序邏輯模型檢測：理論、算法及應用[D];西安電子科技大學;2011年

5 張立勇;軟件源代碼安全分析研究[D];西安電子科技大學;2011年

6 王小兵;面向?qū)ο驧SVL語言及其在組合Web服務驗證中的應用[D];西安電子科技大學;2009年

7 楊瀟瀟;框架時序邏輯程序語言MSVL的形式語義[D];西安電子科技大學;2009年

8 張南;命題投影時序邏輯的完備公理系統(tǒng)與形式驗證[D];西安電子科技大學;2012年

9 鐘小梅;基于格值邏輯的α-準鎖語義歸結(jié)自動推理研究[D];西南交通大學;2012年

10 張琛;基于UML2.0模型的測試與驗證方法[D];西安電子科技大學;2012年

相關(guān)碩士學位論文 前6條

1 曾海林;基于SMT約束求解器的Verilog組合電路等價性驗證[D];吉林大學;2012年

2 張培友;基于移動互聯(lián)網(wǎng)的幾何證明系統(tǒng)的研究與實現(xiàn)[D];電子科技大學;2012年

3 莫大鵬;MSVL中異步通信方法的研究與實現(xiàn)[D];西安電子科技大學;2012年

4 郭夏;MSVL建模、仿真與驗證軟件的擴展及其應用[D];西安電子科技大學;2011年

5 張笑星;PPTL模型檢測器的改進及應用[D];西安電子科技大學;2011年

6 楊廣;控制流提取模型及軟件可靠性評價應用研究[D];大連理工大學;2013年

【二級參考文獻】

相關(guān)期刊論文 前10條

1 王海霞,韓承德;整數(shù)乘法電路的形式化驗證方法研究[J];計算機研究與發(fā)展;2005年03期

2 孫吉貴;李瑩;朱興軍;呂帥;;一種新的基于擴展規(guī)則的定理證明算法[J];計算機研究與發(fā)展;2009年01期

3 賴永;歐陽丹彤;蔡敦波;呂帥;;基于擴展規(guī)則的模型計數(shù)與智能規(guī)劃方法[J];計算機研究與發(fā)展;2009年03期

4 鄧澍軍;吳為民;邊計年;;RTL驗證中的混合可滿足性求解[J];計算機輔助設(shè)計與圖形學學報;2007年03期

5 王湘浩,劉敘華;廣義歸結(jié)[J];計算機學報;1982年02期

6 李光輝,李曉維;基于增量可滿足性的等價性檢驗方法[J];計算機學報;2004年10期

7 孫吉貴，劉敘華;模態(tài)歸結(jié)弱包含刪除策略[J];計算機學報;1994年05期

8 孫吉貴，劉敘華;Cialdea一階模態(tài)歸結(jié)系統(tǒng)的不完備性及其改進[J];計算機學報;1995年06期

9 孫吉貴,劉敘華;廣義線性半鎖歸結(jié)[J];科學通報;1992年19期

10 舒新峰;段振華;;投影時序邏輯的公理系統(tǒng)與形式驗證[J];西安電子科技大學學報;2009年04期

【相似文獻】

相關(guān)期刊論文 前10條

1 張振,楊羽,張溯,胡永華;一種基于PVCI的總線封裝設(shè)計[J];微處理機;2004年06期

2 黃清泉;洪沙;吳垣甫;;主從式片上總線系統(tǒng)交易級的實現(xiàn)[J];計算機工程;2008年22期

3 黃以華;凌國俊;廖世文;劉燕林;張健，

本文編號：2425613