As the operational behavior of IC chips become more complex, the number of clocks in a single chip also increases. In particular, IP based designs drive the merging of heterogeneous modules into a single chip. Additionally, in the interest of reducing total energy usage, voltage and frequency scaling techniques are used to make such IPs operate at variable frequencies. Under such circumstances, designing interfaces for different clock connections becomes a highly complex task.
In this thesis, a symbolic reachability analysis method and a model checking method for multiple-clock system designs are proposed. This is the first approach to deal with both synchronization problems caused by metastability and rate mismatch problems caused by clock frequency mismatches in a single framework.
First of all, a method to remove certain parts of the design being verified is proposed. By removing certain parts of the design, we can reduce the complexity of the testbench model. Secondly, a method to remove one clock domain is proposed. This way, we can make a single clock model from multiple-clock models. Instead of setting inputs to the target model as free variables which could assume any arbitrary value regardless of the input constraints, the proposed method reflects the input constraints into the target model by modifying the transition relation of the target model. Therefore, false alarms caused by infeasible inputs do not occur. This was verified by various circuit examples. Two schemes are proposed to achieve this goal; one is to remove the testbench from the entire transition relation after removing the inactivated edges by applying a set of reachable states. The other is to apply the so-called input-sifting function to the transition relation of the target model to maximize the benefits of using a partitioned transition relation which is employed to deal with target systems of industrial complexity. Experimental results are given to show that an improvement in the model checking time was observed by up to about 5000 times.
In order to reproduce problems that occur with multiple-clock system designs during reachability analysis, three methods are described; 1) alternate evaluation for a system with two clocks as the base-line model, 2) non-deterministic delayed evaluation to reproduce a synchronization problem, and 3) double evaluation to reproduce a clock frequency mismatch. Experimental results on ISCAS 89 benchmark show an improvement factor of average CPU time as compared to Clarke's method[1] by 1.30, 60.08, 1.98 and 54.28 times when alternate evaluation double evaluation, alternate evaluation with NDDE and double evaluation with NDDE is applied, respectively.
A single clock domain model can be made from a multiple-clock system model by using the first method mentioned above, by which one can remove a given clock domain after performing a reachability analysis. Then, traditional model checking methods can be applied to the single clock domain model that has been extracted. Thus, model checking for multiple-clock domain system designs can be performed by using the proposed methods.
본 논문에서는 다중 클락 시스템 설계의 검증을 위한 기호적 상태 도달성 분석 방법 및 모델 확인 방법을 제안한다.
먼저 주어진 모델에서 검증에 사용하지 않을 일정 부분을 제거하는 방법을 제안한다. 제안된 방법은 타겟 모델의 입력을 자유 변수로 설정하는 대신에 상태 도달성 분석의 결과를 이용하여, 실제로 존재 가능한 값 만을 이용하도록 한다. 이를 위해 단일 상태 천이 연관 함수를 이용하는 방법과, 분할 상태 천이 연관 함수를 이용하는 방법을 제시한다. 제시된 방법은 모델 확인 시간을 최대 5000배까지 줄일 수 있었다.
또한 본 논문에서는 다중 클락 시스템의 기호적 상태 도달성 분석 방법을 제안한다. 제안된 방법은 다중 클락 시스템이 가지는 메타스테빌리티, 속도 불일치등에 의한 동기화 문제를 고려한 상태 도달성 분석을 단일 체제로 해 낼 수 있다. 세가지 방법을 통해 상태 도달성 분석을 수행한다. 먼저 기본 모델을 검증하기 위한 순차적 계산과, 동기화 문제를 고려하기 위한 비 결정적 지연 계산 그리고 속도 불일치를 고려하기 위한 이중 계산이다. 제안된 방법은 ISCAS89 벤치마크 회로로서 기존의 클라케가 제시한 방법과 비교 하였을 때에 순차적 계산, 이중 계산, 비결정적 지연 계산, 그리고 이중계산과 비결정적 지연 계산을 함께 했을 경우 각각1.30, 60.08, 1.98, 54.28배의 성능 향상을 보여 주었다.
제안된 두 방법, 즉 다중 클락 시스템의 기호적 상태 도달성 분석 방법과, 전체 시스템 모델의 일부를 제거할 수 있는 방법을 함께 활용하여, 다중 클락 시스템에서의 도달 가능한 상태 하의 모델 확인 방법을 수행 할 수 있다.
