순차 논리 회로의 모델 검증을 위한 STG 탐색 알고리듬 구현
- 발행기관 서강대학교 대학원
- 지도교수 황선영
- 발행년도 2005
- 학위수여년월 200508
- 학위명 석사
- 학과 및 전공 전자공학
- 식별자(기타) 000000084498
- 본문언어 한국어
초록/요약
본 논문은 순차 논리 회로의 state transition graph 를 탐색하는 모델 검증기의 설계와 구현에 대해 기술한다. 효율적인 state transition graph 의 탐색을 위해 symbolic STG(State Transition Graph) 탐색을 수행하는 heuristic 알고리듬을 제안하였다. state 탐색 과정은 너비 우선 탐색과 state transition 관계를 이용한 image computation 을 이용하여 수행된다. 기존 state 집합들 사이의 image computation 과정을 이용하는 방법과는 달리 제안된 image computation 과정은 과거 image computation 의 기록을 이용하여 탐색함으로 32% 의 성능 향상으로 탐색 시간을 줄일 수 있도록 개선되었다. 실험 결과를 통하여 제안된 알고리듬이 순차 논리 회로의 state transition graph 를 탐색하는 효율적인 툴임을 보였다.
more초록/요약
This thesis describes the design and implementation of an model checker which explores state transition graph(STG) for sequential logic circuits. For the efficient exploration of a state transition graph, a heuristic algorithm is proposed for symbolic STG traversal. The exploration process is performed by image computation based on state transition relations using the breadth-first search algorithm. In the image computation process, efforts are made to reduce the search time by utilizing previous results of image computation rather than using unique transition relations among state sets. Experimental results show that the proposed algorithms can reduce the runtime by about 32% on the average, and can be a viable tool for model checking for the verification of sequential logic circuits.
more