陳瓏，黃穎坤，羅繼亮

（華僑大學 信息科學與工程學院，福建 廈門361021）

現(xiàn)場可編程門陣列（field－programmable gate array，F(xiàn)PGA）是一種可編程使用的信號處理器件［1］.FPGA具有靈活性強、時序控制能力強、開發(fā)周期短和產(chǎn)品上市速度快等優(yōu)勢［2］，廣泛應用于通信、軍事、醫(yī)療和工業(yè)控制等重要領(lǐng)域.然而，F(xiàn)PGA數(shù)字系統(tǒng)的分析和設(shè)計復雜性隨系統(tǒng)規(guī)模指數(shù)級增長，傳統(tǒng)的測試方法難以保證程序的正確性和可靠性，而形式化驗證能夠枚舉驗證每一個狀態(tài)，因此獲得了廣泛關(guān)注［3－5］，形式化驗證的前提是形式化建模方法.FPGA系統(tǒng)可以抽象為離散事件系統(tǒng)，Petri網(wǎng)是一種描述離散事件系統(tǒng)的數(shù)學模型，較自動機而言，它能夠刻畫系統(tǒng)的結(jié)構(gòu)信息，具有更高的建模效率.因此，F(xiàn)PGA的Petri網(wǎng)建模方法具有重要研究價值.FPGA的描述語言VHDL（very－h(huán)igh－speed integrated circuit hardware description language）的形式化建模分析主要分為兩個方面：一是利用擴展Petri網(wǎng)［6－7］和有色Petri網(wǎng)［8－10］對FPGA系統(tǒng)進行建模，這些擴展是針對某一特定的應用，適用范圍比較窄，不具有一般性，并且基于一種Petri網(wǎng)模型的分析方法不能應用到另一種模型上去；二是用變遷描述VHDL中的執(zhí)行語句，庫所表示語句的執(zhí)行狀態(tài)，通過托肯的遷移揭示語句的執(zhí)行過程［11－13］，這些模型是對程序的整體概況描述，分析能力比較差而且無法揭示變量間的邏輯關(guān)系.為此，本文提出了一種將描述FPGA組合邏輯電路的VHDL程序轉(zhuǎn)換為普通Petri網(wǎng)的算法.

1 基礎(chǔ)知識

1.1 描述組合邏輯電路的VHDL程序

電路的VHDL描述由兩大部分組成［14］：1）以關(guān)鍵字entity引導，end entity e＿name結(jié)尾的語句部分，稱為VHDL的實體，實體描述了電路器件的外部情況及各信號端口的基本性質(zhì)，如信號流動方向、流動在其上的數(shù)據(jù)類型等；2）以關(guān)鍵字architecture引導，end architecture a＿name結(jié)尾的語句部分，稱為VHDL的結(jié)構(gòu)體，結(jié)構(gòu)體描述電路器件的內(nèi)部邏輯功能和電路結(jié)構(gòu).

1.2 Petri網(wǎng)［15－16］

普通Petri網(wǎng)是三元組，即N＝（P，T，F(xiàn)），其中，P為狀態(tài)庫所集合，T為變遷集合，F(xiàn)?（P×T）∪（T×P）表示庫所與變遷之間有向弧的集合.Petri網(wǎng)系統(tǒng)是（N，m0），其中，m0是初始標識.標識是一個向量m∶P→｛0，1，2，…｝，其中，第i維上的分量記作m（Pi），表示狀態(tài)庫所Pi的標識.

2 組合邏輯程序的Petri網(wǎng)設(shè)計

針對組合邏輯電路的VHDL程序，程序?qū)嶓w中是一系列邏輯表達式，輸入量和輸出量抽象為不同的系統(tǒng)狀態(tài).控制變量值的變化抽象為一個事件，以變量間的邏輯關(guān)系為研究對象，考慮電路零延遲情況下，F(xiàn)PGA組合邏輯程序的Petri網(wǎng)建模方法.

算法1從FPGA組合邏輯程序到普通Petri網(wǎng)的轉(zhuǎn)換算法

輸入：組合邏輯電路VHDL程序

輸出：Petri網(wǎng)（N，m0）

步驟1在程序?qū)嶓w中找出輸入量X1，X2，…，Xn（n∈N＋）和輸出量Y1，Y2，…，Ym（m∈N＋），從結(jié)構(gòu)體的描述語句中確定變量間的邏輯函數(shù)表達式為

