Browsing by Author "Yen, CC"

Now showing 1 - 7 of 7

A divide-and-conquer-based algorithm for automatic simulation vector generation
(2004-03-01)
Yen, CC
;
Jou, JY
;
Chen, KC
;
電子工程學系及電子研究所
;
Department of Electronics Engineering and Institute of Electronics
An optimum algorithm for compacting error traces for efficient functional debugging
(2005)
Yen, CC
;
Jou, JY
;
電子工程學系及電子研究所
;
Department of Electronics Engineering and Institute of Electronics
Diagnosing counter examples with error traces has acted as one of the most critical steps in functional verification. Unfortunately, error traces are normally very lengthy such that designers need to spend considerable effort to understand them. To alleviate designers' burden for debugging, we present a SAT-based algorithm for reducing the lengths of error traces. The algorithm performs the paradigm of binary search algorithm to halve the search space recursively. Furthermore, it applies a novel theorem to guarantee to gain the shortest lengths for the error traces. Experimental results demonstrate that our approach greatly surpasses previous work and indeed has the optimum solutions.
Automatic functional vector generation using the interacting FSM model
(2001)
Liu, CNJ
;
Yen, CC
;
Jou, JY
;
電子工程學系及電子研究所
;
Department of Electronics Engineering and Institute of Electronics
While the coverage-driven design validation is getting popular, it would be more convenient for users to have an automatic generator that can generate the input patterns to satisfy the coverage requirements. The symbolic techniques can be used to generate the desired input patterns easily for a specific state transition 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 issues for large circuits. It can generate all possible input combinations or notify that such cases will never happen for any specific state transitions. Because we can reasonably partition the HDL designs into the interacting FSM model, the peak memory requirement can be significantly reduced by using the "divide and conquer" strategy for those small FSMs. The experimental results show that we can indeed generate the required input patterns with reasonable memory requirement for the designs with thousands of registers.
Enhancing sequential depth computation with a branch-and-bound algorithm
(2004)
Yen, CC
;
Jou, JY
;
電子工程學系及電子研究所
;
Department of Electronics Engineering and Institute of Electronics
We present an effective algorithm to enhance sequential depth computation. The sequential depth plays the most crucial role to the completeness of bounded model checking. Previous work computes the sequential depth by exhaustively searching the state space, which is unable to keep pace with the exponential growth of design complexity. To improve the computation, we develop an efficient approach that takes the branch-and-bound manner. We reduce the search space by applying a partitioning as well as a pruning method. Furthermore, we propose a novel formulation and integrate the techniques of BDDs and SAT solvers to search states that determine the sequential depth. Experimental results show that our approach considerably enhances the performance compared with the results of the previous work.
Formal compliance verification of interface protocols
(2005)
Yang, YC
;
Huang, JD
;
Yen, CC
;
Shih, CH
;
Jou, JY
Verifying whether a building block conforms to certain interface protocol is one of the important steps while constructing an SoC However, most existing methods have their own limitations. Simulation-based methods have the false positive problem while formal property checking methods may suffer from memory explosion and excessive runtime. In this paper, we propose a novel branch-and-bound algorithm for interface protocol compliance verification. The properties of the interface protocol are specified as a specification FSM, and the interface logic is formally verified at the higher FSM level. Using the FSM for property specification is relatively systematic than using other proprietary property languages, which greatly reduces the possibility of incomplete property identification. And it is shown theoretically and experimentally that the proposed algorithm can finish in reasonable time complexity.
Integration of finite element analysis and optimum design on gear systems
(2002-01-01)
Li, CH
;
Chiou, HS
;
Hung, CH
;
Chang, YY
;
Yen, CC
This work establishes a batch module called "integration of finite element analysis and optimum design" by taking gear systems as testing examples. This batch module consists of I-DEAS, ABAQUS/Standard and MOST software, which serve as the preprocessor, the numerical solver and the optimizer, respectively. A simple and practical method was developed, by which this module was enabled to search for contact nodes and elements and to automatically define the contact surfaces for contact analysis. A simple gear-pair system and a complete planetary gear system were successively used as testing examples for this integrated module. The module will automatically construct the geometrical model, analyze contact stress and solve for the optimal solutions when gearing parameters are input. The results are expected to enhance the technology of gear system design. (C) 2002 Elsevier Science B.V. All rights reserved.
On compliance test of on-chip bus for SOC
(2004)
Lin, HM
;
Yen, CC
;
Shih, CH
;
Jou, JY
;
電子工程學系及電子研究所
In this paper, we employ a monitor-based approach for on-chip bus (OCB) compliance test. To describe the OCB protocols, we propose a FSM model, which can help to extract the necessary properties systematically and verify the data part of a bus transfer efficiently. To demonstrate our methodology, we illustrate two OCB protocols, WISHBONE and AMBA AHB, as the study cases. The experimental results show that we can verify the OCB protocols efficiently and detect the design errors when tests fail.