KR19990077472A - 모델검사용동작환경을자동적으로생성하는방법 - Google Patents

Abstract

본 발명은 모델 검사용 동작환경을 자동적으로 생성하는 방법에 관한 것이다. 디자인의 시뮬레이션 중 포착된 상태천이에 대하여 모델검사를 사용함으로써 테스트중인 디자인의 검증을 자동적으로 향상시키는 방법이 제공된다. 포착된 모든 개별 천이가 시뮬레이션 중 사용되지만, 이들 천이의 모든 가능한 시퀀스가 반드시 시뮬레이션 중 사용되지는 않고, 이 사용되지 않은 시퀀스에 버그가 숨겨져 있을 수 있기 때문에 향상된 검증이 가능하다. 모델검사기의 비결정적이며 철저한 특성에 의하여 포착된 상태천이로 이루어지는 모든 가능한 시퀀스가 사용되는 것이 보장된다. 본 발명의 방법론은 상태천이의 활용과 이들 상태천이(시뮬레이션중 관측됨)를 유발하는 입력으로 구성되어, 모델검사기가 테스트중인 디자인에 인가될 수 있는 올바른 입력을 비결정적이며 철저하게 정의한다.

Description

모델 검사용 동작환경을 자동적으로 생성하는 방법 {METHOD FOR AUTOMATICALLY GENERATING BEHAVIORAL ENVIRONMENT FOR MODEL CHECKING}

본 발명은 일반적으로 정보처리시스템에 관한 것이며, 특히 로직시스템(logic system)의 자동화된 형식검증(formal verification)에 관한 것이다.

다양한 종류의 전자장치가 계속 증가하고 있어서, 전자장치를 동작시키는 직접회로 또는 칩(chip)의 수요 또한 계속 확대되고 있다. 소형화 되는 칩에 새로운 기능을 구현하거나 여러 기능을 통합함으로 해서 주어진 시간 내에 용이한 방법으로 새로운 칩 디자인을 검증하여 이 칩 디자인이 디자인 사양(specification)과 디자인 규칙에 따라 동작하는지 보장하기 어렵다. 트랜지스터 소자가 소형화하고, 칩에 다양한 기능이 요구됨에 따라서 매우 많은 트랜지스터 소자가 포함된 새로운 집적회로가 나타나고 있다. 이러한 다양한 종류의 새롭게 디자인된 집적회로 모델을 검증하는 절차가 매우 크므로, 디자인 플로우 중 검증에 가장 많은 시간이 소요된다.

디지털시스템을 검증하는 종래의 방법은 시뮬레이션(simulation)이다. 테스트중인 모델에 인가할 입력 시퀀스를 생성하고, 시뮬레이션 실행 중 디지털시스템이 적절히 동작하는지 정확성 검출기(correctness checker) 또는 수작업으로 검증한다. 이 방법론(methodology)은 단순하지만 디자인의 복잡성이 증가하면, 시뮬레이션 시간이 지수적으로 증가하기 때문에 디자인을 완전히 검증하는 것은 실현 불가능하다. 또한 로직의 복잡성이 증가하면 시간적으로 적절한 방법으로 수행될 수 있는 시뮬레이션 양이 산출하는 수행범위(total coverage)는 매우 낮다.

시뮬레이션 수행범위 문제 때문에, 형식검증이 매우 널리 사용되고 있다. 형식검증은 구현된 로직디자인이 그 디자인 명세를 충족시키고 있는지 엄격하게 검증하는 절차이다. 시뮬레이션의 목적 또한 형식검증과 같지만, 시뮬레이션은 엄격하지 않다. 모델검사(model checking)가 형식검증의 대표적 형태(form)이다.

