透過您的圖書館登入
IP:3.22.248.208
  • 學位論文

設計去管道化之抽象化技術

Abstraction Techniques for Design Depipelining

指導教授 : 黃鐘揚

摘要


在利用事件驅動的方法來進行模擬的時候,管道設計中的同步控制電路反而是拖慢模擬速度的信號。因此,設計去管道化的技術在簡化管道設計中的控制電路中扮演著很重要的角色。然而,為了特定的規格或性質而實作的控制圖,控制圖上時常發生狀態爆炸。因此,這樣的技術並不適合驗證超純量暫存器轉移層次設計。這裡有各種方式去解決狀態爆炸的問題,例如分解和抽象化技術都是可行的解決方案。以抽象化技術而言,將具體的路徑映射到抽象路徑可以有效減少狀態的數量。因此,我們提出了一個設計去管道化的抽象化技術,這樣的技術將會自動產生一個網表,然後設計者就可以在這個網表上模擬電路運作。雖然,這個網表的輸出量和原本的管道化設計不同,但我們確保這兩個設計的模擬輸出結果將會是相同的。為了提高模擬的效率,我們的演算法尋找有限狀態機與使用抽象化技術。根據實驗結果,這樣的演算法能有效的提高模擬速度於管道化設計。與迴圈展開的技術做比較,我們的模擬時間將會大幅降低。

關鍵字

抽象化技術 去管道化 模擬 驗證

並列摘要


For simulation-based verification, control circuits for synchronization in pipelined design are tedious, especially for the event-driven simulation. Therefore, depipelining technique plays an important role in the control logic simplification of pipelined design. However, it would cause state explosion due to the need of formulating the implementation with respect to a certain specification or property. Consequently, it is not scalable for current superscalar RTL design. To conquer these problems, the techniques utilizing various strategies such as decomposition and abstraction might be the solutions. The abstraction technique that maps concrete paths to abstract ones attempts to reduce the number of states. Therefore, we propose a design depipelining algorithm which computes approximate abstraction of pipelined design. Moreover, a netlist will be generated in our approach. Although the throughput of the netlist is different from the original design, we ensure that the simulation outputs of these two designs are identical. In addition, to enhance the efficiency, finite-state machine extraction and abstraction techniques are applied to our work. The experimental results show that our algorithm is effective in increasing simulation-speed of pipelined design. When compared to the loop-unrolling technique, the simulation of our work is much faster.

參考文獻


[12] P. Chauhan, D. Goyal, G. Hasteer, A. Mathur, and N. Sharma,“Non-Cycle-Accurate Sequential Equivalence Checking,” In Design Automation Conference (DAC ‘09), pp. 460-465, 2009.
[2] K. Namjoshi and R. Kurshan, “Syntactic Program Transformations for Automatic Abstraction,” In Computer-Aided Verification (CAV ‘00), pp. 435-449, 2000.
[3] P-H. Ho, A. J. Isles, and T. Kam, “Formal Verification of Pipeline Control Using Controlled Token Nets and Abstract Interpretation,” In ACM-IEEE International Conference on Computer-Aided Design (ICCAD ‘98), pp. 529-536, 1998.
[4] Z. S. Andraus, M. H. Liffiton, and K. A. Sakallah, “Refinement Strategies for Verification Methods Based on Datapath Abstraction,” In Asia South Pacific Design Automation (ASP-DAC ‘06), pp. 19-24, 2006.
[6] V. Ciubotariu, “Automatic Datapath Abstraction of Pipelined Circuits,” PhD thesis, Computer Science, University of Waterloo, 2011.

延伸閱讀