標題: 用於高階合成之派翠網路式系統階層驗證技術
Petri-Net based System-level Verification Techniques on High-level Synthesis
作者: 江宗錫
Tsung-Hsi Chiang
董蘭榮
Lan-Rong Dung
電控工程研究所
關鍵字: 高階合成;資料流系統;正規化驗證;派翠網路;high-level synthesis;dataflow system;formal verification;Petri net;model checking
公開日期: 2006
摘要: 本論文提出創新的系統階層驗證(system-level verification)技術,驗證的目標是高階合成(high-level synthesis)的設計結果,驗證的範圍是針對資料流系統(dataflow)或數位信號處理導向(DSP-driven)的演算法,驗證的理論是基於派翠網路(Petri net)圖型理論與技術。系統階層驗證的意義,主要在於驗證系統架構(architecture)的正確性,其目的與在RTL階層所做的功能性(functionality)驗證是不同的。通常,資料流或數位信號處理導向的演算法需要利用系統階層之演算法轉換技術(arithmetic transformation)作系統架構的最佳化設計,目的是為了使受設系統能夠符合系統規範,或藉由改善系統架構,來達成效能最佳化;另一方面,將演算法實現到硬體架構之前,所有運算工作也必須明確的被排程或將工作指派給某些運算單元依序執行。然而,系統階層的演算法轉換技術與運算元排程需要仰賴複雜的演算法來達成,而這樣的設計流程是非常容易出錯的。為了能夠偵測系統階層設計時候的設計錯誤,在系統階層的設計流程中,我們引入了系統階層驗證技術來驗證高階合成結果的正確性。不同於傳統複雜邏輯推論的驗證方法,我們提出以Petri net圖型理論與技術作為基礎,用來偵測資料流系統在高階合成階段可能發生的設計錯誤。首先,我們會利用所提出的圖型轉換法則,將原始的資料流圖型轉換成Petri net圖型。然後,以我們所提出的兩個系統階層驗證架構,使受測系統能在Petri net圖型領域中進行系統階層的驗證工作。與傳統的驗證技術比較起來,我們將驗證的工作從RTL階層提升到系統階層,因此,在系統階層設計初期,就能偵測可能產生的設計錯誤。越早在設計初期偵測設計的錯誤,就越能夠減少重新設計的成本並且縮短產品上市的時間。利用本論文所提出的驗證方式,我們也實現了幾種不同的系統階層的驗證演算法用來驗證高階合成的設計結果,並從實驗數據中,歸納出最佳的驗證演算法。
This thesis presents a novel verification technique for detecting design faults of high-level synthesis (HLS) results of the dataflow or DSP-driven algorithms by using Petri net (PN) theory. System-level or high-level verification means architecture verification, which is different from functional verification in register transfer level (RTL). Generally, dataflow or DSP-driven algorithms need algorithmic transformations to achieve optimal goals and also need scheduling algorithms to allocate processor resources for all execution tasks before mapping on a silicon. However, the optimization procedures of the algorithmic transformations and the design scheduling in HLS are error-prone and complex. In order to detect high-level faults, PN based high-level verification flow is introduced and applied in HLS. Instead of applying Boolean algebra in conventional verification, the PN based verifier adopts mathematical matrix manipulation of linear algebra. In the proposed verification flow, we first convert a dataflow or DSP-driven design in the form of FSFG graph into PN domain by using proposed graph based conversion method. Then, two PN based verifier frameworks are proposed to verify the correctness of the HLS results. While comparing to the conventional verification techniques, we put the verification work beyond the RTL or gate level, thus high-level design faults can be detected in the early stage of the design flow. Early fault detection in system-level design flow is helpful for reducing redesigning cost and time-to-market cycle time. Base on the proposed method, we also implement several algorithms of HLS verifiers. From the experimental results of the verification algorithms, we conclude the best approach algorithm of the verifier.
URI: http://140.113.39.130/cdrfb3/record/nctu/#GT008912804
http://hdl.handle.net/11536/77101
Appears in Collections:Thesis


Files in This Item:

  1. 280401.pdf