為了敘述簡便，以下只以一個邏輯輸出表達式進行說明，即

步驟2通過公式法或卡諾圖法對式（2）進行化簡得到

步驟3對式（3）進行邏輯運算得到

步驟4對式（3）兩邊同時取非得到

步驟5對式（5）進行化簡得到

步驟6對式（6）進行邏輯運算得到

步驟7分別用一對庫所表示每個輸入量Xj（1≤j≤n）的“0”和“1”兩種狀態(tài)；并在每對庫所（PXj0，PXj1）（1≤j≤n）之間分別加上兩個變遷ts＋和ts－（1≤s≤n），有向弧集合F＝

步驟8用一對庫所表示輸出量Y1的“0”和“1”兩種狀態(tài)，并在庫所之間加入兩個變遷和，有向弧集合

步驟9根據(jù)式（4）得出：Y1從當前狀態(tài)值“0”變?yōu)橄乱粋€狀態(tài)值“1”（即當前托肯在狀態(tài)庫所中轉(zhuǎn)移到庫所中時）需要項，又存在G個變遷用雙向弧把每項Φg（X1，X2，…，Xn）（1≤g≤G）中所涉及的輸入量的狀態(tài)庫所與對應的變遷：相連.

步驟10根據(jù)式（7）得出：Y′1從當前狀態(tài)值“0”變?yōu)橄乱粋€狀態(tài)值“1”（即當前托肯在狀態(tài)庫所中轉(zhuǎn)移到庫所中時）需要項又存在L個變遷用雙向弧把每項ψl（X1，X2，…，Xn）（1≤l≤L）中所涉及的輸入量的庫所與變遷相連接.

3 FPGA組合邏輯系統(tǒng)的狀態(tài)可達圖

系統(tǒng)程序的Petri網(wǎng)模型已經(jīng)建立，Petri網(wǎng)的動態(tài)行為有效模擬了FPGA系統(tǒng)行為，揭示了變量間的邏輯關(guān)系.因此，利用Petri網(wǎng)的可達圖分析法可以進一步分析程序的運行，便于計算機枚舉驗證每個狀態(tài).但是，Petri網(wǎng)描述的是一個比FPGA系統(tǒng)更復雜的并發(fā)系統(tǒng)，理論上只要變遷滿足使能條件就能被激發(fā)，這樣就會生成很多無關(guān)狀態(tài).為了避免這樣的問題，算法2提出了一種可以等價描述FPGA組合邏輯系統(tǒng)運行過程的狀態(tài)可達圖的計算方法.

定義1假設(shè)Petri網(wǎng)系統(tǒng)（N，m0）是一個FPGA組合邏輯程序的Petri模型，其中，T＝Tin∪Tout，Te，in?Tin，Te，out?Tout，Tin和Tout分別是輸入和輸出變遷集合，Te，in和Te，out分別是可使能的輸入和輸出變遷集合.

定義2假設(shè)三元組GFPGA＝〈M，E，W〉是FPGA組合邏輯系統(tǒng)狀態(tài)可達圖，其中，M＝Min∪Mout，E＝Ein∪Eout.

集合M中的每個節(jié)點對應系統(tǒng)的一個狀態(tài).其中：Min是以實線圈表示節(jié)點的輸入狀態(tài)（由激發(fā)輸入變遷得到的狀態(tài)）集合；Mout是以虛線圈表示節(jié)點的門級輸出狀態(tài)（由激發(fā)輸出變遷得到的狀態(tài)）集合；E是狀態(tài)節(jié)點間的有向邊集合；Ein是標有輸入變遷的實線有向邊集合；Eout是標有輸出變遷的虛線有向邊集合；W是集合E到T的一個映射，即每條有向邊上的變遷標記的集合.

算法2FPGA組合邏輯系統(tǒng)狀態(tài)可達圖生成算法如下.

輸入：程序的Petri網(wǎng)系統(tǒng)

輸出：GFPGA＝〈M，E，W〉，M＝Min∪Mout，E＝Ein∪Eout

步驟1令Mnew＝?，Mold＝?，E＝?，W＝?.

步驟2將初始狀態(tài)m0標記為“new”，并將｛m0｝→Mnew.

步驟3若未計算的系統(tǒng)狀態(tài)集合Mnew≠?，則繼續(xù)以下操作；否則算法結(jié)束，輸出GFPGA＝〈M，E，W〉.