모델검사에 있어서, 가장 시간이 소비되는 노력중의 하나가 동작환경(behavioral environment)을 제공하여 테스중인 유닛에 대한 마이크로구조상의 인터페이스(microarchitectural interface)를 모델링하는 것이다. 종래 이 노력은 수개월이 소요됐으며, 수작업이므로 오류가 발생하는 경향이 있었다. 따라서 검증은 원하는 시점보다 상당히 늦게 시작될 수 있으며, 검증엔지니어는 많은 시간을 검증에 소비하고, 설계자는 오류가 발생하기 쉬운 환경에 의하여 생성된 이러한 "그릇된 실패(false fail)"를 제거하려고 노력한다.

디지털디자인은 필요한 기능을 구현한 "상태기계(state machine)"의 컬렉션(collection)으로 구성된다. 이 상태기계는 상태의 집합(초기상태를 포함), 입력의 집합, 출력의 집합 및 상태천이함수(state transition function)로 구성되는 추상적 기계(abstract machine)로 정의될 수 있다. 천이함수는 현 상태와 입력을 취하여 새로운 출력의 집합과 다음 상태를 반환한다. "출력값"과 "상태"사이에 1 대 1 대응관계가 있기 때문에, 이하에서 "상태"만을 언급한다. 상태기계는 또한 입력 이벤트(input event)의 순서화된 시퀀스를 대응하는 상태의 시퀀스로 사상(map)하는 함수로써 생각될 수 있다.

주어진 시점에서 순차 디지털디자인의 상태는 디자인내 다양한 상태기계가 가지는 상태들을 교차곱(cross product)한 것이다. 이것을 이하에서 "적(積)상태기계(product state machine)"라 부른다. 주어진 입력에 의한 현 상태로부터 다음 상태로 천이를 나열하는 상태천이표는 이러한 순차 디자인의 모든 기능을 정의할 수 있다. 그러나 순차 디자인의 검증은 상태천이의 검증뿐만 아니라 검사되고 있는 직접회로에 의하여 주사(traverse)될 수 있는 상태천이의 모든 유효 시퀀스를 필요로 한다. 모델 검사 툴이 상태천이의 모든 시퀀스를 검증할 수 있다. 상태천이의 시퀀스를 이하에서 "워크(walk)" 또는 "트레이스(trace)"라 부른다. "워크" 또는 "트레이스"는 혼용된다.

따라서 직접회로 디자인의 모델검사에 필요한 환경적 동작입력(environment behavioral inputs)을 자동적으로 생성하는 개선된 방법이 필요하다.

디자인의 시뮬레이션 테스트중 포착된 상태천이에 대하여 모델검사를 사용함으로써 디자인의 검증을 향상시키는 방법이 제공된다. 이러한 방법론은, 예시적 실시예에서, 상태천이의 활용과 이들 상태천이(시뮬레이션중 관측됨)를 유발하는 입력으로 구성되어, 모델검사기가 테스트중인 디자인에 인가할 수 있는 올바른 입력을 비결정적이며(non-deterministically) 철저하게(exhaustively) 정의한다.

도 1은 본 발명을 설명하는데 유용한 예시적 회로 디자인을 예시하는 단순화된 개략도.

도 2는 도 1에 예시된 회로내 점 또는 노드(node)에서 로직상태에 의하여 정의되는 다양한 회로상태의 조건에 대한 예시도면.

도 3은 상태기계의 다양한 상태 간에 천이 경로(path)를 도시하는 예시적 상태천이도.

도 4는 입력변화에 따른 상태의 변화를 예시하는 예시적 천이관계표.

도 5는 시뮬레이션중 얻어진 "트레이스"의 기록을 예시하는 표.

도 6은 다양한 입력이 인가됨에 따라 회로상태 간의 여러 가지 예시적 트레이스를 예시하는 도면.

도 7은 시뮬레이션 트레이스로부터 자동적으로 형식적 환경을 발생하는 방법의 개요를 도시하는 흐름도.

첨부된 도면과 함께 본 발명의 바람직한 실시예를 고려하면 본 발명을 좀더 잘 이해할 수 있다.

