利用高階合成技術來進行高階與暫存器轉移階層等效電路驗證

Abstract

高階設計與暫存器轉移階層設計的等同電路驗證是一個在系統晶片及半導體領域是非常有挑戰性且重要的問題。由於高階語言，如C/C++/SystemC和硬體描述語言，如Verilog/VHDL，的特性非常不同，傳統的等效電路驗證方法不再適用。 在此碩論中，我們分析此問題並定義一個可以利用高階合成技術來解決的子問題，稱做「有限狀態機等效驗證」。更詳細地說，我們分析並從暫存器轉移階層建立一個有限狀態機，並且驗證是否存在一種對高階設計做高階合成的方法，使得高階合成之後之有限狀態機和從暫存器轉移階層建立的完全相同。如果存在這種方法，我們可以知道他們等效。 另外，我們提出「攤平的程式相依圖」(flattened program graph)來代表高階設計的，它的優點是可以比傳統用來做高階合成的控制資料流程圖(control data flow graph)保有更多的彈性。我們也利用「雙模擬」(bi-simulation)來快速地刪減不可能的解，並利用正規方法(formal method)來確認是否等同。 最後，我們做了許多單元測試(Unit test)來表示我們可以支援的語法並利用其他測資來確認我們的等同電路驗證方法是可行且有效率的。

Equivalence checking between high-level designs and register-transfer-level designs has been a very challenging and important problem in the context of system on chips (SoCs). Due to the very different language constructs and features in high-level languages, such as C/C++/SystemC and RT-level languages, like Verilog/VHDL, the traditional definition of equivalence is not suitable anymore. In this work, we analyze the whole problem space and define a subset of it, called FSM-compatible equivalence checking, which can be solved efficiently utilizing high-level synthesis techniques. That is, we extract a FSM from RT-level design and verify whether there exists a way to synthesize the high-level design into an equivalent FSM. If there exists, we can conclude that the two designs are equivalent. Furthermore, we propose the flattened program dependence graph, which has more flexibilities than the conventional control data flow graph, to represent a high-level model and enlarge the search space. We utilize bi-simulation to quickly prune infeasible solution and then apply formal engine to verify the equivalence of two FSMs as well. We conduct several unit tests and utilize three case studies to show the language constructs that we can support. We demonstrate the effectiveness of our methodologies, too.