In this thesis, a SAT-based unbounded symbolic model checking algorithm is proposed to reduce memory usage. The conjunctive normal form is used to represent sets of states and transition relation. A logical operation on state sets is implemented as an operation on conjunctive-normal-form formulas. A Satisfy-All procedure is proposed to compute the existential quantification required in obtaining the pre-image and fix-point. The proposed Satisfy-All procedure is implemented by modifying a SAT procedure to generate all the satisfying assignments of the input formula, which is based on new efficient techniques such as line justification to make an assignment covering more search space, excluding clause management, and two-level logic minimization to compress the set of found assignments.
In addition, a cache table is introduced into the Satisfy-All procedure. It is a difficult problem for a Satisfy-All procedure to detect the case that a previous result can be reused. This thesis shows that the case can be detected by comparing sets of undetermined variables and clauses. The data structure that can perform the operation efficiently will also be described. Line justification and excluding clause management schemes are discussed to be applied to the cache scheme. It will be discussed also to obtain better performance when the cache scheme is applied.
A few benchmark circuits with various sizes are used in the experiments. Parameters will be determined based on the performance measure. The experimental results show the proposed algorithm can check more circuits than BDD-based and previous SAT-based model checking algorithms.
설계하는 회로의 복잡도가 증가하여 검증하기가 어려워 짐에 따라 회로를 검증하는 기법에 대해 많은 연구가 이루어 지고 있다. 이 논문에서는 범위를 지정하지 않는 모델 검증에 있어서 메모리의 사용을 줄이기 위해 SAT을 사용하는 방법을 제안하였다. 이 방법에서는 회로의 상태들의 집합과 상태들 사이의 이동을 conjunctive normal form으로 표현한다. 따라서 상태 집합들 사이의 집합 연산들은 conjunctive normal form의 식들 사이의 연산으로 대체된다. 모델 검증에서는 합집합이나 교집합과 같은 간단한 집합 연산뿐 아니라 pre-image를 구하기 위해 quantification가 같은 연산도 필요하다. Conjunctive normal form의 식에 quantification을 수행하기 위해 기존의 SAT 알고리즘을 변형하여 주어진 식의 모든 해를 구하는 Satisfy-All 알고리즘을 제안하였다. 제안된 알고리즘에서는 line justification을 이용하여 주어진 해가 더 많은 search space를 포함하게 하였고, 효율적으로 clause들을 관리하는 기법을 개발하였으며, two-level logic 최소화 기법을 이용하여 해들의 집합을 압축하였다.
그리고, Satisfy-All 알고리즘에 캐쉬 테이블을 도입하여 같은 search space를 다시 찾지 않아도 되게 하였다. Satisfy-All 알고리즘에 캐쉬 테이블을 도입하는데 있어 제일 큰 문제점은 이전의 결과를 재사용할 수 있는 경우를 찾는 것이 어렵다는 것이다. 이 논문에서는 값이 결정되지 않은 변수들과 만족되지 않은 clause들을 비교함으로써 그러한 경우를 알아 낼 수 있음을 보였다. 그리고, 이러한 비교를 효율적으로 할 수 있는 데이터 구조와 프로시져를 개발하였다.
다양한 벤치마크 회로들을 이용해서 실험을 하였으며, 성능 측정을 통해 캐쉬 테이블의 파라메터들을 정하였다. 실험 결과를 통해 제안한 알고리즘이 기존의 BDD에 기반한 알고리즘이나 SAT에 기반한 알고리즘에 비해 더 많은 회로를 검증할 수 있음을 보였다