인터페이스 레벨의 형식환경을 코딩함에 있어서 개시된 방법론이 효과적으로 구현된다. 본 방법론은 테스트중인 디자인의 천이표가 시뮬레이션중인 디자인의 동작을 관찰하여 구축될 수 있고, 역으로 천이표가 모델검사를 위하여 동일 디자인의 입력을 구동하도록 사용될 수 있다는 사실에 기초한다. 이 역천이표(inverted transition table)가 일부이지만 유효한 입력제약(input constraint) 집합을 모델검사에 제공한다. 시뮬레이션중 관측된 상태 "x"로부터의 모든 천이는 가능한 입력 벡터로 부호화되므로, 테스트중인 모델이 "x"상태에 있을 때 형식환경이 이 입력벡터를 모델에 인가할 수 있다. 주어진 천이표로부터, 모델검사가 모든 가능한 상태천이 "워크" 또는 "트레이스"－여기서 워크 또는 트레이스는 시뮬레이션중 관측된 천이로 구성됨－에 대하여 디자인을 철저하게 검증할 수 있으며, 따라서 모델검사가 잠재적인 버그(potential bug) 또는 이들 천이 워크중에 나타날 수 있는 디자인 문제를 발견할 수 있다. 모델검사기(model checker)가 수행하는 각각의 개별 천이가 비록 시뮬레이션으로부터 포착되지만, 주어진 천이관계에서 가능한 모든 실질적 워크에 대하여 시뮬레이션할 필요는 없다(이들 모든 워크에 대한 시뮬레이션을 하려면 시뮬레이션 실행회수가 지수적으로 증가하여 실현 불가능하다).

테스트중인 디자인의 상태기계가 가지는 천이표는 시뮬레이션 트레이스 파일로부터 매 주기별로 입력 및 상태값을 관측하여 구축된다. 시뮬레이션 주기가 "i"일 때, 주어진 입력 I_i, 주어진 상태 S_i가 관측되고, 주기 "i+1"에서 상태가 천이표의 엔트리를 완성한다. 주어진 시뮬레이션이 실행되는 동안 적상태기계는 모든 가능한 상태천이를 나타내지는 않지만, 매우 많은 주기 후에 올바른 천이의 대다수가 관측되고 기록된다. 수행범위 해석(coverage analysis)을 사용하여 모든 시뮬레이션 집합 중 포착되는 상태천이 에지(edge)의 퍼센트를 결정할 수 있다.

이상과 같이 포착된 상태천이표는 각 상태에 대하여 그 상태에서의 시뮬레이션중 나타난 입력벡터의 리스트를 부여하는 기능을 한다. 이 기능은 디자인의 입력을 구동하도록 사용될 수 있다. 모델검사기는 주어진 상태에 대하여 가능한 입력 벡터들로부터 입력벡터를 "비결정적으로" 선택한다. 시뮬레이션은 "결정적"이므로 주기 "i"에서 임의 주어진 상태 "x"에 대하여, 시뮬레이터(simulator)는 실행중인 테스트 케이스에 의하여 고정된 단일의 입력벡터를 인가한다. 모델검사는 "비결정적이어서" 주기 "i"에서 임의 주어진 상태 "x"에 대하여 하나 이상의 가능한 천이가 존재하며, 모델검사기는 이 주어진 상태로부터 모든 가능한 천이를 조사한다. 이러한 모든 가능한 천이를 체계적으로 조사하여, 모델검사기는 천이관계로 이루어진 모든 가능한 워크를 고려한다. 따라서 이 모델검사 환경에서 사양을 검사하는 것이 시뮬레이션 실행으로부터 얻을 수 있는 것 이상의 검증을 산출한다.

