실습: 카운터의 리셋·순환·불변식 검증

실험 대상과 관찰 조건

초기값을 3으로 두고 첫 상승 에지^{i상승 에지 클록이 0에서 1로 바뀌는 순간입니다. CLK=1인 구간 전체를 뜻하는 레벨과 구별합니다. 자세히 보기}에서 리셋^{i리셋 상태를 명세한 초기값으로 돌리는 제어입니다. 동기식인지 비동기식인지, 다른 제어보다 우선하는지를 함께 정해야 합니다. 자세히 보기}합니다. 이후 0, 1, 2, 3, 0으로 진행합니다. 리셋 신호가 켜져 있어도 클록 에지 전에는 값이 그대로입니다.

시작하기 전에

Digital Design Studio의 Desktop 프로젝트와 정상 실행 권한을 준비하세요. 각 예제는 별도 폴더의 rtl/top.sv로 저장합니다.

SystemVerilog 소스

module top (
    input logic clk,
    input logic rst,
    output logic [1:0] count
);
    // Active-high synchronous reset: sampled only at the rising clock edge.
    always_ff @(posedge clk)
        if (rst) count <= 2'b00;
        else count <= count + 2'b01;
endmodule

실행 방법

New analysis에서 Two-state single-clock v1을 선택하세요. Clock port는 clk, 주기는 1000ps입니다. 아래 값으로 Preflight 후 Run RTL simulation을 실행하고 결과를 비교하세요.

입력 자극

[
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  }
]

각 열은 한 상승 에지의 관찰 기록입니다. 입력은 에지 직전, 이름에 after가 붙은 상태는 갱신 직후 값입니다. 열의 정렬은 샘플 순서를 나타내며 물리적인 전파 지연^{i전파 지연 입력이 바뀐 뒤 출력이 올바른 값으로 안정되기까지 걸리는 시간입니다. 논리식의 등가성과 시간 특성은 별개입니다. 자세히 보기}을 그린 것이 아닙니다. E0~E4는 각각 500, 1500, 2500, 3500, 4500ps의 상승 에지입니다. 최종값뿐 아니라 중간 count 열도 전부 비교하세요.

결과 비교

5 cycles · count=00. 500, 1500, 2500, 3500, 4500ps에서 00 → 01 → 10 → 11 → 00을 확인하세요.

이 실습은 0/1 단일 클록 RTL을 사용합니다. #delay·initial·X/Z 테스트벤치는 포함하지 않습니다. 학습 완료 표시는 학습 기록이며 실제 시뮬레이션 결과를 뜻하지 않습니다.

기대 상태를 에지 단위로 계산합니다

초기 레지스터^{i레지스터 여러 비트의 상태를 저장하는 회로입니다. 이 과정의 동기식 레지스터는 클록 에지에서 정해진 입력을 저장합니다. 자세히 보기} 값은 3이지만 첫 상승 에지에서는 리셋이 우선합니다. 초기화와 리셋을 같은 것으로 취급하지 마세요.

리셋이 없는 구간에서는 다음 관계가 매 에지에 성립해야 합니다.

최종값 00만 확인하면 중간에 잘못된 값을 거쳐도 통과할 수 있습니다. 상태열 전체와 리셋 우선순위를 따로 검사하세요.

실험을 한 번에 하나씩 바꿉니다

• 초기값을 00으로 바꿔도 첫 리셋 이후의 상태열은 같습니다. 이 결과로 리셋이 초기값에 의존하지 않는지 확인합니다.
• Reset cycles를 2로 바꾸면 첫 두 상승 에지의 count가 모두 00이어야 합니다. 이후 증가 시작 시점이 한 에지 늦어집니다.
• 폭을 3비트로 확장한다면 순환 주기는 8회 증가입니다. 선언만 바꾸지 말고 상수 폭, 초기 레지스터 배열, 실행 길이도 함께 검토합니다.

modulo-10 설계로 일반화합니다

4비트 저장소는 0부터 15까지 표현합니다. 따라서 단순 증가만으로는 9 다음에 0이 되지 않습니다. 다음 상태 함수를 별도로 정해야 합니다.

이 정의는 사용하지 않는 상태 10~15에서 enable이 들어오면 0으로 복귀시킵니다. 다른 복구 정책도 가능하지만 명세와 검증 모델이 같은 정책을 사용해야 합니다.