In verifying the memory interface of a complex network processor, it is crucial to reduce the number of state variables in the design and the verification time. In this paper, two methods are presented for these purposes. One is to remove the temporal operator ‘NEXT’ for reducing the verification time. The other is to separate data path signals from control path signals and set data path signals as scalar set for reducing the number of state variables. The first method allowed us to reduce the verification time by the factor of 2~100 times by just adding a small number of flip-flops without changing the design. We found a bug using this method. The second method is also found out to be crucial to the success of our work as we could verify the design which could not have been verified otherwise.
형식 검증은 설계의 기능성을 검증하는데 있어 사용되는 하나의 방법이다. 형식 검증은 사양과 구현의 관계를 논리적으로 추론해 냄으로써 검증을 수행한다. 그로 인해, 효과적으로 검증 시간을 줄일 수 있다. 또한, 기존의 기술들로는 발견해내기 힘든 코너케이스에 대하여 조사를 할 수 있기 때문에 사용자들에게 신뢰감을 줄 수 있다. 만약, 시스템이 주어진다면 사양을 만족시키는 모든 가능한 행위를 조사하기 때문이다. 그래서, 형식 검증은 검증에 있어서 주요한 부분이 되고 있다. 그러나, 실제 집적시스템에 있어서 구현의 크기가 커서 형식 검증에 사용되는 모델 체킹(model checking)을 곧바로 사용할 수가 없다. 이것은 상태변수의 수가 많아져 발생하는 상태 폭발(state explosion)에서 비롯된다. 대부분의 경우 상징적 모델 체킹(symbolic model checking)을 이용해 다룰 수 있는 상태변수의 비트(bit) 수는 150-250정도이다.
만약, 네트워크 프로세서의 메모리 경계(memory interface)같은 부분을 검증하고자 한다면 여러 다른 부분들과 연결이 되어 있기 때문에 다루어야 하는 변수의 수가 많게 된다. 이것이 상태 폭발을 야기 시키기 때문에 반드시 상태 변수의 수를 줄여야만 한다. 또한, 변수의 수가 많아질수록 검증하는데 소요되는 시간이 길어지기 때문에 효율적으로 구현을 검증하기 위해선 검증시간을 줄이는 것도 필요하게 된다. 이런 문제들을 해결하기 위해 여러 다른 방법들이 사용되었다. 그 대표적인 것이 추상화인데 이 경우, 사용자가 잘못 추상화를 한다면 그 검증 결과는 실패하게 된다. 그러므로, 정확한 추상화가 이뤄져야 하는데 이런 과정은 매우 복잡하고 많은 시간을 필요로 하게 된다. 그래서, 우리는 이 논문을 통해 위에 열거한 문제점들을 해결하기 위해 2가지 방법을 제시한다. 하나는 넥스트(next)라는 연산자를 제거해 검증 시간을 줄이는 것이고 다른 하나는 제어 경로에 있는 신호들을 데이터 경로에 있는 신호들과 분리해 이를 모델 검증기의 일종인SMV에서 지원하는 스칼라셋(scalar set)으로 정의해 상태변수의 수를 줄이는 것이다. 실제, 우리가 제시한 2가지 방법을 통하여 커다란 모델을 검증할 수 있었으며, 그 과정에서 기존의 방법으론 발견하기 힘들었던 버그(bug)를 발견해 낼 수 있었다.