개시된 기술의 이점이 기능 모델(functional model)을 시뮬레이션에 사용할 수 있으면(이것은 구현 레벨에서 모델검사가 응용될 수 있는 가장 빠른 단계임) 모델검사를 시작할 수 있는데 있다. 표준 시뮬레이션 트레이스 설비를 사용하여 테스트 중인 유닛 또는 제품을 시뮬레이션 환경 내에 장치하고 테스트 중인 디자인에 대한 래치값과 입력 신호의 데이터를 주기별로 수집한다. 상태기계의 디자인에 사용되는 래치값은 자동적으로 또는 디자이너(designer)에 의하여 디자인 소스(source)로부터 추출될 수 있다. 시뮬레이션이 반복 실행되면, 상태천이에 관한 부가적인 데이터가 사용되어 모델검사 테스트중인 유닛을 구동하는 역상태기계의 기능을 증가시킬 수 있다. 이 시간동안, 모든 기능을 가지는 형식환경의 개발이 일반적으로 진행되어, 결과적으로 자동화된 모델을 대신하여 시뮬레이션중 간과될 수 있는 상태천이의 수행범위를 제공한다. 시뮬레이션중 상태천이 트레이스 또는 워크가 시뮬레이션 되지 않지만 자동적으로 생성된 형식환경과 함께하는 모델검사기는 시뮬레이션중 관찰되는 천이로 이루어진 모든 가능한 트레이스에 대하여 사양을 철저하게 검사하여 존재할지 모르는 "버그"를 노출시키기 때문에, 모델검사기와 함께하는 자동화된 형식환경이 시뮬레이션보다 수행범위가 넓다. 만일 시뮬레이션으로부터 전혀 관측된바 없는 천이로 이루어진 트레이스가 존재한다면, 수동환경(manual environment)은 이러한 트레이스를 생성할 수 있는 부가적 이득을 제공할 수 있다.

상기 개시된 방법은 대규모이며 복잡한 시뮬레이션 모델의 임의 서브유닛을 선택하여 철저하게 검증할 수 있다. 테스트중인 특정 유닛에 대하여 포착된 트레이스가 시뮬레이션중인 유닛과 완전히 일치할 필요는 없지만, 전체 시뮬레이션 모델보다 작거나 동일한 크기의 서브유닛이 될 수 있다. 하나 이상의 유닛으로 이루어진 시스템용으로 시뮬레이션 환경 및 테스트 케이스 생성 툴이 개발된다. 시스템을 철저하게 시뮬레이션하기 위하여 이들 툴이 사용된다. 천이관계 데이터가 대규모 시스템 모델이 가지는 하나 이상의 서브유닛용으로 추출될 수 있어 각 개별 서브유닛용으로 개별적 시뮬레이션 환경과 테스트 케이스 생성 툴을 구축할 필요가 없다.

도 1은 입력 I(1) 내지 I(n)을 수신하고, 출력 O(1) 내지 O(m)을 제공하지만, 입출력의 동일한 번호간 특별한 관계가 없는 테스트중인 회로(101)를 도시하고 있다. 테스트중인 회로(101)는 예를 들어서, 로직 어레이(logic array)(103,113)와 이 로직 어레이(103,113) 사이에 연결된 래치 LA1(105)과 LA2(107)를 포함한다. 회로(101)에 대한 입력이 변화함에 따라, 래치장치(LA1,LA2)의 상태 또한 변화한다. 이들 래치의 다음 상태(즉 트리거되었을 때 래치가 가지는 값)는 래치의 현재값과 입력의 함수이다. 래치(105,107)가 각각 "1" 또는 "0"의 두 가지 가능한 로직상태중 하나의 상태에 있으며 따라서 래치(105,107)의 조합에 의하여 4가지 즉 상태 "a", "b", "c" 및 "d"가 가능하다. 이 상태는 도 2의 표에 도시되어 있다. 상기 래치(105,107)로부터의 출력이 각각 노드 N1과 N2로 연결되고, 이 노드의 출력은 다시 제1 로직 어레이(103)와 제2 로직 어레이(113)에 인가된다. 제2 로직 어레이(113)가 O(1)내지 O(m)의 출력신호를 제공한다. 일정 경우에는, O(1) 내지 O(m)의 출력은 현 상태 N1과 N2 뿐만 아니라 현재의 입력 I(1) 내지 I(n)의 함수이기도 하다. 이러한 케이스를 "밀리(Mealy)"기계라 하며, 본 명세서에 개시된 기술은 또한 이들 기계에도 사용될 수 있다.

