陳成官,張小軍,周韜略,張德學,郭 華
(山東科技大學電子信息工程學院,山東 青島266590)
Petri 網(wǎng)(Petri Net,PN)是一種適合于描述異步、并發(fā)、分布式系統(tǒng)的抽象描述方式,可用圖形表示法和代數(shù)表示法分別表示,具有直觀性[1]。 由于這些特點,Petri 網(wǎng)的理論得以快速發(fā)展和應用,其中有色Petri 網(wǎng)(Colored Petri Net,CPN)已經(jīng)被廣泛用于系統(tǒng)仿真與驗證[2-4]、工作流分析[5-7]、性能分析[8-9]與算法錯誤檢測[10-11]等工作中。 對于PN 工具的設計與開發(fā),目前已經(jīng)取得了許多研究成果[12]。 但是,這些項目主要集中于通用計算機系統(tǒng)下對P/T 網(wǎng)(庫所/變遷網(wǎng))進行的建模及模型的仿真驗證;并且在通用計算機系統(tǒng)上,存在模擬PN 并發(fā)性低效與仿真速度慢的問題。
現(xiàn)場可編程門陣列(FPGA)提供了一種新的建模方法。 FPGA 與通用計算機系統(tǒng)相比具有速度快、可重構和能效比高的優(yōu)勢,并且可直接描述Petri 網(wǎng)異步并發(fā)的特性。 隨著Petri 網(wǎng)規(guī)模的擴大與復雜度的增加,F(xiàn)PGA 的速度優(yōu)勢會越來越明顯。目前對基于FPGA 的PN 仿真系統(tǒng)的研究較少,且大多數(shù)涉及Petri 網(wǎng)的研究,都是以Petri 網(wǎng)在實際問題的應用研究為導向的,例如,Petri 網(wǎng)在邏輯控制器設計與離散事件系統(tǒng)監(jiān)控理論中的應用[13];并且現(xiàn)有的基于FPGA 的PN 實現(xiàn)方法不支持CPN 的仿真[14-15]。
本文實現(xiàn)基于FPGA 的CPN 仿真系統(tǒng)解決了兩個問題:CPN 的硬件架構設計、CPN 硬件模型的自動生成。 由于CPN 的一般定義與描述特別抽象,使得無法直接利用已有描述自動生成硬件模型,因此本文設計了“CPN 描述文檔”的內(nèi)容及格式,并實現(xiàn)了CPN 硬件模型的自動生成工具,該工具根據(jù)“CPN 描述文檔”自動生成相應CPN 模型與仿真控制器的Verilog 代碼描述。 系統(tǒng)設計與驗證方案如圖1 所示,在已知CPN 模型的基礎上,將CPN 用“CPN 描述文檔”進行描述,通過自動生成工具生成Verilog 代碼描述;經(jīng)過RTL 級仿真驗證后,建立Quartus 工 程, 經(jīng) 過 編 譯, 在 Altera Cyclone V 5CSEMA5F31C6N FPGA 平臺上運行測試。
圖1 設計與驗證方案
本文內(nèi)容安排如下:首先介紹了CPN 的基本概念與定義,并設計了CPN 描述文件的內(nèi)容格式與結構,然后制定了CPN 元素到Verilog 描述的映射規(guī)則,給出了自動生成工具的程序流程,最后結合實例進行了運行測試。
每個PN 都由三部分組成:表征狀態(tài)的庫所、表征動作的變遷以及表征流關系的有向弧。 庫所用于存儲托肯(token);流關系是權向量,方向與有向弧相同,其大小是權值,變遷的發(fā)生通過權值對庫所產(chǎn)生影響。 在CPN 中,每個庫所中可包含多種顏色的token;每個變遷可存在多種激活條件,稱為變遷的發(fā)生顏色;每個有向弧可包含多個流關系,每個流關系又對應變遷的一種或多種發(fā)生顏色。
一個經(jīng)典CPN 可定義為一個9 元組N =〈P,T,A,Σ,V,C,G,E,I〉[16-17]。 其中:
· P 是庫所的有窮集合,在圖形表示法中,每個庫所用一個圓形(○)表示;
· T 是變遷的有窮集合,在圖形表示法中,每個變遷用一個矩形(□)表示;
· A?P×T∪T×P 是一個有限的“有向弧”集合,用單向箭頭(→)表示一個有向弧,Petri 網(wǎng)中用有向弧表征變遷與庫所之間的流關系;
· Σ 是一個非空有限的顏色集的集合,集合元素是顏色集;
· V 是變量的集合,?v∈V,Type[v]∈Σ,變量的類型由顏色集限定,Type[a]表示a 的類型;
· C 是庫所的顏色集函數(shù),每個庫所與Σ 中的一個顏色集對應,庫所中token 的顏色與顏色集中的元素一一對應;
· G 是從變遷T 到變量表達式集EXPRV的映射函數(shù),表征變遷的發(fā)生受到變量表達式的約束,?expression∈EXPRV,Type[expression]∈Σ;
· E 是從弧A 到變量表達式集EXPRV的映射函數(shù);每個“有向弧”由一個變量表達式限定流關系,通常,變量表達式的所有取值對應該弧表示的所有流關系,?a∈A,Type[E(a)]=C(p),庫所p 與弧a 相連;
· I 是CPN 的初始化函數(shù),為CPN 中每個庫所分配一個初始化表達式及該表達式對應token 的數(shù)量,?p∈P,Type[I(p)]=C(p)。
CPN 與一般P/T 網(wǎng)不同,其復雜的流關系無法使用單一前后關聯(lián)矩陣表示。 為了描述CPN 中的流關系,本文提出了“庫所的全局關聯(lián)矩陣W”概念。為庫所Pn定義一個描述其與變遷的流關系的矩陣:
Wn=NCT-MAX×NT(1)
式中:n∈[1,NP],NP是CPN 中庫所的數(shù)量;列數(shù)NT是變遷的數(shù)量;行數(shù)NCT-MAX是單個變遷發(fā)生顏色數(shù)量的最大值。 矩陣Wn中的每一項用常數(shù)“0”表示顏色C(p)下變遷發(fā)生對庫所p 沒有影響,常數(shù)“1”表示顏色C(p)下變遷發(fā)生會導致該庫所中一種或幾種顏色的token 的數(shù)量增加,常數(shù)“-1”表示顏色C(p)下變遷發(fā)生會導致該庫所中一種或幾種顏色的token 的數(shù)量減少,常數(shù)“2”表示顏色C(p)下變遷發(fā)生會導致使該庫所中一種或幾種顏色的token 的數(shù)量增加的同時使該庫所中token 減少。
為增強CPN 描述文檔的可讀性,并清晰地描述變遷與庫所間的流關系,本文將庫所的全局關聯(lián)矩陣W 拆成前向Wpre與后向Wpost兩個矩陣進行描述,前向表征有向弧從變遷指向庫所,后向表征有向弧從庫所指向變遷。 將W 中所有“-1”項置為0,“2”項置為1 得到Wpre;將W 中所有“1”項置為0,“2”項置為-1 得到Wpost。 描述文檔包括7 個部分:
(1)庫所與變遷的個數(shù)描述:
(2)變遷發(fā)生顏色的個數(shù)描述:
(4)Pre 描述:
定義表示流關系(權向量)的基本元素為字符串“顏色標識符:權值”,顏色標識符是流關系對應庫所token 的顏色,權值表示此流關系發(fā)生時對相應顏色token 數(shù)量的影響;將Wpre的每一項用基本元素表示,不同項之間用空格隔開,同一項內(nèi)的不同流關系之間用“+”連接;如,Wpre的“0”項用“0:0”替換,“1”項用“sand:2+cement:1”替換;得到Wspre。描述格式如下:
圖2 給出了CPN 的Verilog 模塊的映射架構設計,共4 種模塊:頂層模塊、控制器模塊、庫所模塊、變遷模塊;通過模塊中的判斷、判決與更新邏輯實現(xiàn)CPN 的狀態(tài)更新;reg 存儲庫所的token 數(shù)。
上述描述中,NP是庫所的個數(shù),NT是變遷的個數(shù);NCTi是變遷i 發(fā)生顏色的個數(shù);NCPj是庫所j 包含token 的顏色的個數(shù);L 是庫所對該顏色token 的最大容量;M 是在CPN 的初始狀態(tài)下庫所中該顏色token 的數(shù)量。
本文將CPN 狀態(tài)的更新分成3 步:變遷的預激活、變遷的激活與庫所token 的更新,每一步消耗一個時鐘完成。 變遷的預激活是根據(jù)庫所中當前token 數(shù)判斷滿足激活條件的變遷;在變遷的激活階段對滿足激活條件的變遷進行沖突的判斷,并激活符合條件的變遷;在庫所token 的更新階段,根據(jù)激活的變遷更新庫所中token 的數(shù)量,實現(xiàn)一次CPN狀態(tài)的更新。
表1 描述了從CPN 描述到Verilog 描述的映射規(guī)則。 在Verilog 設計中,將庫所和變遷分別定義為一個module 模塊;將token 定義為庫所模塊中的output reg 類型的變量,位寬由庫所的token 容限描述確定;在CPN 頂層模塊中,為描述文檔的Pre/Post描述中每個基本元素定義一個wire,連接庫所模塊與變遷模塊,并將權值定義為庫所模塊中的parameter 參量。
表1 映射
圖2 映射架構設計
自動生成工具的工作流程如圖3 所示,主要包括描述文件讀取、參數(shù)分析、Verilog 描述文件打印和測試文件打印4 個部分。 測試文件包括用于RTL仿真的testbench 文件和用于Verilog 編譯的自動綜合腳本。 參數(shù)分析過程會生成分析文件,可用于檢驗讀取文件得到的CPN 參數(shù)的正確性。
圖3 工作流程
本文選用一個描述通信中“包傳輸”的CPN 模型[18]作為測試案例,如圖4 所示,其顏色集和變量如表2 所示。 模型可以分為3 個部分:Sender、Network 和Receiver。 庫所Send 存儲要發(fā)送的字符串包及其編號,用顏色為(n,p)的token 表示,如(1,“Modellin”)。 變遷SendPacket 的發(fā)生根據(jù)庫所NextSend 中字符串包的編號將字符串包發(fā)送到Network 端的A 庫所。 庫所E、F 與變遷Ok 用來模擬網(wǎng)絡50%的丟包率,本文假設丟包率為50%。 變遷Update 根據(jù)庫所NextRec 中包的編號進行包的驗證,若通過驗證(n =k),則將包中字符串與庫所Received 中原有字符串拼接得到的字符串更新到庫所Received 中,同時將C 庫所和NextRec 庫所中token顏色更新為下一個待傳輸包的編號。 最后依次通過變遷TransmitAck 和變遷ReceiveAck 將下一個待傳輸包的編號更新到NextSend 庫所中,使變遷Send-Packet 開始發(fā)送一個新的字符串包。
表2 “包傳輸”CPN 模型的顏色集和變量
圖4 “包傳輸”CPN 模型
假設待傳輸包有3 種,為(1,“Modellin”)、(2,“g and An”)和(3,“alysis”),分別記為包1、包2 和包3,視為庫所Send 中3 種不同顏色的token,分別對應表4 中Send 行的顏色標識C1、C2 和C3;庫所E、 F 包 含 2 種 ok-token, 分 別 用 于 變 遷TransmitPacket 與變遷TransmitAck;將變量n 和k 的每種取值(1,2,3)都視作庫所NextSend、NextRec、C和D 中一種顏色的token。 本例中所有變遷的發(fā)生對token 的數(shù)量消耗都是1。 本文根據(jù)該“包傳輸”CPN 模型得到表3 所示的參數(shù),并以此設計了描述文檔。 庫所容限與CPN 初始狀態(tài)如表4 所示。
表3 “包傳輸”CPN 模型的參數(shù)
為了簡化表述,本文采用p1、p2 等字符區(qū)分不同的庫所,采用t1、t2 區(qū)分變遷,采用C1、C2 等字符作為token 的顏色標識,區(qū)分庫所中不同的token,對應關系見表3 與表4。 其中p1、p3、p7 的顏色標識的含義對應相同,p2、p4、p8、p9 的顏色標識的含義對應相同,如p1 的C1 與p3 的C1 都指包1,p2 的C3 與p8 的C3 都指數(shù)字“3”。
表4 CPN 的庫所容限與初始狀態(tài)
在Received(p10)庫所中,C1-token 是指空字符token,即未接收到任何字符包時的token,是CPN 初始狀態(tài)下的p10 庫所包含的token;C2-token 是接收包1 后的token;C3-token 是在C2-token 的基礎上接收包2 后的token;C4-token 是在C3-token 的基礎上接收包3 后的token。 Received 庫所中出現(xiàn)C4-token標志著3 個包的成功發(fā)送。
在Altera Cyclone V 5CSEMA5F31C6N 平臺上進行綜合,綜合頻率為156.37 MHz,ALMs 資源占用781,Register 資源占用2 027。 CPN 狀態(tài)每秒更新5.2×107次。 并采用Quartus 18.1 的Signal tap 邏輯分析儀監(jiān)控設計的運行,得到圖5 所示的信號波形圖,圖中color2_of_place3 信號表示庫所p3 的C2 顏色token,其值是庫所中該token 的數(shù)量。
如圖5 所示,rst_n 信號置為高電平后(圖中虛線),測試從表4 第3 列所示的CPN 初始狀態(tài)開始,此時庫所p1 中有1 個C1-token,庫所p2 中有1 個C1-token,滿足變遷t1 的發(fā)生條件,而其他變遷的發(fā)生條件不充足;因此從圖中虛線后在outclk_2 信號第3 個時鐘上升沿時只有color1_of_place3 信號變高電平,而其他信號數(shù)值不變,表示變遷t1 的發(fā)生在庫所p3 中產(chǎn)生了一個C1-token 并且其他庫所的token 數(shù)量不發(fā)生變化。 測試成功的標志,如圖5 中最下方4 條信號波形所示,庫所p10(Received)的4種token 從C1-token 到C4-token 依次出現(xiàn),表示庫所從空字符依次接收了3 個字符包的過程,進一步對其他信號進行分析,信號的變化過程與CPN 模型的規(guī)定一致,驗證了自動生成工具的正確性。
圖5 Signal tap 邏輯分析儀結果
為了加速CPN 模型的仿真,本文設計基于FPGA 的系統(tǒng)進行加速。 本文完成了CPN 的模塊到硬件結構的映射邏輯,設計了基于C 語言的CPN模型的Verilog 自動生成工具,實現(xiàn)了基于FPGA 的有色Petri 網(wǎng)仿真系統(tǒng)設計。 Signal tap 邏輯分析儀采集得到的信號驗證了仿真系統(tǒng)的正確性。