綜上所述，引導式護理能有效改善MHD患者疾病認知程度、自護能力、自我效能感、生活質(zhì)量及管理能力，并減輕其照護家屬心理負擔，明顯降低MHD相關(guān)并發(fā)癥發(fā)生率。

步驟4從集合Mnew中任取一個標記為“new”的狀態(tài)m.

步驟4.1若狀態(tài)m與可達圖已有的其他狀態(tài)相同，將其標記為“old”，則已計算獲得的系統(tǒng)狀態(tài)集合Mold＝Mold∪｛m｝，然后轉(zhuǎn)向步驟4；若狀態(tài)m與可達圖已有的其他狀態(tài)不相同，則進行以下操作.

步驟4.2如果在狀態(tài)m下，沒有使能的輸入變遷和輸出變遷，則將m標記為“dead end”，然后轉(zhuǎn)向步驟4.如果在狀態(tài)m下存在使能變遷，此時會有兩種情況：一種是存在使能的輸入變遷且有使能的輸出變遷，則跳轉(zhuǎn)到步驟5；另一種是只存在使能的輸入變遷，則跳轉(zhuǎn)到步驟6.

步驟5只要可使能的輸出變遷集合Te，out＝｛tout｜m［tout〉｝≠?，tout∈Tout，就要優(yōu)先激發(fā)所有可使能的輸出變遷，生成門級輸出狀態(tài).

步驟5.1從集合Te，out中任取一個輸出變遷tout，激發(fā)該變遷，生成輸出狀態(tài)m′out.

步驟5.2將｛m′out｝→Mout，如果輸出狀態(tài)m′out與可達圖中已有的狀態(tài)相同，則Mout＝Mout∪｛m′out｝；否則，從狀態(tài)m到輸出狀態(tài)m′out之間畫一條虛線有向邊，則集合Eout＝Eout＋｛〈m，m′out〉｝；并在該虛線上標記輸出變遷tout，則有向邊上的變遷集合為｛W（〈m，m′out〉）＝tout｝→W，說明在狀態(tài)m下通過激發(fā)輸出變遷tout會生成輸出狀態(tài)m′out.

步驟5.4因為標記為“new”的狀態(tài)m是從集合Mnew中取出的，所以集合Mnew＝Mnew－｛m｝，并返回步驟3.

步驟6當狀態(tài)m下只存在使能的輸入變遷，即Te，in＝｛tin｜m［tin〉｝≠?，tin∈Tin，則繼續(xù)激發(fā)一個使能的輸入變遷，來改變輸入狀態(tài).

步驟6.1從集合Te，in中任取一個輸入變遷tin，激發(fā)該變遷，生成輸入狀態(tài)m′in.

步驟6.2將｛m′in｝→Min，如果m′in與可達圖中已有的狀態(tài)相同，則集合Mold＝Mold∪｛m′in｝；否則從狀態(tài)m到m′in之間畫一條實線有向邊，則集合為Ein＝Ein＋｛〈m，m′in〉｝；在該實線上標記輸入變遷tin，則有向邊上的變遷集合為｛W（〈m，m′in〉）＝tin｝→W，說明在狀態(tài)m下，通過激發(fā)輸入變遷tin會生成輸入狀態(tài)m′in.

步驟6.2.1判斷輸入狀態(tài)m′in下是否存在可使能的輸出變遷，如果m′in下存在可使能的輸出變遷，則跳轉(zhuǎn)到步驟6.2.2；否則，跳轉(zhuǎn)到步驟6.2.5.

步驟6.2.2在集合Te，out＝｛tout｜m′out［tout〉｝≠?，tout∈Tout中任取一個輸出變遷tout，激發(fā)該變遷，生成輸出狀態(tài)m″out.

步驟6.2.3將｛m″out｝→Mout，如果m″out與可達圖中已有的狀態(tài)相同，則集合Mold＝Mold∪｛m″out｝；否則，從狀態(tài)m′in到m″out之間畫一條虛線有向邊，則集合為Eout＝Eout＋｛〈m′in，m″out〉｝；在該虛線上標記輸出變遷tout，則集合為｛W（〈m′in，m″out〉）＝tout｝→W，說明在輸入狀態(tài)m′in下，通過激發(fā)輸出變遷tout會生成輸出狀態(tài)m″out.

