針對互動有限狀態機中狀態改變序列的自動測試向量產生器

Abstract

隨著涵蓋驅動設計驗証方法的普及，若能有一種通用的自動測試向量產生器來產生輸入的測試向量，對於滿足功能涵蓋需求將會有大大的助益。在有限狀態機中，用符號式的技巧能輕易地對特定的狀態改變序列產生所需的輸入測試向量。然而，對於記憶體的龐大要求使得符號式的技巧無法應用於實際的設計之中。在這篇論文□，我們提出了一個能克服記憶體需求限制的自動測試向量產生器。它能針對任何特定的狀態改變序列產生出所需的輸入測試向量，或是告知某狀態改變序列不可能發生。因為我們能直接從硬體描述語言（HDL）中抽出有限狀態機，所以我們更進一步使用“個個擊破”的策略，讓符號式的技巧能在較小的記憶體需求下使用。因此，我們的測試產生器能真正處理實際的、高複雜度的電路設計。有了這個自動測試向量產生器，我們可以建造出許多涵蓋驅動設計驗証的工具。由實驗結果証明，我們能在合理的記憶體要求下，處理擁有超過千個以上暫存器的複雜電路。

While the coverage-driven design validation is getting popular, it would be more convenient for the users to have a universal automatic pattern generator that can produce input patterns to satisfy coverage requirements. The symbolic techniques can easily generate the desired input patterns for a specific state transition or state sequence in a FSM. However, it is not practical for real designs because the memory requirement is often unmanageable. In this paper, we propose an automatic pattern generation engine that can overcome the memory issue in large circuits. It can generate all possible input combinations or notify that such cases will never happen for any specific state transitions or state sequences. Because we use the FSM extraction technique to automatically translate the HDL designs into the interacting FSM model, the peak memory requirement for the symbolic techniques can be significantly reduced by using the “divide and conquer” strategy for those small FSMs. Our tool can thus handle the high-complexity designs. With this powerful engine, we can build many useful tools including the desired automatic pattern generator for the coverage-driven design validation. The experimental results show that we can indeed generate the required input patterns with reasonable memory requirement for the designs with thousands of registers. ABSTRACT ii ACKNOWLEDGEMENTS iii CONTENTS iv LIST OF TABLES v LIST OF FIGURES vi Chapter 1 Introduction………………………………………. 1 Chapter 2 Basic Symbolic Methods…………………………. 4 2.1 Binary Decision Diagrams………………….. 4 2.2 Build BDDs for Boolean Networks………… 7 2.3 Represent a FSM using BDDs……………… 9 2.4 Symbolic Operations………………………... 13 2.4.1 Cofactor Operation……………………… 13 2.4.2 Existence Quantification………………… 14 2.4.3 Image Computation……………………… 16 Chapter 3 Interacting FSM Model (IFSM)…………………… 18 3.1 IFSM Model…………………………………… 18 3.2 HDL Assumptions…………………………….. 19 Chapter 4 Functional Test Pattern Generation by the “Divide- and-Conquer” Strategy…………………………….. 20 4.1 The “Divide-and-Conquer” Strategy…………... 20 4.2 Divide: Building the IFSM Model…………….. 21 4.3 Conquer: Dealing with Each FSM…………….. 23 4.4 Combine: Interaction Checking……………….. 25 4.5 Pattern Generation Algorithm…………………. 27 4.6 An Example: The Car-Speed-Control-System… 28 4.6.1 The Car Speed Control System………….. 28 4.6.2 Divide: Build the IFSM Model…………... 30 4.6.3 Conquer: Dealing with Each FSM……….. 30 4.6.4 Combine: Interaction Checking………….. 34 Chapter 5 Experimental Results………………………….. 37 Chapter 6 Conclusions……………………………………. 41 Reference…………………………………………………... 42