[發(fā)明專利]一種利用圖式標明HPD邏輯可靠性的方法

有效

• 申請?zhí)枺?/td>: 201310627430.1
• 申請日: 2013-11-29
• 公開（公告）號: CN103729289A
• 公開（公告）日: 2014-04-16
• 發(fā)明（設(shè)計）人: 秦宇;高玉斌;袁勁濤;張亞棟;趙云飛
• 申請（專利權(quán)）人: 北京廣利核系統(tǒng)工程有限公司;中國廣核集團有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京元中知識產(chǎn)權(quán)代理有限責(zé)任公司 11223
• 代理人: 王明霞

技術(shù)領(lǐng)域

本發(fā)明涉及HPD邏輯的驗證技術(shù)領(lǐng)域，特別是針對用Verilog語言描述的邏輯的可靠性驗證。

背景技術(shù)

并發(fā)性是HPD邏輯的主要特點，并發(fā)的HPD邏輯容易出現(xiàn)競爭、死鎖等不確定性問題，例如同時訪問同一個資源、進程阻塞或某個狀態(tài)達不到。因此，HPD邏輯的可靠性驗證首先需要關(guān)注其并發(fā)性，然后驗證由并發(fā)引起的競爭、死鎖等不確定性問題對HPD邏輯的影響。

目前，HPD邏輯的可靠性驗證方法主要有仿真驗證、模型檢測（形式化驗證）和動態(tài)故障樹分析驗證。仿真一直是HPD邏輯可靠性驗證的主要手段，仿真驗證的目標是盡可能覆蓋所有邏輯功能的語句、分支、表達式和條件等，由于目前的仿真和硬件測試方法的覆蓋率很難滿足核安全級的全面覆蓋的要求，從而難以保證其可靠性。

基于模型檢測的形式化驗證方法利用時態(tài)邏輯來表達HPD的并發(fā)性，在時態(tài)邏輯中，時間并不是顯式地表述，相反，在公式中可能會描述某個指定狀態(tài)最終（eventually）會到達，或者會描述某個錯誤狀態(tài)從不（never）進入。性質(zhì)eventually，never可以用時態(tài)算子說明，這些算子也可以和邏輯連接詞（∨、∧、）結(jié)合在一起或嵌套使用，構(gòu)成更復(fù)雜的時態(tài)邏輯公式來描述并驗證并發(fā)系統(tǒng)的性質(zhì)。動態(tài)故障樹的基礎(chǔ)是布爾類元素和與/或等邏輯門，與HPD邏輯的特性十分相符。動態(tài)故障樹以靜態(tài)故障樹為基礎(chǔ)，引入了動態(tài)邏輯門。動態(tài)故障樹分析方法綜合了故障樹分析方法和馬爾科夫模型兩者的優(yōu)點，并采用二元決策圖法和馬爾可夫過程方法求解，可以獲得HPD邏輯的可靠性情況。動態(tài)故障樹方法主要面向復(fù)雜的實現(xiàn)層面的對象，而不是分布式架構(gòu)。動態(tài)故障樹是一種通用的方法，對高并發(fā)邏輯的描述比較困難。

發(fā)明內(nèi)容

為解決現(xiàn)有技術(shù)主中HPD邏輯的可靠性驗證比較困難的問題，本發(fā)明提供一種利用圖式顯示HPD邏輯功能塊中各元素之間邏輯關(guān)系的方法，具體方案如下：一種利用圖式標明HPD邏輯可靠性的方法，包括由Verilog語言描述的邏輯功能模塊，其特征在于，首先建立一個圖式文件，然后在圖式文件中進行如下操作：

步驟1、將邏輯功能模塊中的所有信號類型用相應(yīng)的信號圖式符號進行表示；

步驟2、將邏輯功能模塊中的阻塞賦值關(guān)系、非阻塞賦值關(guān)系和約束關(guān)系分別用相應(yīng)的關(guān)系圖式符號替換，根據(jù)邏輯功能模塊的輸出來反推各信號類型的連接關(guān)系，然后在圖式文件中從結(jié)尾逐級向上用相應(yīng)的關(guān)系圖式符號對各信號圖式符號進行連接；

步驟3、在連接過程中，出現(xiàn)兩個或兩個以上的下級信號圖式符號與同一個上級信號圖式符號連接的情況時，復(fù)制此上級信號圖式符號并分別與相應(yīng)的下級信號圖式符號建立連接關(guān)系；

步驟4、在相同或不同層級的信號圖式符號出現(xiàn)重復(fù)時，對類型為變量的重復(fù)信號圖式符號用重用圖式符號進行標明，同時建立針對此信號圖式符號的下級連接圖式的連接子圖，連接子圖用帶有對應(yīng)調(diào)用圖式符號的此信號圖式符號標識；

步驟5、建立一個表示最終邏輯輸出的功能信號圖式，然后與圖式文件中涉及到輸出的信號圖式符號連接，得到邏輯功能模塊無閉環(huán)的樹形邏輯關(guān)系圖式。

為獲取信號圖式符號的時序信息：所述信號圖式符號中，當一個關(guān)系圖式符號兩端的信號圖式符號相同時，分別對相應(yīng)的信號圖式符號進行時域標識。

為獲取信號圖式符號的重要度信息：所述信號圖式符號中包含有重要度信息，所述重要度信息根據(jù)各信號圖式符號在圖式文件中的出現(xiàn)次數(shù)、層級和加權(quán)系數(shù)的乘積得到。

為對信號進行針對處理：所述的變量不包括在圖式上結(jié)構(gòu)已知或固定的輸入信號類型、保持信號類型和自運算信號類型。

為簡化圖式文件：當同一個信號圖式符號連接有兩個相同的信號圖式符號時，刪除多余的重復(fù)信號圖式符號僅保留一個。