liveness: 100사이클 뒤의 응답과 영원한 대기는 다르다

요청을 받아들인 회로가 100사이클 동안 응답하지 않았다. 아직 기다리는 것일까, 영원히 멈춘 것일까. 관측한 100사이클만으로는 이후에 응답하는 경우와 계속 멈춰 있는 경우를 구별할 수 없다. 대신 명세가 ‘8사이클 안에 응답’이라고 요구했다면 이미 위반을 확정할 수 있다.

liveness는 필요한 일이 결국 일어난다는 성질이다. 시간 제한이 있는 응답 요구와 같은 말로 쓰면 증명 범위가 달라진다.

유한한 실패와 끝없는 실패를 나눈다

‘존재하지 않는 요청의 응답을 내보내지 않는다’는 safety 성질이다. 잘못된 응답 하나가 나온 순간 유한한 기록으로 위반을 보여 줄 수 있다. ‘수락한 모든 요청은 결국 완료된다’는 liveness 성질이다. 아무리 긴 유한 대기도 그 다음에 완료될 가능성은 남아 있다.

설명용 단일 요청 모듈을 생각하자. 요청을 수락하면 pending이 1이고, 응답 valid는 완료할 때까지 유지된다. valid와 외부 ready가 함께 1인 edge에 완료되며 pending이 0이 된다. 이 요청 동안 reset은 없고 새 요청도 없다고 정한다.

여기서 DUT는 응답을 계속 제시하지만 환경이 ready를 영원히 0으로 둘 수 있다. 그러면 완료는 영원히 일어나지 않는다. DUT가 valid를 유지한다는 사실과 시스템에서 전송이 결국 완료된다는 사실은 다르다.

SBY 공식 문서는 unbounded safety 검사용 prove와 liveness 검사용 live를 별도로 제공한다. 지원하는 engine과 frontend의 속성 문법도 확인해야 하며, mode 이름만 바꾸어 모든 속성이 자동으로 처리된다고 생각해서는 안 된다. YosysHQ SBY, Options 및 Engines section

환경이 영원히 막지 않는다는 가정이 필요할 수 있다

위의 모듈에서 ready가 무한히 자주 1이 된다는 환경 조건을 둔다고 하자. DUT가 미완료 응답을 계속 제시하고 요청을 잃지 않는다면, pending 동안 이후의 ready=1과 만나 완료할 수 있다. 이는 환경의 진행 조건과 DUT의 유지 보장을 함께 사용한 결론이다.

ready가 한 번이라도 1이었다는 조건은 충분하지 않다. 그 한 번이 요청을 받기 전이라면 이후 영원한 stall이 가능하다. 요청이 기다리는 동안의 진행을 설명하는 조건이어야 한다.

반대로 ‘DUT의 응답이 결국 나온다’를 환경 가정으로 넣고 같은 응답 발생을 증명하면 검사하려던 의무를 먼저 가정한 셈이다. 환경의 준비 여부와 DUT의 응답 생성 책임을 분리한다. 회로가 pending을 조용히 버리거나 valid를 내리는 오류는 별도의 유지·완료 조건으로 잡아야 한다.

SBY의 현재 live 준비 흐름은 일반 safety assertion을 assumption으로 바꾼다. 따라서 요청을 잃지 않는다는 safety 조건을 같이 적었다고 해서 live 실행이 그 조건 자체까지 증명했다고 읽으면 안 된다. 그 조건을 별도 safety 검사로 확인한 근거와 함께 완료 증명을 해석해야 한다. SBY, 모델 준비 구현

여러 요청이 진행 중이면 aggregate한 활동도 조심한다. 다른 요청이 계속 완료되는 상황에서 특정 요청 하나만 영원히 남을 수 있다. ‘언젠가 응답 하나가 있다’보다 각 수락 요청이 명세에 맞게 끝나는지를 정의해야 한다. 필요한 식별과 순서 계약이 그 성질의 일부다.

결국 완료해도 마감 시각은 어길 수 있다

환경 조건이 ready를 무한히 자주 올리도록 해도 첫 ready의 시점을 제한하지는 않을 수 있다. 요청을 0번째에 수락하고 ready를 1~99번째에 0, 100번째에 1로 하면 100번째에 완료한다. 이후에도 ready가 반복해서 1이 되도록 하면 무한한 진행 조건을 만족할 수 있다.

마지막 행은 100번째 완료 edge를 아직 포함하지 않은 관측 구간을 뜻한다. 시점의 포함 여부를 명시해야 같은 숫자로 다른 기록을 섞지 않는다.

8사이클 제한은 위반 여부를 유한한 기록에서 확인할 수 있는 bounded response 요구다. 이를 결국 완료한다는 성질로 바꾸면 시간 요구를 약화한다. 필요한 명세가 마감이라면 환경도 어느 기간 안에 준비해야 하는지, DUT 자체가 어느 기간 안에 valid를 만들어야 하는지를 나누어 정의한다.

timeout은 결론의 이름을 바꾸지 않는다

검증 실행의 wall-clock timeout도 회로의 응답 마감과 다르다. solver가 계산에 오래 걸려 중단되었다면 해당 속성에 대한 증명을 완료하지 못한 것이다. 회로가 정한 사이클 수를 넘긴 것과 같은 실패로 보고하지 않는다.

시뮬레이션의 대기 timeout 역시 설정된 기간의 응답 부재를 보여 준다. 실제 명세의 deadline과 일치하면 기능 위반의 근거가 될 수 있지만, 단순히 실행을 유한하게 만들기 위한 임의 제한이라면 영원한 정지를 증명한 것은 아니다.

liveness 검증의 가정은 실제 시스템이 보장해야 한다. 외부 장치가 무한히 준비되지 않을 수 있는데 준비를 가정하고 완료를 증명했다면, 그 결과는 조건부다. 무한한 진행 조건으로 얻은 결론을 일정한 성능이나 최대 지연으로 확대하지 않는다.

100사이클 뒤의 응답과 영원한 대기는 서로 다른 실행이다. liveness는 후자를 배제하려는 질문이고, 마감 검사는 늦은 전자도 배제하려는 질문이다. 환경이 제공하는 진행과 DUT의 책임, 시간 제한을 따로 적어야 원하는 완료 성질을 정확히 검증할 수 있다.