past-valid로 첫 클록과 리셋 뒤의 비교 기준을 정하기

형식 검증에서 첫 클록에만 실패하는 속성을 만나면 회로의 초기화부터 의심하기 쉽다. 그런데 q == $past(d)라는 비교의 오른쪽에는 아직 존재하지 않는 과거가 들어갈 수 있다. 회로가 데이터를 잘못 저장했는지 판단하기 전에, 그 데이터를 비교할 만큼의 이력이 실제로 만들어졌는지 확인해야 한다. past-valid는 이 경계를 속성 안에 명시하는 작은 상태다.

첫 샘플에는 이전 샘플이 없다

$past(d)는 같은 샘플링 클록에서 한 번 전 관측한 d를 뜻한다. 현재 시간에서 임의의 나노초를 빼거나, 가장 최근에 신호가 바뀐 값을 찾는 함수가 아니다. SymbiYosys의 formal 확장 문서는 첫 클록의 $past에는 초기값이 주어지지 않는다고 설명한다. 이 값을 당연히 0이라고 생각하면, 도구의 초기 모델과 사람이 의도한 명세가 어긋난다. SymbiYosys의 과거 값 설명

예를 들어 입력을 매 클록 저장하는 8비트 레지스터가 있다고 하자. 리셋은 클록 상승 에지에서만 적용되는 동기식이며, 리셋이면 q를 0으로 만든다. 그 밖에는 d를 저장한다. 이 회로의 정상 동작은 이전 에지에서 캡처한 d가 현재 에지 직전의 q와 같다는 관계로 표현할 수 있다.

여기에는 두 조건이 필요하다. 이전 에지를 실제로 관측했어야 하고, 그 에지에서 리셋 대신 데이터를 저장했어야 한다. 현재 리셋 중인 에지도 정상 데이터 전달 검사를 적용할 구간에서 제외할 수 있다. 단순히 현재 rst가 0이라는 조건 하나로는 앞의 두 조건을 모두 설명하지 못한다.

검사하는 시점과 저장하는 시점을 구분하기

다음은 위 가상 회로와 함께 사용하는 clocked immediate assertion의 예다. past-valid는 회로의 출력이 아니라 검증용 이력 표시다.

reg [7:0] q;
always @(posedge clk)
  if (rst) q <= 8'd0;
  else     q <= d;

reg past_valid = 1'b0;
always @(posedge clk) begin
  past_valid <= !rst;
  if (past_valid && !rst)
    assert(q == $past(d));
end

비차단 대입은 그 에지의 검사가 끝난 뒤 상태를 갱신한다. 따라서 if에서 읽는 past_valid는 방금 대입한 !rst가 아니라 이전 에지에서 저장한 값이다. q도 현재 d를 저장하기 전 값이다. 이 코드에서는 past_valid가 1이면 이전 에지가 리셋이 아니었음을 함께 알 수 있다. 별도로 $past(rst)를 조건에 넣지 않아도 되는 이유다.

순서를 따라가 보자. 에지 0에서 rst=1이면 검사하지 않고 q=0, past_valid=0을 저장한다. 에지 1에서는 rst=0, d=7이라고 하자. 에지 직전 q는 0이지만 past_valid가 아직 0이므로 데이터 전달 검사를 건너뛰고 q=7을 저장한다. 에지 2의 d가 9일 때는 q=7, past_valid=1, $past(d)=7이다. 비교가 성립한 뒤 q가 9로 바뀐다.

현재 d=9와 q=7을 비교했다면 정상 회로에서 실패했을 것이다. 반대로 첫 정상 에지의 $past(d)를 임의의 0으로 간주해 검사를 통과시켰다면, 유효한 전달을 확인한 것이 아니다. 이력의 유효성과 비교 대상의 샘플링 시점은 함께 정의해야 한다.

리셋 뒤에 다시 쌓아야 하는 이력

동작 중 에지 3에서 리셋을 다시 넣으면 past_valid는 0으로 돌아간다. 에지 4에서 리셋을 풀고 d=4를 넣는 순간에는 정상 데이터 검사를 건너뛴다. 에지 5에서 q=4인지 비교하면서 새 동작 구간의 검사를 시작한다. 리셋 전 마지막 입력을 리셋 후 첫 출력의 기준으로 섞지 않는 구조다.

그렇다고 리셋 동작을 검증한 것은 아니다. 이 속성은 의도적으로 리셋과 그 직후의 데이터 비교를 제외한다. 리셋 에지 다음 상태가 정말 0인지, 필요한 신호가 언제 알려진 값이 되는지는 별도 속성으로 검사해야 한다. past-valid를 넣었다는 이유로 초기화 버그까지 덮어서는 안 된다.

OpenTitan의 assertion 매크로도 속성에 사용할 클록과 리셋 조건을 명시한다. 표준 매크로의 disable iff가 검사를 비활성화하는 모습은 참고할 만하지만, 그것이 모든 과거 값에 필요한 이력을 자동으로 만들어 주는 기능은 아니다. OpenTitan assertion의 클록·리셋 정의

이 예는 하나의 클록과 동기식 리셋에 한정된다. 에지 사이에 짧은 비동기 리셋이 들어오는 회로라면 그 사건을 검증용 상태가 놓치지 않도록 별도로 설계해야 한다. 다른 클록에서 얻은 과거 값도 현재 클록의 한 주기 전 값과 같은 뜻으로 사용할 수 없다. 두 주기 전 입력을 비교하는 속성이라면 한 비트가 아니라 필요한 만큼의 연속 유효 이력을 확보해야 한다.

첫 클록의 실패를 없애는 것만이 목적이라면 속성을 넓게 비활성화하는 방법도 있다. 그러나 그러면 언제부터 무엇을 검사했는지 흐려진다. past-valid를 사용할 때는 처음과 리셋 직후에 제외되는 에지, 실제 데이터 관계가 시작되는 에지를 나란히 써 보면 좋다. 그 표가 회로의 동작과 맞을 때, 초기 반례를 단순한 잡음으로 버리지 않고 회로 오류와 속성 오류를 구별할 수 있다.