FPGA組合邏輯程序的Petri網建模方法

陳瓏，黃穎坤，羅繼亮

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

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

1 基礎知識

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

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

1.2 Petri網［15－16］

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

2 組合邏輯程序的Petri網設計

針對組合邏輯電路的VHDL程序，程序實體中是一系列邏輯表達式，輸入量和輸出量抽象為不同的系統狀態.控制變量值的變化抽象為一個事件，以變量間的邏輯關系為研究對象，考慮電路零延遲情況下，FPGA組合邏輯程序的Petri網建模方法.

算法1從FPGA組合邏輯程序到普通Petri網的轉換算法

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

輸出：Petri網（N，m0）

步驟1在程序實體中找出輸入量X1，X2，…，Xn（n∈N＋）和輸出量Y1，Y2，…，Ym（m∈N＋），從結構體的描述語句中確定變量間的邏輯函數表達式為

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

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

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

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

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

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

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

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

步驟9根據式（4）得出：Y1從當前狀態值“0”變為下一個狀態值“1”（即當前托肯在狀態庫所中轉移到庫所中時）需要項，又存在G個變遷用雙向弧把每項Φg（X1，X2，…，Xn）（1≤g≤G）中所涉及的輸入量的狀態庫所與對應的變遷：相連.

步驟10根據式（7）得出：Y′1從當前狀態值“0”變為下一個狀態值“1”（即當前托肯在狀態庫所中轉移到庫所中時）需要項又存在L個變遷用雙向弧把每項ψl（X1，X2，…，Xn）（1≤l≤L）中所涉及的輸入量的庫所與變遷相連接.

3 FPGA組合邏輯系統的狀態可達圖

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

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

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

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

算法2FPGA組合邏輯系統狀態可達圖生成算法如下.

輸入：程序的Petri網系統

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

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

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

步驟3若未計算的系統狀態集合Mnew≠?，則繼續以下操作；否則算法結束，輸出GFPGA＝〈M，E，W〉.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

步驟6.3未計算的系統狀態集合Mnew＝Mnew－｛m｝，并返回步驟3.

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

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

4 實例分析

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

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

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

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

部分狀態標識為

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

圖4 反應釜控制系統的Petri網模型的狀態可達圖Fig.4 State reachable graph of Petri net model for the reactor control system

5 結束語

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

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

［2］楊海鋼，孫嘉斌，王慰.FPGA器件設計技術發展綜述［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網仿真分析［J］.系統仿真學報，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網的邏輯電路仿真模型設計［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］藩松，黃繼業.EDA技術與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.