UPPAAL 모델 검사기를 사용하여 게이트 레벨에서 동기 회로를 모델링했습니다. 시계를 모델링 할 수있는 방법에 대한 혼란이 있습니다. 목표는 설정 시간과 대기 시간을 확인하는 것입니다. 위반하지 않았다. appal model checker에서 t = 10, 예를 들어 상승 에지에 해당하는 것과 t = 20과 같은 모델이 테스트 벡터와 비슷하게 보이도록 만드는 모델을 발견했습니다. 누구나 UPAAL에서 동기식 회로를 모델링하는 방법에 대한 기본 예제를 제안 할 수 있습니까? UPPAAL의 모델 싱크로너스 회로 확인
당신이 선언에서이 쓰기 감사합니다
clock t;
broadcast chan rise, fall;
그런 Uppaal의 동기 클록은 다음과 같이 보일 것이다 :
이 가
이
그런 다음 연결된 다른 구성 요소가 rise?와 들어야
fall?.
당신의 설명을 위해 mariusm을 고맙다, 내가 정말로 혼란스러워하는 부분은, 나의 D 플립 플롭 입력이고, 나는 D 플립 플롭 동작의 모델을 가지고있다. 그러나 나는 어떻게 D 플립 플롭 입력을 모델링하는지 모르겠다. 어느 쪽이든 2 상태로 오토마타를 모델링 할 때마다 (지연을 고려하여) 0과 1 사이를 swithching하거나 (첫 번째 "0_logique"상태와 같은 시퀀스로 제공) 다음 X 시간 동안 남아있게됩니다. "1_logique"상태가 유지됩니다. , especiallay 설정 시간을 존중하고 시계의 시간을 잡아 내 입력이 필요합니다. –
@HachaniAhmed, 당신은 더 많은 중간 상태가 필요할 것입니다. 두 개의 위치로 시작한 다음 일어날 일을 모델링하는 입력에 각 이벤트의 가장자리를 추가하십시오. 모든 위치에서 언제든지 입력을 처리 할 수있을 때까지 가장자리를 계속 추가하십시오. 아마도 중간 상태 (대기 상태의 불변량과 경비원을 기다리는 모델)에서 약간의 대기 시간이 필요할 것입니다. 이것은 약간 지루하지만 정상적인 현상입니다. 왜냐하면 실제 전자 장치도 순간적이지 않고 상태를 변경할 시간이 필요하기 때문입니다. – mariusm
시간이 지정된 자동 완성 기능에 익숙해야합니다. Uppaal 튜토리얼을 확인하십시오. 타이밍 다이어그램을 제공 할 수 있다면 몇 가지 시계 가드 및 불변성이있는 상태 시스템으로 모델링하는 것이 매우 간단합니다. – mariusm
답장을 보내 주셔서 감사합니다. @ UPDATE 다이어그램이 어떻게 도움이되는지 잘 모르겠습니다. 실제로 게이트 레벨에서 D 플립 플롭을 모델링하고 설정 시간을 확인하고 시간을 확인합니다. 하지만 모델을 만들 때 나는 모델을 오토마타로 모델링 할 수있는 혼란을 겪었습니다. 지금까지 발견 한 가장 좋은 것은 8 개의 상태 모델과 같은 테스트 벡터로 시계를 제공하고 있기 때문입니다. 가장자리, 테스트 벡터 가능성이 높습니다, 나는 모든 상승 에지에서 D 플립 플롭 동작을 확인할 수 있도록 어떻게 시계 공간을 할 수 있는지 잘 모르겠습니다. –
"테스트 벡터"부분을 이해할 수 없습니다. 동기 클럭에 관해서는 주어진 타이밍 (가드와 불변 변수에 의해'clock' 변수를 사용하여 모델링 됨)에 따라'상승 '과'하강'채널에서 방출하는 하나의 프로세스를 모델링 한 다음 다른 연결된 컴포넌트가들을 것입니다 해당 채널에 적용하고 그에 따라 상태를 업데이트하십시오. – mariusm