步驟6.2.4集合Te，out＝Te，out－｛tout｝.判斷輸入狀態(tài)m′in下的集合Te，out是否為空集，如果可集合Te，out≠?，即存在使能的輸出變遷，那么返回步驟6.2.2；如果集合Te，out＝?，即不存在使能的輸出變遷，則繼續(xù)以下操作.

步驟6.2.5因為在狀態(tài)m下從集合Te，in中取走了一個使能輸入變遷tin，所以Te，in＝Te，in－｛tin｝.判斷集合Te，in是否為空集，如果集合Te，in≠?，即存在使能的輸入變遷，那么返回步驟6.1；如果集合Te，in＝?，即不存在使能的輸入變遷，則繼續(xù)以下操作.

步驟6.3未計算的系統(tǒng)狀態(tài)集合Mnew＝Mnew－｛m｝，并返回步驟3.

在算法2中，〈m，m′out〉表示從狀態(tài)m指向m′out的一條有向邊，W（〈m，m′out〉）＝tout表示在狀態(tài)m下通過激發(fā)變遷tout得到m′out.Mnew是未計算的狀態(tài)集合，Mold是已計算獲得的狀態(tài)集合.當Mnew中某個可達狀態(tài)被計算獲得，則將其從Mnew中剔除并添加到Mold中，直至Mnew為空集，算法結(jié)束.

根據(jù)算法2可知：在某個電路狀態(tài)下，如果同時存在使能的輸入變遷和輸出變遷，應當優(yōu)先激發(fā)該電路狀態(tài)下所有的輸出變遷，得到一個穩(wěn)定的門級輸出狀態(tài)；如果在某個電路狀態(tài)下，只存在使能的輸入變遷，則激發(fā)一個輸入變遷，得到一個穩(wěn)定的輸入狀態(tài)，通過改變輸入量的取值，再判斷該輸入狀態(tài)下是否存在使能的輸出變遷.

4 實例分析

某化工原料生產(chǎn)反應釜，如圖1所示.系統(tǒng)啟動后，當液位低于S1，V1打開，注入原料A；當液位到達S1，V1關(guān)閉，同時打開V2閥，注入原料B；當液位到達S2，V2關(guān)閉，啟動M加熱；當溫度值到達S3，M停止加熱，同時打開V3閥，并且L啟動計時；一段時間后，定時器L關(guān)閉，V3關(guān)閉，系統(tǒng)回到最初狀態(tài).根據(jù)系統(tǒng)要求，某程序員給出圖1所示反應釜控制系統(tǒng)的部分VHDL程序，如圖2所示.

圖1 某化工原料生產(chǎn)反應釜 Fig.1 A chemical raw materials production reactor

圖2 反應釜控制系統(tǒng)的部分VHDL程序Fig.2 A part of VHDL program of the reactor

根據(jù)算法1，針對圖2的反應釜控制系統(tǒng)程序，首先將程序中的每個變量分別用一對庫所表示，抽象為運行（on）和休息（off）狀態(tài)，即邏輯上表示“1”和“0”兩個狀態(tài)；其次在輸入變量的庫所間加上輸入變遷，在輸出變量的庫所間加上輸出變遷；然后根據(jù)邏輯表達式所描述的輸出量與輸入量間的邏輯關(guān)系，描述出輸入量庫所與輸出變遷間的控制關(guān)系；最后由算法1，將圖2的系統(tǒng)程序轉(zhuǎn)換為圖3的Petri網(wǎng)模型.根據(jù)算法2，由反應釜控制系統(tǒng)的Petri網(wǎng)模型，從某個初始狀態(tài)開始，分別計算出每個輸入狀態(tài)下所對應的穩(wěn)定的輸出狀態(tài)，得到如圖4所示的系統(tǒng)狀態(tài)可達圖.由圖4分析可知：系統(tǒng)具有可逆性和活性，其中每個狀態(tài)的表現(xiàn)形式為

部分狀態(tài)標識為

圖3 反應釜控制系統(tǒng)的Petri模型 Fig.3 Petri net model of the reactor control system

圖4 反應釜控制系統(tǒng)的Petri網(wǎng)模型的狀態(tài)可達圖Fig.4 State reachable graph of Petri net model for the reactor control system

5 結(jié)束語

