본문바로가기

자료 카테고리

검색결과

검색결과 (전체 1건)

검색결과제한

열기
내서재담기 야간이용신청목록담기(서울관) 한자 한글변환 목록으로 알림톡 발송 우편복사 목록담기 프린트
이 자료 추천하기 오류신고
MARC
논문명/저자명
범위를 지정하지 않는 SAT 기반 모델 검증에 관한 연구 = SAT-Based unbounded symbolic model checking / 강형주 인기도
발행사항
대전 : 한국과학기술원, 2005.2
청구기호
TD 621.38195 ㄱ272ㅂ
형태사항
vii, 88 p. ; 26 cm
자료실
전자자료
제어번호
KDMT1200545548
주기사항
학위논문(박사) -- 한국과학기술원, 전기및전자공학, 2005.2
원문

목차보기더보기

Title Page

Abstract

Contents

Chap. 1. Introduction 11

Chap. 2. Previous works 14

2.1. Model checking 14

2.1.1. Modeling Systems 14

2.1.2. Temporal Logics 20

2.1.3. Model Checking : a CTL property 25

2.1.4. Model Checking Procedures Represented in Fixpoint 33

2.2. Symbolic model checking 35

2.2.1. Symbolic Representation 35

2.2.2. Model Checking in Symbolic Representation 38

2.3. Boolean satisfiability checking (SAT) 40

2.3.1. Conjunctive Normal Form 41

2.3.2. SAT Procedure 43

2.4. SAT-based unbounded symbolic model checking 45

Chap. 3. Quantification by a satisfy-all procedure 47

3.1. Problem definition 47

3.2. Proposed satisfy-all procedure 48

3.2.1. Converting a Set of Assignments into a CNF Formula 49

3.2.2. Example 50

3.2.3. Justification 53

3.2.4. Managing Excluding and Conflict Clauses 56

Chap. 4. Cache table in the satisfy-all procedure 58

4.1. Motivation 58

4.2. Example 59

4.3. Basic principles 62

4.4. Table management 63

4.5. Implementation 66

4.6. Enhancing techniques 67

4.6.1. Cache Access Region 67

4.6.2. Justification 68

4.6.3. Excluding Clauses 68

4.6.4. Compressing Solutions 69

4.6.5. Hit Between Non-Equivalent Situations 69

4.7. Minor techniques 70

4.7.1. Watching Literal Scheme 70

4.7.2. Hit Ratio Increasing Schemes 72

Chap. 5. SAT-based unbounded symbolic model checking algorithm 74

5.1. Pre-image and fix-point calculation 76

5.2. Inclusion and empty checking 78

5.3. Enhancing safety-property checking 78

Chap. 6. Experimental results 81

6.1. Test sets 81

6.2. Statistics about a cache table 82

6.3. Results with options 86

6.4. Comparison with SMV and McMILLAN's algorithm 88

Chap. 7. Conclusion 90

요약문 92

References 94

Curriculum Vitae 101

Table 1. The relationship between the next state variables, the current state variables, and the input variables. 17

Table 2. Characteristics of ISCAS 89 Circuits 82

Table 3. Processing Time and Memory Usage With Options 85

Table 4. Experimental Results for the Proposed Algorithm with Various Weighting Schemes 87

Table 5. Experimental Results for SMV, McMillan's Algorithm and the Proposed Algorithm 89

Fig. 2-1. An example circuit. 15

Fig. 2-2. The transition graph of the circuit in Fig. 2-1. 18

Fig. 2-3. The computation tree made from Fig. 2-2 21

Fig. 2-4. Examples of CTL operators. 24

Fig. 2-5. A tree from a property. 26

Fig. 2-6. A procedure to obtain the set of states where EF p holds. 27

Fig. 2-7. The concept of the procedure in Fig. 2-6. 27

Fig. 2-8. The process of the procedure in Fig. 2-6 : (a) before the iteration, (b) after the first iteration, (c) after the second iteration, (d) after the third iteration, (e) after the forth iteration, and (f) after the sixth iteration. 30

Fig. 2-9. A procedure to obtain the set of states where EG p holds. 31

Fig. 2-10. The process of the procedure in Fig. 2-9 : (a) before the iteration, (b) after the first iteration, (c) after the second iteration, (d) after the third iteration, (e) after the forth iteration. 33

Fig. 2-11. The procedure for a least fixpoint. 34

Fig. 2-12. The procedure for a greatest fixpoint. 34

Fig. 2-13. Symbolic version of the procedure in Fig. 2-6. 40

Fig. 2-14. Symbolic version of the procedure in Fig. 2-9. 40

Fig. 2-15. An example Boolean formula. 43

Fig. 2-16. A CNF form of the example Boolean formula 43

Fig. 2-17. Conventional SAT procedure 44

Fig. 2-18. The process of the SAT procedure. 45

Fig. 3-1. Proposed Satisfy-All procedure. 48

Fig. 3-2. Example of the Satisfy-All procedure. 52

Fig. 3-3. (a) A satisfying assignment is found. (b) A better assignment is generated by the JustifyO routine. 54

Fig. 4-1. Two nodes that have the same sub-tree. 60

Fig. 4-2. When a node that has the same sub-tree as a previously met node is encountered. 61

Fig. 4-3. Detecting a node that has the same sub-tree as a node previously met. 61

Fig. 4-4. Proposed Satisfy-All procedure with a cache table. 65

Fig. 4-5. Data structure of the proposed Satisfy-All procedure. 66

Fig. 5-1. UMC algorithm with state sets represented in CNF. 75

Fig. 5-2. Pre-image calculation. 77

Fig. 5-3. Fix-point calculation in the case of EF p. 77

Fig. 5-4. Safety-property checking procedure. 79

Fig. 6-1. Statistic of a cache table: (a) the number of hits and misses and the average number of solutions per hit and (b) the hit ratio and the expected number of reused solutions. 83

Fig. 6-2. Processing time and hit ratio fluctuations with various cache access regions: (a) fixed width and various positions and (b) fixed upper-bound and various widths. 84

초록보기 더보기

설계하는 회로의 복잡도가 증가하여 검증하기가 어려워 짐에 따라 회로를 검증하는 기법에 대해 많은 연구가 이루어 지고 있다. 이 논문에서는 범위를 지정하지 않는 모델 검증에 있어서 메모리의 사용을 줄이기 위해 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에 기반한 알고리즘에 비해 더 많은 회로를 검증할 수 있음을 보였다.

내서재담기 야간이용신청목록담기(서울관) 한자 한글변환 목록으로 알림톡 발송 우편복사 목록담기 프린트

권호기사보기

권호기사 목록 테이블로 기사명, 저자명, 페이지, 원문, 기사목차 순으로 되어있습니다.
기사명 저자명 페이지 원문 기사목차
연속간행물 팝업 열기 연속간행물 팝업 열기