由於現今的設計其複雜度以指數方式成長，驗證設計的正確性已成為超大型積體電路設計流程的主要瓶頸。在所有的驗證技術中，隨機模擬驗證技術越來越受到大家的重視，最主要的因素是隨機模擬驗證技術可以自動產生非常大量的驗證用之輸入向量。而這些輸入向量可以幫助設計者找到許多預想不到的程式錯誤。可是，向量隨機產生器所產生的輸入向量對於所要驗證的設計來說可能是非法的輸入向量。因此，設計者必須提供限制條件方程式來防止非法之輸入向量的產生。
然而，萃取完整精確的限制條件方程式是一件非常困難的事，而且非常容易出錯。在本篇論文中，我們提出了一個概念：利用一個限制條件硬體模型來避免產生非法之輸入向量。這個限制條件硬體模型可以從設計的驗證環境自動轉換而來而不需要去萃取限制條件方程式。我們以許多的標準檢查之組合電路來做實驗。實驗結果，我們所產生的限制條件硬體模型其面積為原來標準檢查之組合電路的面積的十分之一。

With the rising complexity of designs, design verification has become a bottleneck of the VLSI design process. Among techniques of design verification, random simulation verification has attracted much more interests due to its ability of both automatically generating large verification vectors and uncovering obscure bugs. However, random vector generator may produce input vectors which are “illegal” to a circuit’s inputs. As a result, designers are required to provide the constraint equations to prevent generating of illegal input vectors.
The exact constraint equations are very difficult to derive and error-prone. In this thesis, we propose a hardware model called Constraint Hardware Model, which can avoid generating illegal input vectors. The Constraint Hardware Model can be automatically translated from design environment without the need of writing constraint. We conducted experiments on several combinational benchmark circuits. The experimental results show that our approach can shrinks the circuit size to 10% of the benchmark circuits and reduces the number of primary inputs to 29% of the benchmark circuits.

[1] Scott Taylor, Michael Quinn, Darren Brown, Nathan Dohm, Scot Hildebrandt, James Huggins, Carl Ramey, “Functional Verification of a Multiple-issue, Out-of-Order, Superscalar Alpha Processor—The DEC Alpha 21264 Microprocessor”, In Proc. of Design Automation Conference, June 1998.
[2] James H. Kukula, Thomas R. Shiple, ”Building Circuit from Relations”, In Proc. of the Computer Aided Verification Conf., 2000
[3] K. Shimizu, D. L. Dill, “Deriving a Simulation Input Generator and a Coverage Metric from a Formal Specification,” In Proc. of Design Automation Conference, June, 2002.
[4] J. Yuan, K. Shultz, C. Pixley, H. Miller, A. Aziz, “Modeling design constraints and biasing in simulation using BDDs,” In Proc. of Int'l Conf. on Computer-Aided Design, pages:584-589, Nov. 1999
[5] A. K. Chandra and V. S. Iyengar, “Constraint Solving for Test Case Generation: A Technique for High Level Design Verification,” In Proc. Int'l Conf. on Computer Design, pages:245-248, 1992
[6] S.-C. Chang, L. V. Ginneken, and M. Marek-Sadowska, "Circuit Optimizations by Rewiring," IEEE Trans. on Computer, vol. 48, pp. 962-970, Sept. 1999.
[7] C.-W. Jim Chang, M.-F. Hsiao, and M. Marek-Sadowska, "A New Reasoning Scheme for E±cient Redundancy Addition and Removal," IEEE Trans. on Computer-Aided Design, vol. 22, pp. 945-952, July 2003.
[8] Y.-C. Chen and C.-Y. Wang, "An Improved Approach for Alternative Wires Identi‾cation," In Proc. of Int. Workshop on Logic and Synthesis, 2005.
[9] Shi-Yu Huang, Kwang-Ting ( Tim) Cheng, “Formal Equivalence Checking and Design Debugging”.
[10] System Science, Inc. (Synopsys, Inc.), “The VERA verification system,” http://www.systems.com/product/vera.
[11] Verisity Design, Inc., “Spec-man: Spec-based approach to automate functional verification,” http://www.verisity.com.
[12] Ken Albin , “Nuts and Bolts of Core and SoC Verification,” In Proc. of Design Automation Conference, 2001, June 2001.
[13] P. Faye, E. Cerny, and P. Pownall, “Improved Design Verification by Random Simulation Guided by Genetic Algorithms,” In Proc. of IEEE/IFIP World Computer Congress 2000, Int'l Conf. On Chip Design Automation (ICDA2000), page 2000.
[14] M. Kantrowitz, L.M. Noack, “Functional Verification of a Multiple-issue, Pipelined, Superscalar Alpha Processor – the Alpha 21164 CPU Chip,” In Digital Technical Journal, Vol. 7 No.1 Fall 1995.
[15] A. Aharon, A. Bar-David, B. Dorfman, E. Gofman, M. Leibowitz, and V. chwartzburd, "Verification of the IBM RISC System/6000 by a Dynamic Biased Pseudo-random Test Program Generator," IBM Systems Journal, vol. 30, no. 4 (1991): 527-538
[16] Laurent Fournier, Yaron Arbetman, Moshe Levinger, “Functional Verification Methodology for Microprocessors Using the Genesys Test-Program Generator – Application to the x86 Microprocessors Family” Proceedings of the conference on Design, automation and test in Europe (DATE) March 1999.