提出了一個完整的將FPGA組合邏輯程序自動轉(zhuǎn)換為普通Petri網(wǎng)的方法，與現(xiàn)有基于擴展Petri網(wǎng)的建模方法相比，文中基于普通Petri網(wǎng)的建模方法更具一般性，應用范圍更廣，對于系統(tǒng)變量間的邏輯功能關(guān)系有更強的分析能力.另外，在考慮電路零延遲的情況下，根據(jù)已建好的程序Petri網(wǎng)模型，通過定義新的變遷激發(fā)規(guī)則，建立一個可以等價描述FPGA組合邏輯系統(tǒng)運行過程的狀態(tài)空間，去掉一些無關(guān)的中間狀態(tài)，指數(shù)級地壓縮狀態(tài)空間，為后續(xù)的形式化驗證［17－18］提高效率.后續(xù)工作將利用計算機通過系統(tǒng)狀態(tài)可達圖對程序進行形式化驗證，檢測存在邏輯錯誤的系統(tǒng)程序.

［1］王芯，孫富明，李磊，等.FPGA設(shè)計安全性綜述［J］.小型微型計算機系統(tǒng)，2010，31（7）：1333－1335.

［2］楊海鋼，孫嘉斌，王慰.FPGA器件設(shè)計技術(shù)發(fā)展綜述［J］.電子與信息學報，2010，32（3）：716－718.

［3］王彥本.集成電路形式化驗證方法研究［J］.電子科技，2008，21（8）：4－7.

［4］GHARBI A，KHALGUI M，BEN A S，et al.Optimal model checking of safe control embedded software components［C］∥15th Conference on Emerging Technologies and Factory Automation.Bilbao：IEEE Press，2010：1－8.

［5］PATIL S，VYATKIN V，SOROURI M，et al.Formal verification of intelligent mechatronic systems with decentralized control logic［C］∥17th Conference on ETFA.Krakow：IEEE Press，2012：1－7.

［6］古天龍.組合邏輯電路的Petri網(wǎng)仿真分析［J］.系統(tǒng)仿真學報，1994，6（2）：32－36.

［7］TSAI J I，TENG C C，LEE C H.Test generation and site of fault for combinational circuits using logic Petri－nets［C］∥International Conference on Systems Man and Cybernetics.Taipei：IEEE Press，2006：8－11.

［8］歐陽星明，胡青海.基于有色Petri網(wǎng)的邏輯電路仿真模型設(shè)計［J］.華中科技大學學報：自然科學版，2006，34（3）：18－20.

［9］BUKOWIEC A，ADAMSKI M.Synthesis of Petri nets into FPGA with operation flexible memories［C］∥15th International Symposium on Design and Diagnostics of Electronic Circuits and Systems.Tallinn：IEEE Press，2012：16－21.

［10］KOKASH N，ARBAB F.Formal design and verification of long－running transactions with extensible coordination tools［J］.IEEE Transactions on Services Computing，2013，6（2）：186－200.

［11］OLCOZ S，COLOM J M.A Petri net approach for the analysis of VHDL descriptions［M］.Berlin Heidelberg：Springer，1993：15－26.

［12］WALTER D，LITTLE S，SEEGMILLER N，et al.Symbolic model checking of analog／mixed－signal circuits［C］∥Asia and South Pacific Design Automation Conference.Yokohama：IEEE Press，2007：316－323.

［13］MOUTINHO F，GOMES L.State space generation algorithm for gals systems modeled by IOPT Petri nets［C］∥37th Annual Conference on Industrial Electronics Society.Melbourne，VIC：IEEE Press，2011：7－10.

［14］藩松，黃繼業(yè).EDA技術(shù)與VHDL［M］.北京：清華大學出版社，2009：42－47.

［15］LUO Ji－liang，NONAMI K.Approach for transforming linear constraints on Petri nets［J］.IEEE Transactions on Automatic Control，2011，56（11）：2751－2765.

［16］DAVID R，ALIA H.Discrete continuous and hybrid Petri nets［M］.Berlin Heidelberg：Springer，2005：24－40.

［17］SCHWARICK M，ROHR C，HEINER M.MARCIE－model checking and reachability analysis done efficiently［C］∥8th Conference on Quantitative Evaluation of Systems.Aachen：IEEE Press，2011：91－100.

［18］KHALGUI M，MOSBAHI O，LI Z W，et al.Reconfigurable multiagent embedded control systems：From modeling to implementation［J］.IEEE Transactions on Computers，2011，60（4）：538－551.