계층적 설계를 유한상태기계(FSM)로 변환해 CTL 기반 모델 체킹으로 검증하는 방법과 BDD/MDD, 공정성 제약, 언어 포함(언어 공허성) 개념을 설명하고, 신호등 제어기 예제로 속성과 제약을 제시합니다.
형식적 검증 소개
다음: Formal Verification in 위로: 제목 없음 이전: Describing Designs for
형식적 검증은 설계가 특정 요구사항(속성)을 만족하는지 여부를 점검하는 과정이다. 우리는 (이전 절에서 보인 것처럼) 계층적으로 명세될 수 있는 설계의 형식적 검증에 관심이 있으며, 이는 인간 설계자의 작업 방식과도 일치한다. 설계를 형식적으로 검증하려면 먼저 더 단순한 “검증 가능한” 형식으로 변환해야 한다. 설계는 상호작용하는 시스템들의 집합으로 명세되며, 각 시스템은 상태라고 부르는 유한 개의 구성(configuration)을 갖는다. 상태와 상태 간 전이는 FSM(유한상태기계)을 이룬다. 전체 시스템은 각 구성요소에 대응하는 FSM들을 합성해 얻은 하나의 FSM이다. 따라서 검증의 첫 단계는 시스템의 완전한 FSM 기술을 얻는 것이다. 주어진 현재 상태(또는 현재 구성)에서, FSM의 다음 상태(또는 연속 구성)는 현재 상태와 입력의 함수(전이 함수 또는 전이 관계)로 표현될 수 있다.
이 전체 틀은 이산 함수의 세계에 속한다. 이산 함수는 BDD(이진 의사결정도; 불리언(2값) 함수를 표현하는 자료구조)와 그 확장인 MDD(다중값 의사결정도; 유한값 이산 함수를 표현하는 자료구조)로 편리하게 표현될 수 있다. 우리는 이산 공간에서 필요한 모든 양(더 구체적으로 전이 함수, 입력, 출력, FSM의 상태)을 표현하기 위해 BDD와 MDD를 사용한다. BDD와 MDD가 이산 함수의 효율적 표현이 되려면, 함수의 입력 변수(실제 입력, 출력, 상태)의 좋은 순서를 계산해야 한다. 일반적으로 BDD는 개별 점이 아니라 점들의 집합을 대상으로 동작하며, 이를 상징적 조작(symbolic manipulation)이라 한다.
자동 형식 검증에서 가장 널리 쓰이는 두 방법은 언어 포함과 모델 체킹이다. VIS의 현재 버전은 모델 체킹을 강조하지만, 제한된 형태의 언어 포함(언어 공허성)도 사용자에게 제공한다.
유한 상태 시스템은 라벨이 붙은 상태 전이 그래프로 표현될 수 있는데, 상태의 라벨은 그 상태에서의 원자 명제의 값(예: 래치 값)이다. 시스템에 대한 속성은, 상태 전이 시스템이 그 공식을 “모델”로 삼을 수 있는 시제 논리의 공식으로 표현된다. 모델 체킹은 전이 시스템의 그래프를 순회하면서 해당 속성을 나타내는 공식이 만족되는지 검증하는 과정, 즉 시스템이 그 속성의 모델인지 확인하는 과정이다.
시제 논리는 “
가 언젠가는 성립한다”와 같은 성질을 지정하는 연산자를 통해 시간에 따른 사건의 순서를 표현한다. 시제 논리에는 여러 변종이 있는데, 그중 하나가 계산 트리 논리(CTL)이다. 계산 트리는 상태 전이 그래프로부터 유도된다. 그래프 구조를 초기 상태를 뿌리로 하는 무한 트리로 풀어 전개한다. 그림 3.1은 그래프를 트리로 전개한 예를 보여준다. 이 트리의 경로는 모델링 중인 시스템의 모든 가능한 계산을 나타낸다. CTL의 공식은 모델로부터 유도된 계산 트리를 기준으로 기술된다. CTL은 이 트리의 분기 구조를 설명하는 연산자를 갖기 때문에 분기 시간 논리로 분류된다.
그림 3.1: 상태 전이 그래프의 전개(unwinding).
CTL의 공식은 원자 명제(각 명제는 모델의 변수 하나에 대응), 명제 논리의 표준 불리언 결합자(예: AND, OR, XOR, NOT), 그리고 시제 연산자로부터 구성된다. 각 시제 연산자는 두 부분으로 이루어진다 
: 경로 한정자(
또는 
)와 그 뒤를 잇는 시제 양상(모달리티)(
, 
, 
, 
). 모든 시제 연산자는 암묵적인 “현재 상태”를 기준으로 해석된다. 현재 상태에서 시작하는 시스템의 실행 경로(상태 전이의 시퀀스)는 일반적으로 여러 개가 존재한다. 경로 한정자는 그 모달리티가 그 가능한 모든 경로에서 참이어야 하는지(보편 경로 한정자 로 표시) 아니면 어떤 하나의 경로에서만 참이면 되는지(존재 경로 한정자 로 표시)를 나타낸다. 시제 모달리티는 실행 경로를 따라 시간에 따른 사건의 순서를 기술하며, 그 직관적 의미는 다음과 같다.
(“
가 미래 언젠가 성립한다”로 읽음)는 경로 위의 어떤 상태에서는 공식 이 참이면 참이다.
(“ 가 전역적으로(항상) 성립한다”로 읽음)는 경로의 모든 상태에서 가 참이면 참이다.
(“ 가 다음 상태에서 성립한다”로 읽음)는 현재 상태 바로 다음에 도달하는 상태에서 가 참이면 참이다.
(“ 가 
가 성립할 때까지 성립한다”로 읽음, “강한 until”이라 부름 )는 경로 위의 어떤 상태에서는 가 참이고, 그 이전의 모든 상태에서 가 참이면 참이다.VIS 문서에는 “CTL 문법”이라는 제목의 문서에서 CTL의 문법이 설명되어 있다. 본 장에서는 CTL 공식을 단순화한 문법으로 표기한다. 시스템의 상태는 모든 래치에 저장된 값으로 구성된다. 논리의 각 공식은 주어진 상태에서 참 또는 거짓이며, 그 진리는 하위 공식들의 진리로부터 재귀적으로 평가되어, 결국 주어진 상태에서 참 또는 거짓인 원자 명제에 도달한다. 시스템이 공식을 만족한다는 것은 시스템의 모든 초기 상태에서 그 공식이 참이라는 뜻이다. 만약 속성이 성립하지 않으면, 모델 체커는 실패를 증명하는 실행 경로, 즉 반례를 산출한다. VIS에서도 사용되는 자동 모델 체킹의 효율적 알고리즘은 Clarke 등[7]이 기술하였다. 다음 표는 그림 3.1의 계산 트리에서 공식들의 평가 예를 보여준다.
시제 논리 공식은 해석이 어려울 수 있어, 설계자가 실제로 어떤 속성이 검증되었는지를 이해하지 못할 수 있다. 따라서 하드웨어 검증에서 가장 흔히 사용되는 CTL 구성에 익숙해지는 것이 중요하다.
도달 가능한 모든 상태(
)에서, 그 상태에서 
가 참이면, 반드시 어떤 이후 시점(
)에 
가 참인 상태에 도달해야 한다. 는 시스템의 초기 상태들을 기준으로 해석된다. 는 가 참인 상태를 기준으로 해석된다. 다시 말해, 신호 가 높으면, 결국 도 높아진다는 뜻이다. 흔한 실수는 
를 대신 쓰는 것이다. 전자의 의미는 초기 상태에서 가 참이면, 항상 결국 가 참인 상태에 도달한다는 뜻인 반면, 후자는 가 참인 모든 도달 가능 상태에 대해 조건이 성립해야 함을 요구한다. 만약 가 항등적으로 참이라면, 는 
로 환원된다.
2. 
모든 도달 가능 상태에서, 그 상태에서 시작하는 모든 경로에 대해 반드시 
가 참인 다른 상태에 도달해야 한다. 다시 말해, 는 무한히 자주(asserted infinitely often) 참이어야 한다.
3. 
어떤 도달 가능 상태에서도, 그 상태에서 시작해 
가 참인 상태에 도달하는 경로가 적어도 하나는 존재해야 한다. 다시 말해, 언제나 재시작 상태에 도달할 수 있어야 한다.
4. 
가 성립하지만 
는 성립하지 않는 상태에 도달하는 것이 가능하다.
5. 
항상, 만약 
가 발생하면, 결국 
이 참이 되며, 그때까지는 가 계속 참이어야 한다.
6. 
가 High가 될 때마다, 
는 두 클록 사이클 이내에 High가 된다.
7. 
만약 
가 세 연속 상태에서 참일 수 있다면, 
가 참인 상태에 도달하는 것도 가능하고, 거기에서 두 번 더 진행해 
가 참인 상태에 도달할 수 있다.
다음은 가장 흔한 CTL 템플릿과 그에 대응하는 자연어 의미를 요약한 것이다.
은 “나쁜 일이 결코 일어나지 않는다”(
가 나쁜 것). 모든 상태에서 참이어야 하는 불변식(invariant)을 지정하는 데 사용된다. 부분 정당성(틀린 답을 내지 않음), 상호 배제(두 프로세서가 동시에 임계구역에 있지 않음), 교착 회피(교착 상태에 도달하지 않음)에 유용하다.
은 “결국 시스템이 이 항상 참인 상태들로 제한된다” 또는 “시스템이 이 참인 상태들에서 유한 번만 머문다”는 뜻이다. 시스템의 유한 횟수 실패(finitely many failures) 속성을 명세하는 데 사용할 수 있다.
은 “ 이 참인 모든 도달 가능 상태에서, 좋은 일 
이 결국 일어난다”는 뜻이다. 전 정당성(종료가 결국 일어나면서 올바른 답을 냄), 접근성(요청한 프로세스가 결국 임계구역에 들어감), 기아 회피(대기 중인 프로세서에게 결국 서비스가 제공됨)를 표현하는 데 유용하다. 만약 이 항상 참이면, 이는 
으로 환원된다. 은 “무한히 자주 ”라는 뜻, 즉 어떤 도달 가능 상태에서든 가 참인 상태에 도달해야 한다는 뜻이다. 예컨대 어떤 상태에서든 리셋 조건을 강제하는 데 사용할 수 있다.
은 “좋은 일 이 결국(마침내) 일어난다”( 보다 덜 제한적)라는 뜻이다.
은 “항상 로의 가능성이 있다”는 뜻이다. 예컨대 항상 교착이 없는 상태에 도달할 수 있어야 한다고 요구함으로써 교착 부재를 검출할 수 있다. 이것은 
-자동자로는 표현할 수 없는 CTL 속성의 한 예이다 .
은 시스템의 상태들을 완전히 순회하도록 강제한다.
은 “ 가 가능하다”는 뜻이다. 이것은 또 다른 -자동자로 표현할 수 없는 CTL 속성의 예이다.주의사항
CTL 공식에 등장하는 변수는 레지스터 변수의 함수(예: 상태나 상태에 연결된 출력)여야 한다. 입력 또는 의사 입력(pseudo-input)에 의존하는 변수는 허용되지 않는다. 그렇지 않으면 입력에 따라 와 가 모두 참이 되는 상태가 생길 수 있기 때문이다.
명제 논리 연산자 
(예: 
)는 
와 동치이며, 
에 의해 만족된다. 이를 
대신 사용하지 말라. 후자는 와 가 모두 참일 때이자 그때만 참이다.
CTL과 Verilog의 문법은 다르다. 예를 들어 다음과 같다. Verilog CTL 의미
&& * AND || + OR == = equal a!=NO !(a=NO) not equal -> implies ^ xor
공정성 개념을 도입해야 하는 경우가 자주 있다. 예를 들어 시스템이 여러 사용자에게 공유 자원을 할당하는 경우, 어떤 사용자도 영원히 자원을 독점하지 않는 경로만 고려되어야 한다. CTL 자체만으로는 공정한 경로에서의 정당성에 관한 주장(assertion)을 표현할 수 없다.
Fair CTL은 공정성을 다루기 위해 CTL을 수정한 것이다. Fair CTL은 각 공정성 조건을 주는 CTL 공식으로 표현된 상태 집합인 공정성 제약을 도입하는 것으로 특징지어진다. 공정한 경로(fair path)란 각 공정성 조건이 무한히 자주 만족되는 경로를 말한다. 이러한 종류의 공정성 제약을 뷔히(Büchi)형이라 한다. Street(정확히는 Streett)형과 같은 더 일반적인 공정성 제약은 현재 허용되지 않는다. Fair CTL은 CTL과 동일한 문법을 가지지만, 의미론이 수정되어 모든 경로 한정자가 공정한 경로만을 범위로 삼는다. VIS는 Fair CTL을 지원하며, 문서에서는 때때로 CTL이라고만 부르더라도 실제로는 Fair CTL을 의미하기도 한다.
공정성 조건의 예로 이 있는데, 이는 가 무한히 자주(asserted infinitely often) 참인 경로들로 시스템을 제한한다.
신호등 제어기의 기술(description)이 보이는 모든 동작이 유효한 것은 아니다. 동작을 제한하기 위해 다음 두 가지 공정성 제약을 부과한다. 첫째:
!(timer.state=START); 타이머는 결국 START 상태를 떠나야 한다. 이 제약은 타이머가 영원히 START에 머무르는 것을 방지한다. 둘째 공정성 제약: !(timer.state=SHORT); 이는 타이머가 결국 SHORT 상태를 떠나야 함을 보장한다. 이러한 공정성 제약이 타이머에 부과되지 않으면 활성(liveness) 속성(예: 농로와 고속도로의 차량이 결국 교차함)이 성립하지 않을 수 있다. 명백히 점검해야 할 속성 하나는 두 방향의 신호가 동시에 녹색이 되어서는 안 된다는 것으로, 농로와 고속도로의 교통이 충돌하지 않도록 보장한다. 이 속성은 다음 CTL 공식으로 쓴다:
AG ( !((farm_light = GREEN) * (hwy_light = GREEN)) ); 농로의 차량이 결국 교차로를 통과하도록 보장하려면, 농로에 차량이 있고 타이머가 LONG일 때, 결국 농로 신호가 녹색으로 바뀌어야 한다고 요구한다. CTL로는 다음과 같이 쓴다:
AG(((car_present = YES) * (timer.state = LONG)) -> AF(farm_light = GREEN)); 또한, 농로에서 무엇이 일어나든지와 무관하게, 고속도로는 항상 미래에 녹색이어야 한다:
AG(AF(hwy_light = GREEN)); 농로에 차량이 존재한다고 해서 결국 농로 신호가 녹색이 되는 것이 보장되지는 않는다. 차량이 접근했다가 타이머가 LONG이 되기 전에 물러날 수도 있다. 이 속성은 안전(safety)에 필수는 아니며, 단지 고속도로 신호가 녹색인 시간을 극대화할 뿐이다. 따라서 시스템이 다음 속성을 만족하는 것이 바람직하다:
!(AG((car_present = YES) -> AF(farm_light = GREEN)));
CTL로는 기술할 수 없는 실용적으로 중요한 속성들이 있다. 예 하나가 “거의 항상(almost always)” 속성이다. 어떤 조건 이 유한한 수의 전이 후에는 항상 성립한다(공식 
과 
이 이를 표현하겠지만, 이들은 합법적인 CTL 공식이 아니다). 이 속성은 
과 매우 비슷하지만 동일하지는 않다. 은 참이지만 은 거짓인 전이 시스템을 제시할 수 있다.
한 가지 해법은 더 표현력이 높은 시제 논리(예: 위 속성은 PLTL이나 CTL*에서 표현 가능)를 사용하는 것이다. 그러나 모델 체킹 알고리즘의 복잡도 증가 같은 단점이 있다. 대안으로 -자동자 이론에 기반한 또 다른 검증 패러다임인 언어 포함을 사용할 수 있다. 예를 들어 앞의 “거의 항상” 속성은 자동자를 사용해 쉽게 표현할 수 있다.
현재 VIS는 제한된 형태의 언어 포함을 지원한다. 언어 포함의 아이디어를 간단히 요약하면 다음과 같다. 어떤 시스템이 속성을 만족하려면 
여야 한다. 여기서 
는 시스템을 나타내는 -자동자이고, 
는 속성을 나타내는 -자동자이며, 
는 그 자동자가 받아들이는 언어이다. 사실 는 
와 동치이다.
언어 포함 검사를 수행하기 위해, 주어진 시스템을 속성의 부정(여집합)을 표현하는 모델과 합성한 뒤 언어 공허성을 검사한다. 합성된 시스템의 언어가 공집합일 때이자 그때만 시스템이 속성 을 만족한다.
언어 공허성은 Fair CTL로는 표현할 수 없는 속성을 검증하는 데에만 쓰이지 않고, 추상화된 시스템이 여전히 원래 시스템을 포함하는지 점검하는 데에도 사용된다. 두 경우 모두 어떤 -자동자()를 여집합으로 만드는(보수 취하는) 일이 필요하며, 자동자가 비결정적일 경우(추상화에서는 보통 그렇다) 이는 어렵다. 결정적 속성의 여집합은 쉽지만 비결정적 속성의 여집합은 어려울 수 있다는 사실은 언어 포함의 핵심 난점이다. 이 때문에 표현력과 보수의 난이도가 서로 다른 다양한 부류의 -자동자에 대한 많은 연구가 촉발되었다. 현재 VIS는 비결정적 뷔히 자동자의 언어 공허성을 지원하지만, 주어진 비결정적 속성의 여집합을 도출하는 책임은 사용자에게 있다. 뷔히 자동자의 수용 조건은 무한히 자주 도달해야 하는 상태들이며, 이는 공정성 제약으로 지정된다. 따라서 언어 포함을 사용하려면, 사용자는 Verilog 계층 구조 안에 보수 자동자 구조를 나타내는 모니터를 삽입하고, 보수 자동자의 수용 조건을 지정할 공정성 제약 집합을 부과해야 한다. 즉, 수용 조건은 공정한 경로의 관점에서 지정된다.
마지막으로, VIS 내부에서는 언어 공허성(언어 포함)이 CTL로 환원된다. 즉 시스템(시스템과 보수 속성의 합성)에 대해 CTL 공식 
을 검사한다. 이는 적절한 공정성 제약을 만족하는 무한 경로의 존재 여부에 대한 검사이다(
은 항상 만족된다는 점에 주목하라).
다음: Formal Verification in 위로: 제목 없음 이전: Describing Designs for
_Yuji Kukimoto
1996년 2월 6일 화요일 11:58:14 PST_
