高階合成中使用臆測編碼轉換技術之排程等效驗證

Abstract

高階合成是一個將演算法層次的描述轉換成暫存器轉移層次設計的程序，它可以提昇生產力。然而這轉換程序容易錯誤。排程，高階合成的子工作，是驗證高階合成中最大的挑戰，因為排程會改變原來的執行順序。這篇論文的研究主題是排程驗證。我們提出一個正規方法可用來驗證排程前後的描述是否相等。排程前後的描述由包含資料路徑的有限狀態機所表示。它們一開始先被分解成有限條路徑；接著，在這些路徑中找到相等的路徑。兩個包含資料路徑的有限狀態機的相等和兩條路徑的相等在這篇論文中被定義。提出的方法不只適合驗證保留控制架構的排程，也適合驗證會改變控制架構的排程。排程改變控制架構藉由合併連續的路徑或將某些程式碼在不同的基本塊中移動。由驗證高階合成的測試程式的實驗結果顯示我們演算法可以有效地驗證排程。