도 3은 예시적인 상태천이도를 예시한다. 상태천이도는 상태를 나타내는 원과 상태간 천이를 나타내는 직선부분으로 구성된다. 하나 이상의 동작(action) 또는 출력이 각 천이 및/또는 상태와 연관될 수 있다. 예시된 상태천이도는 유한상태기계(Finite State Machine: FSM)를 나타낸다. 도시된 바와 같이, 상태 "a"(301), 상태 "b"(305), 상태 "c"(309), 상태 "d"(313)의 4가지 상태가 있다. 예에 있어서, 상태기계의 상태는 상태 "a"(301)에서 로직 "0"의 입력에 의하여 상태 "b"(305)로 변화 또는 천이(303)한다. 상태는 상태 "b"(305)에서 로직 "0" 입력에 의하여 상태 "c"(309)로 변화 또는 천이(307)한다. 상태는 상태 "c"(309)에서 로직 "1" 입력에 의하여 상태 "a"(301)로 천이(319)하고, "0" 입력에 의하여 상태 "d"(313)로 천이(311)한다. 상태는 상태 "d"(313)에서 로직 "1" 입력에 의하여 상태 "a"(301)로 상태변화 또는 천이(315)한다. 상태는 상태 "a"(301)에서 로직 "1" 입력에 의하여 상태 "c"(309)로 천이(317)한다.

본 방법론의 이점을 예시하기 위하여 도 3에서 "0-0-0-1-1-1"의 테스트 케이스를 실행하여 "a-b-c-d-a" 및 "a-c-a"의 상태천이 "워크"를 유발하는 시뮬레이션을 가정한다. 관측된 천이로부터, 비록 워크 "a-b-c-a"와 "a-c-d-a"가 시뮬레이션중 관측되지 않지만, 이들 워크를 생성하는 것은 가능하다는 것을 알 수 있다. 만일 워크 "a-b-c-a"가 시뮬레이션중 관측되지 않았지만 버그를 예시한다면, 관측된 워크 "a-b-c-d-a 및 "a-c-a"에 기초하여 자동화된 형식환경은 모델검사기가 비결정적으로 두 개의 입력값중 하나를 선택하여 상태 "c"에서의 다음 상태를 결정할 수 있음을 예시하며, 따라서 자동적으로 "a-b-c-a"를 조사한다. 만일 이 워크로부터 에러를 검사하기 위한 규칙을 사용할 수 있다면, 이 에러는 검출된다.

도 3에 도시된 상태기계가 가지는 천이관계표가 도 4에 도시되어 있다. 이 표는 일반적으로 입력벡터를 인가하고 상태기계의 천이결과를 관측하여 시뮬레이션의 실행으로부터 개발된다. 도 5는 2회의 시뮬레이션 실행에 의하여 얻어진 트레이스를 예시한다. 매 주기(클록)마다 상태비트(state bit)와 입력비트(input bit) 모두가 추적(trace)된다. 클록 "i"에서의 각 상태-입력 쌍(클록 "i+1"에서의 결과 상태와 결합됨)은 천이관계표의 엔트리로 이루어진다. 현재 상태, 현재 입력 및 다음 상태로 구성된 한 벌(triplet) 각각은 일단 반드시 기록될 필요가 있어서 시뮬레이션 트레이스 내부 또는 트레이스간에 많은 용장성(redundancy)이 있다.

