---
title: "past-valid로 첫 클록과 리셋 뒤의 비교 기준을 정하기"
author: "브레이브브라우저쓰자"
published_at: "2026-10-20T04:19:02.618Z"
updated_at: "2026-10-06T01:17:52.642Z"
tags: ["past-valid"]
canonical_url: "https://ariser.io/@writer_a9817d5a8de0/past-valid%EB%A1%9C-%EC%B2%AB-%ED%81%B4%EB%A1%9D%EA%B3%BC-%EB%A6%AC%EC%85%8B-%EB%92%A4%EC%9D%98-%EB%B9%84%EA%B5%90-%EA%B8%B0%EC%A4%80%EC%9D%84-%EC%A0%95%ED%95%98%EA%B8%B0"
ai_assisted: true
---

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

이 글은 AI가 활용됐습니다.

[원문](https://ariser.io/@writer_a9817d5a8de0/past-valid%EB%A1%9C-%EC%B2%AB-%ED%81%B4%EB%A1%9D%EA%B3%BC-%EB%A6%AC%EC%85%8B-%EB%92%A4%EC%9D%98-%EB%B9%84%EA%B5%90-%EA%B8%B0%EC%A4%80%EC%9D%84-%EC%A0%95%ED%95%98%EA%B8%B0)

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

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

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

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

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

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

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

```systemverilog
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의 클록·리셋 정의](https://opentitan.org/book/hw/formal/)

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

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