일반기술

반복적 과도 근사 도달 상태 계산 방법 및 장치

본 발명은 디지털 집적회로의 정상적 동작 중에는 절대 도달 불가능한 상태 또는 그러한 도달 불가능한 상태의 일부를 계산해내는 과도근사도달상태 계산 알고리즘(Over-approximate reachable state computation algorithm)의 근사 성능 개선을 위한 방법이다. 그 내용은 기존의 과도근사도달상태 계산을 더 이상의 성능 개선이 없을 때까지 여러번 반복 적용하되, 단순히 같은 초기 조건으로부터 여러 번 계산을 반복하는 것이 아니라, 매번 구하여진 중간 계산 결과를 이후의 반복 계산마다 활용하여 최종 계산 결과의 정확도를 향상시키도록 하는 것이다.본 발명은 과도근사도달상태 계산시 회로 표현용 자료구조로 BDD(Binary Decision Diagram)가 사용되는 경우를 대상으로 하고 있으며, 매번 구하여진 이전의 근사 계산 결과를 이용하여, 계산에 많이 사용되는 상태천이관계 BDD의 크기를 대폭 축소함으로써, 분석대상회로를 분할할 필요가 없게 하거나 또는 분할이 불가피 할 경우 최소의 분할만을 통하여 전체분석이 가능하게 하여 근사 성능을 대폭 향상시킨다.본 발명에 따르면, 종래의 근사도달상태는 그 근사의 질이 현저히 떨어져 유용한 정보를 도출할 수 있는 가능성이 현저히 떨어지는 문제점을 해결하고, 근사도달상태의 근사 질 향상을 통하여 통하여 대규모 디지털 집적회로 설계시 논리합성단계에서 활용되어 설계 결과물의 동작속도 향상이나 소요 게이트 수의 현저한 감소를 이룰 수 있다.또한, 본 발명은 과도근사된 도달 상태 계산 결과를 하드웨어의 오류를 찾아내는 정형검증에 적용할 수 있으며, 이 경우도 종래의 근사도달상태를 사용하는 경우는 실제 도달 가능상태보다 너무나 많은 상태를 도달 가능한 것으로 판명하여 그에 기반 한 검증 결과는 지나치게 보수적일 수 있다는 기존의 문제점을 극복할 수 있음으로써, 본 발명 결과를 활용할 경우 보다 정밀하게 회로의 오류를 찾아낼 수 있다.