도 6은 모델검사기 프로그램이 조사할 "워크"를 도시한다. 도 5의 시뮬레이션에 나타난 천이에 따라서, 모델검사기는 상태 "a"로부터 상태 "b"로 천이(601)를 유발하는 입력 "0"과 상태 "c"로 천이(605)를 유발하는 입력 "1"중 하나를 선택 할 수 있다. 상태 "c"에서 "0" 입력은 상태 "d"로 천이(607)를 유발하고, "1"입력은 상태 "a"로 천이(609)를 유발한다. 존재가 알려진 가능한 각 경로를 "트레이스" 또는 "워크"라 한다. 도 6을 참조하여 예를 들어 설명하면, 일 "트레이스"는 상태 "a"로부터 상태 "b"를 거쳐 상태 "c"로 천이하여 그 후로 계속 다음 상태로 천이하는 경로를 포함한다. 다른 경로는 "a-c-d"를 포함하며 또 다른 경로는 "a-c-a"를 포함한다. 다양한 상태를 통과하는 서로 다른 경로 각각은 다른 트레이스를 구성한다. 각 시뮬레이션 실행은 이 천이 트리의 천이열(series of transition)의 단일 직경로(straight path)에 대응하지만, 매 상태에 기초하여 정당한 입력의 비결정적 선택을 활용하여 본 자동화된 형식환경은 모델검사기로 하여금 시뮬레이션에 나타난 천이로 구성된 모든 가능한 워크를 조사하도록 할 수 있다. 모델검사기는 도 6에 도시된 바와 같이, 모든 가능한 경로 또는 "브랜치(branch)"를 병렬로 조사한다.

본 명세서에 개시된 방법론을 달성하기 위한 흐름도가 도 7에 도시된다. 도 7에 있어서, 처리절차중 첫 단계는 도시된 바와 같이 "시뮬레이션 실행" 기능(701)이다. 예를 들어서, 시뮬레이터는 도 3의 상태도로 표현된 디자인에 대하여 시뮬레이션을 실행하여 가능한 상태천이를 시험한다. 다음 단계는 트레이스 생성(703)이며, 이 후에 천이관계정보가 형성된다(705). 상기 트레이스 생성 단계는 시뮬레이션중 관측되는 입력 및 상태정보를 포착한다.

그 후에, 단계(707)에 도시된 바와 같이 모델의 FSM 카피(copy)가 상기 정보로부터 얻어진다. 이 FSM 카피는 도 3의 그래프 또는 도 4의 표로 표현될 수 있다. 다음 단계(709)로 표시된 바와 같이, 상기 FSM에 대하여 입력을 구동하기 위한 형식환경이 구축된다. 이 형식환경은 매 상태에 기초하여 어떠한 정당한 입력이 구동될 수 있는지 정의한다. 예를 들어서, 도 4의 데이터를 사용하면 현 상태 "a"에서 입력 "0"(상태기계의 다음 상태를 "b"로 만듦) 또는 입력"1"(상태기계의 다음 상태를 "c"로 만듦)이 구동될 수 있다. 상태 "b"에서는 오직 입력 "0"(상태기계의 다음 상태를 "c"로 만듬)만이 구동될 수 있다. 기본적으로, 모델검사기는 단계(709)에서 생성된 정의를 사용하여 어떤 입력 값이 주어진 임의 주기에서 모델에 인가될 수 있는지 결정한다(단계(707)에서 모델의 FSM 카피의 상태로부터 결정되었기 때문에, 실제 모델의 천이를 차단함). 모델검사기가 상기 결정을 달성하는 방법은 정당한 값을 상기 모델의 입력에 인가하는 것이다(단계(709)의 정의로부터 결정된 것과 같음). 이 관점에서 모델검사기는 비결정적 시뮬레이션으로 생각될 수 있다. 즉 주어진 임의 주기에서 모델검사기는 값의 집합 중 하나를 상기 모델의 입력에 인가할 수 있다(모델검사기는 모든 가능한 선택을 고려함). 그 후, 테스트중인 모델과 함께 단계(707, 709)에서 정의된 환경이 형식검증 툴에 인가되어 단계(715)에서 표시된 바와 같이 디자인의 버그를 발견한다.

