本發(fā)明屬于核電控制的技術(shù)領(lǐng)域，為了解決現(xiàn)有技術(shù)中綜合后仿真方法和形式化一致性驗(yàn)證方法分別存在的不足，提供一種判定FPGA冗余設(shè)計(jì)的代碼與綜合后電路一致性的方法和系統(tǒng)；所述方法包括：S1、分別檢索FPGA代碼中的第一關(guān)鍵詞和綜合電路對(duì)應(yīng)網(wǎng)表文件中的第二關(guān)鍵詞；S2、判斷FPGA代碼中第一關(guān)鍵詞檢索得到的第一信號(hào)名集合是否屬于網(wǎng)表文件中第二關(guān)鍵詞檢索得到的第二信號(hào)名集合的子集；如果是，則綜合后電路的信號(hào)一致性檢測(cè)通過(guò)；S3、判斷FPGA代碼文件中聲明的所有信號(hào)，在綜合后電路對(duì)應(yīng)網(wǎng)表文件中是否分別都有一個(gè)或多個(gè)有用邏輯單元與相應(yīng)的信號(hào)連接；如果是，則綜合后電路的邏輯一致性檢測(cè)通過(guò)。

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

本發(fā)明涉及核電控制的技術(shù)領(lǐng)域，尤其涉及核電控制系統(tǒng)用現(xiàn)場(chǎng)可編程門(mén)陣列的技術(shù)領(lǐng)域，更具體地，涉及一種判定FPGA冗余設(shè)計(jì)的代碼與綜合后電路一致性的方法和系統(tǒng)。

背景技術(shù)

隨著FPGA(現(xiàn)場(chǎng)可編程門(mén)陣列)技術(shù)在核安全級(jí)儀控系統(tǒng)中的廣泛應(yīng)用，對(duì)FPGA邏輯設(shè)計(jì)的一致性提出很高的要求，特別是為了保證可靠性而對(duì)關(guān)鍵功能進(jìn)行的冗余設(shè)計(jì)，在綜合后的功能一致性日益成為核行業(yè)中重點(diǎn)關(guān)注的問(wèn)題；現(xiàn)有技術(shù)中，常用的分析FPGA冗余設(shè)計(jì)的代碼與綜合后電路功能一致性方法主要包括綜合后仿真方法和形式化一致性驗(yàn)證方法。

綜合后仿真方法是把綜合生成的延時(shí)文件反標(biāo)到綜合仿真模型中，將模擬的測(cè)試激勵(lì)輸入被測(cè)對(duì)象的帶有器件延時(shí)信息的仿真模型中仿真運(yùn)行，通過(guò)比較仿真輸出和預(yù)期輸出的結(jié)果判定綜合后的電路在功能上是否正確；但是由于受到激勵(lì)覆蓋率和仿真成本的約束，只能在一定程度上保證代碼與綜合電路的一致性，不能完全保證，尤其是對(duì)于代碼中的冗余設(shè)計(jì)是否被一致轉(zhuǎn)換為電路問(wèn)題上，通過(guò)綜合后仿真不容易識(shí)別。

形式化一致性驗(yàn)證方法，通過(guò)比較代碼與綜合后電路，識(shí)別代碼與綜合后電路不一致的設(shè)計(jì)，該方法通過(guò)把綜合后電路劃分為一系列的邏輯錐(logic cone)，然后通過(guò)比較點(diǎn)把代碼和綜合后電路的邏輯錐一一對(duì)應(yīng)起來(lái)，再通過(guò)比較相對(duì)應(yīng)的邏輯錐的功能是否一致來(lái)驗(yàn)證代碼和綜合后電路的功能是否一致，如果所有的邏輯錐的功能都是一致的，那么兩個(gè)設(shè)計(jì)就是等價(jià)的；但是由于在綜合過(guò)程中對(duì)電路結(jié)構(gòu)進(jìn)行了改變，使得比較點(diǎn)無(wú)法匹配，而導(dǎo)致比較失敗，需進(jìn)行嚴(yán)格的約束參數(shù)設(shè)置才能比較成功。

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

本發(fā)明為了解決現(xiàn)有技術(shù)中綜合后仿真方法和形式化一致性驗(yàn)證方法分別存在的不足，提供一種判定FPGA冗余設(shè)計(jì)的代碼與綜合后電路一致性的方法和系統(tǒng)，具有覆蓋率高、約束條件少等優(yōu)點(diǎn)。

為了實(shí)現(xiàn)上述效果，本發(fā)明提供的技術(shù)方案包括：

本發(fā)明一方面提供一種判定FPGA冗余設(shè)計(jì)的代碼與綜合后電路一致性的方法，其特征在于，包括：

S1、分別檢索FPGA代碼中的第一關(guān)鍵詞和綜合電路對(duì)應(yīng)網(wǎng)表文件中的第二關(guān)鍵詞；

S2、判斷所述FPGA代碼中第一關(guān)鍵詞檢索得到的第一信號(hào)名集合是否屬于所述網(wǎng)表文件中第二關(guān)鍵詞檢索得到的第二信號(hào)名集合的子集；如果是，則綜合后電路的信號(hào)一致性檢測(cè)通過(guò)；

S3、判斷所述FPGA代碼文件中聲明的所有信號(hào)，在所述綜合后電路對(duì)應(yīng)網(wǎng)表文件中是否分別都有一個(gè)或多個(gè)有用邏輯單元與相應(yīng)的信號(hào)連接；如果是，則綜合后電路的邏輯一致性檢測(cè)通過(guò)；

S4、當(dāng)所述綜合后電路的信號(hào)一致性檢測(cè)和所述綜合后電路的邏輯一致性檢測(cè)都通過(guò)時(shí)，則判定所述FPGA冗余設(shè)計(jì)的代碼與綜合后電路一致性通過(guò)。

本發(fā)明實(shí)施例優(yōu)選地，所述步驟S2還包括：如果所述第一信號(hào)名集合不屬于所述第二信號(hào)名集合的子集，則提示報(bào)警信息，并顯示丟失的信號(hào)名。

本發(fā)明實(shí)施例優(yōu)選地，所述步驟S3包括：如果有一個(gè)或者多個(gè)信號(hào)只連接到IO端口單元時(shí)，提示報(bào)警信息，并顯示信號(hào)和連接信息；如果有一個(gè)或者多個(gè)信號(hào)沒(méi)有連接元件庫(kù)中的任一邏輯單元時(shí)，發(fā)出錯(cuò)誤提醒信息。