This thesis presents a methodology of formal verification using model checking tool. Model checking is used to determine the validity of formulas written in temporal logic to respect the behavioral model of a system.
One of the serious limitations of the model checking approach comes from its reliance on the explicit state transition graph representation of the hardware system to be verified. Typically, the number of states increases exponentially with the number of elements in the system, resulting in what is popularly called the state explosion problem. Although many researchers have tried to verified solved this problem using the abstraction and reduction of the environment and target system, no general and explicit methodology for the abstraction of the environment has been presented yet.
The proposed method in this thesis tries to solve the state explosion problem in the model checking is based on ‘design separation’ and ‘interface abstraction’. Design separation is a process separating the whole design into small designs to be verifiable while the interface abstraction is a process for modeling the interface behavior between separated designs. By means of this method the complex design having a state explosion problem can be verified successfully and the memory usage and computing time for model checking also can be improved about 100 times than no use of the proposed method.
VLSI기술이 발달할수록 디자인의 복잡도는 증가하고 사용 범위도 크게 확대되어 왔다. 전통적인 검증 방법으로는 이러한 상황에 대처하기가 점점 힘들어 지고 있고 있다. 이러한 문제점을 해결하기 위해서 형식화된 검증방법이 도입되었고 모델 체킹은 현재 많이 사용되는 형식화된 검증방법 중의 하나이다. 하지만 모델 체킹은 스테이트 폭발 문제를 해결해야 하는 문제점을 가지고 있다. 이를 위해서 일반적으로 모델을 추상화하는 과정이 필요한데 이것은 검증자에게 많은 시간과 노력을 요한다. 따라서 추상화 과정을 줄이면서도 검증을 가능하게 하는 방법이 필요하다.
이 논문에서는 이러한 방법 중의 하나로 복잡한 모델을 모델 체킹이 가능하게 작은 모듈로 나누고 모듈의 인터페이스 부분만을 모델링하는 인터페이스 추상화를 이용한 모델 체킹 방법을 제안하였다. 이 방법을 이용하여 모델 체킹을 하면 원하는 속성을 검증하면서 메모리 사용량과 계산 시간을 줄일 수 있음을 보였다.