본 발명의 방법 및 장치는 본 명세서에 개시된 바람직한 실시예와 함께 설명되었다. 비록 본 발명의 실시예가 상세하게 설명되고 도시되었지만, 당해 기술분야의 통상의 지식을 가진 자는 본 발명과 함께 본 발명의 개시를 포함하는 많은 변형된 실시예를 용이하게 구성할 수 있으며, 또한 프로세서, CPU 또는 다른 대형 시스템의 직접회로 또는 칩에 포함시키거나 집적시킬 수 있다. 이 방법론은 또한 전적으로 CD, 디스크 또는 디스켓(고정되었거나 이동할 수 있는 것), 또는 다른 메모리 또는 저장장치에 프로그램 코드로 구현되어 기술된 바와 같이 기능하도록 실행될 수 있다. 따라서 본 발명은 명세서에 개시된 특정 형태에 한정됨을 의미하지 않으며, 본 발명의 사상 및 범위내에 합리적으로 포함될 수 있는 변형, 변경 및 균등물을 포함한다.

본 명세서에 개시된 방법은 상태천이에 대한 모델검증을 사용하여 디자인의 검증을 향상시키는 효과를 제공한다.

Claims (24)

1. 로직디자인의 모델검사에 사용되는 동작환경을 제공하기 위한 정보처리방법에 있어서,

   a) 상기 로직디자인에 시뮬레이션 입력 신호를 사용하여 시뮬레이션 테스트를 수행하는 단계;

   b) 상기 시뮬레이션 테스트에 의한 상태천이를 식별하는 단계; 및

   c) 상기 상태천이를 사용하여 상기 로직디자인의 모델검사과정에 사용될 모델입력환경(model input environment)을 제공하는 단계

   를 포함하는 정보처리방법.
2. 제1항에 있어서,

   a) 상기 상태천이로부터 상태천이표를 구축하는 단계; 및

   b) 상기 상태천이표를 확장하여 상기 모델입력환경으로 이루어지는 모델입력의 확장된 집합을 제공하는 단계

   를 더 포함하는 정보처리방법.
3. 제2항에 있어서, 상기 모델입력환경으로 이루어지는 모델입력이 비결정적 방법으로 상기 천이표를 확장하여 개발되는 방법.
4. 제2항에 있어서, 상기 천이표를 구축하는 단계가

   a) 상기 시뮬레이션 테스트중 관측되는 모든 상태로부터 모든 천이를 식별하는 단계; 및

   b) 상기 모델입력환경에 사용되는 가능한 입력벡터를 식별하기 위하여 상기 천이를 부호화하는 단계

   를 포함하는 정보처리방법.
5. 제4항에 있어서, 상기 천이를 식별하는 단계가 상기 시뮬레이션 천이표로부터 매 주기별로 시뮬레이션 입력과 시뮬레이션 상태 값을 식별하는 단계를 더 포함하는 정보처리방법.
6. 제4항에 있어서, 상기 모델입력환경에 상기 확장된 입력집합을 제공함에 있어서, 상기 입력 벡터들로부터 소정의 입력벡터들을 선택하는 단계를 추가로 포함하는 정보처리방법.
7. 제6항에 있어서, 상기 모든 입력벡터가 상기 모델입력환경의 제공에 사용되는 정보처리방법.
8. 제3항에 있어서, 상기 천이표를 구축하는 단계가

   a) 상기 시뮬레이션 테스트중 관측되는 모든 상태로부터 모든 천이를 식별하는 단계; 및

   b) 상기 모델입력환경에 사용되는 가능한 입력벡터를 식별하기 위하여 상기 천이를 부호화하는 단계

   를 포함하는 정보처리방법.
9. 제8항에 있어서, 상기 천이를 식별하는 단계가 상기 시뮬레이션 천이표로부터 매 주기별로 시뮬레이션 입력과 시뮬레이션 상태 값을 식별하는 단계를 더 포함하는 정보처리방법.
10. 제8항에 있어서, 상기 모델입력환경에 상기 확장된 입력집합을 제공함에 있어서, 상기 입력 벡터들로부터 소정의 입력벡터들을 선택하는 단계를 더 포함하는 정보처리방법.
11. 제10항에 있어서, 상기 모든 입력벡터가 상기 모델입력환경의 제공에 사용되는 정보처리방법.
12. 기계가 판독할 수 있는 표시를 포함하는 저장매체에 있어서,

    a) 상기 로직디자인에 시뮬레이션 입력 신호를 사용하여 시뮬레이션 테스트를 수행하는 단계;

    b) 상기 시뮬레이션 테스트에 의한 상태천이를 식별하는 단계; 및

    c) 상기 상태천이를 사용하여 상기 로직디자인의 모델검사과정에 사용될 모델입력환경을 제공하는 단계

    를 수행하여,

    상기 저장매체가 선택적으로 결합되는 판독장치는 상기 기계가 판독할 수 있는 표시를 판독하여 그 판독내용을 표시하는 프로그램 신호를 제공하도록 선택적으로 동작되며, 상기 프로그램 신호는 처리시스템 내의 처리회로―여기서 처리회로에는 상기 판독장치가 선택적으로 결합됨―로 하여금 정보를 처리하여 로직디자인의 모델검사에 사용되는 동작환경을 제공하도록 하는 저장매체.
13. 제12항에 있어서,

    상기 프로그램 신호는

    a) 상기 상태천이로부터 상태천이표의 구축; 및

    b) 상기 상태천이표를 확장하여 상기 모델입력환경으로 이루어지는 모델입력의 확장된 집합의 제공

    에 대해 더욱 유효한 저장매체.
14. 제13항에 있어서, 상기 모델입력환경으로 이루어지는 모델입력이 비결정적 방법으로 상기 천이표를 확장하여 개발되는 저장매체.
15. 제13항에 있어서,

    상기 프로그램 신호는

    a) 상기 시뮬레이션 테스트중 관측되는 모든 상태로부터 모든 천이의 식별; 및

    b) 상기 모델입력환경에 사용되는 가능한 입력벡터를 식별하기 위하여 상기 천이의 부호화

    에 대해 더욱 유효한 저장매체.
16. 제15항에 있어서, 상기 프로그램 신호는 상기 시뮬레이션 천이표로부터 매 주기별로 시뮬레이션 입력과 시뮬레이션 상태 값의 식별에 더욱 유효한 저장매체.
17. 제15항에 있어서, 상기 프로그램 신호는 상기 모델입력환경에 상기 확장된 입력집합을 제공함에 있어서, 상기 입력 벡터들로부터 소정의 입력벡터들의 선택에 더욱 유효한 저장매체.
18. 제17항에 있어서, 상기 모든 입력벡터는 상기 모델입력환경의 제공에 사용되는 저장매체.
19. 제14항에 있어서,

    상기 천이표를 구축하는 단계는

    a) 상기 시뮬레이션 테스트중 관측되는 모든 상태로부터 모든 천이를 식별하는 단계; 및

    b) 상기 모델입력환경에 사용되는 가능한 입력벡터를 식별하기 위하여 상기 천이를 부호화하는 단계

    를 포함하는 저장매체.
20. 제19항에 있어서, 상기 천이를 식별하는 단계가 상기 시뮬레이션 천이표로부터 매 주기별로 시뮬레이션 입력과 시뮬레이션 상태 값을 식별하는 단계를 추가로 포함하는 저장매체.
21. 제19항에 있어서, 상기 프로그램 신호는 상기 모델입력환경에 상기 확장된 입력집합을 제공함에 있어서, 상기 입력 벡터들로부터 소정의 입력벡터들의 선택에 더욱 유효한 저장매체.
22. 제21항에 있어서, 상기 모든 입력벡터가 상기 모델입력환경의 제공에 사용되는 저장매체.
23. 제1항에 있어서, 상기 모델은 다수의 서브 유닛으로 구성되며, 상기 모델의 상태천이는 상기 모델의 서브 유닛으로부터 추출되는 방법.
24. 제12항에 있어서, 상기 모델은 다수의 서브 유닛으로 구성되며, 상기 모델의 상태천이는 상기 모델의 서브 유닛으로부터 추출되는 저장매체.