PSL로 VHDL 모듈 형식 검증 마스터하기

안전关键 FPGA 애플리케이션용 VHDL 설계 시 단순 테스트벤치 작성은 불충분합니다. 엔지니어는 숨겨진 부작용 없이 모듈이 명세대로 정확히 동작함을 증명해야 합니다. 형식 검증이 그 수학적 보장을 제공합니다.

형식 검증은 요구사항과 구현 간 간극을 메워 모든 가능한 입력 시퀀스가 설계 속성을 만족함을 증명합니다. DO-254 인증이 필요한 의료 기기, 항공전자 시스템 등 모든 도메인에서 필수적입니다.

이 게스트 포스트에서 숙련된 형식 검증 실무자 Michael Finn Jørgensen이 실용적 통찰과 실행 가능한 팁을 공유합니다. 아래 예제는 친숙한 AXI FIFO 튜토리얼 How to make an AXI FIFO in block RAM using the ready/valid handshake를 기반으로 PSL을 실제 VHDL 설계에 적용하는 방법을 시연합니다.

형식 검증이란?

형식 검증(FV)은 합성 전 체계적 방법으로 모든 입력 조합에 대한 설계 정확성을 보장합니다. 수동 작성 자극에 의존하는 기존 테스트벤치와 달리 FV는 매 클록 사이클마다 유지돼야 할 속성(property)을 명시합니다. SAT 솔버가 이 속성들이 충족됨을 철저히 증명하거나, 아니면 반례(counter-example)로 정확히 지적합니다.

FV를 구동하는 두 핵심 기법:

Bounded Model Checking (BMC) – 리셋부터 시작해 유한 사이클 수 검사.
귀납 증명(Induction Proof) – 상태가 유효하면 이후 모든 상태도 유효함을 검증. 완전한 속성 세트 필요하지만 무한 사이클 보장.

BMC는 몇 개 속성만으로 실행 가능해 흔히 1차 방어선으로 쓰입니다. 귀납은 더 까다롭지만 절대적 확실성 제공.

왜 형식 검증을 사용하는가?

FV는 전체 입력 공간을 자동 탐색해 찾기 힘든 버그를 발굴하는 데 탁월합니다. 결함 발견 시 도구가 정확한 위반 사이클을 짚어내는 간결한 파형 생성—긴 시뮬레이션 트레이스 디버깅보다 훨씬 쉽습니다.

FV가 강력한 단위 테스트 도구이나 수작성 통합 테스트를 대체하진 않습니다. 모듈 크기 증가 시 솔버 런타임이 감당하기 힘들 수 있습니다. 그럼에도 FV 투자 시간이 전체 디버깅 노력 감소와 타임투마켓 단축으로 이어집니다.

PSL로 속성 작성하기

PSL(Property Specification Language)은 VHDL 형식 검증의 링구아 프랑카입니다. 속성은 보통 솔버가 검증 단계에서 읽는 별도 .psl 파일에 저장합니다.

속성을 기술하는 세 PSL 키워드:

assert – 조건이 항상 성립함을 보장
assume – 입력에 대한 가정 기술
cover – 특정 시나리오 발생 가능성 확인

PSL 파일에는 일반 VHDL 선언과 프로세스도 포함 가능, 복잡한 단언을 위한 보조 신호 생성에 활용.

모든 PSL 파일은 특정 엔티티와 연결하는 vunit 블록으로 시작:

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) { }

기본 클록 선언이 뒤따름:

default clock is rising_edge(clk);

속성 문법:

LABEL : assert always {PRECONDITION} |-> {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-> {POSTCONDITION}

다음 사이클 단언엔 |=> 사용:

LABEL : assert always {PRECONDITION} |=> {POSTCONDITION}

조건 내에서 stable로 신호가 사이클 간 불변 강제, {C1; C2}로 순차 제약 체인 표현 가능.

필수 도구 설치

상용 도구(예: ModelSim)가 형식 검증 지원하나 무료 Student Edition엔 미포함. 다행히 Linux(Windows는 WSL 경유)용 견고한 오픈소스 스택 사용 가능. 다음 가이드는 Ubuntu 20.04 LTS 기준이나 최근 Debian 계열이면 모두 작동.

사전 요구사항

sudo apt update && sudo apt upgrade

필수 개발 라이브러리 설치:

sudo apt install build-essential clang bison flex libreadline-dev \
gawk tcl-dev libffi-dev git mercurial graphviz \
xdot pkg-config python python3 libftdi-dev gperf \
libboost-program-options-dev autoconf libgmp-dev \
cmake gnat gtkwave

Yosys와 SymbiYosys

git clone https://github.com/YosysHQ/yosys
cd yosys; make; sudo make install; cd ..
git clone https://github.com/YosysHQ/SymbiYosys
cd SymbiYosys; sudo make install; cd ..
git clone https://github.com/SRI-CSL/yices2
cd yices2; autoconf; ./configure; make; sudo make install; cd ..

GHDL과 Yosys 플러그인

git clone https://github.com/ghdl/ghdl
cd ghdl; ./configure --prefix=/usr/local; make; sudo make install; cd ..
git clone https://github.com/ghdl/ghdl-yosys-plugin
cd ghdl-yosys-plugin; make; sudo make install; cd ..

예제 프로젝트 다운로드

아래 양식 작성해 AXI FIFO 소스, PSL 파일, 검증 스크립트 포함 ZIP 수령.

실전 예제: AXI FIFO 형식 검증

아래에서 FIFO 핵심 속성 범주와 PSL 인코딩 방법을 개괄합니다.

리셋 처리

f_reset : assume {rst};

always 키워드 생략으로 이 가정은 리셋 후 첫 사이클에만 적용. 라벨 관례(f_)로 실패 식별 용이.

f_after_reset_valid : assert always {rst} |=> {not out_valid};
f_after_reset_ready : assert always {rst} |=> {in_ready};
f_after_reset_head : assert always {rst} |=> {count = 0};

vunit 선언에 아키텍처 이름 포함돼 count 같은 내부 신호 참조 가능.

FIFO Full/Empty 신호

f_empty : assert always {count = 0} |-> {not out_valid};
f_full : assert always {count = ram_depth-1} |-> {not in_ready};

AXI 프로토콜 준수

f_in_data_stable : assume always {in_valid and not in_ready and not rst} |=> {stable(in_valid) and stable(in_data)};
f_out_data_stable : assert always {out_valid and not out_ready and not rst} |=> {stable(out_valid) and stable(out_data)};

레디 신호 안정성:

f_out_ready_stable : assume always {out_ready and not out_valid and not rst} |=> {stable(out_ready)};
f_in_ready_stable : assume always {in_ready and not in_valid and not rst} |=> {stable(in_ready)};

FIFO 순서 보장

먼저 쓴 데이터가 나중에 쓴 데이터보다 먼저 나감을 보장. 특정 데이터 값이 진입/나간 시점 기억하는 보조 신호로 모델링.

signal f_sampled_in_d1 : std_logic := '0';
signal f_sampled_in_d2 : std_logic := '0';
p_sampled : process (clk) begin
if rising_edge(clk) then
if in_valid then
if in_data = f_value_d1 then f_sampled_in_d1 <= '1'; end if;
if in_data = f_value_d2 then f_sampled_in_d2 <= '1'; end if;
end if;
if out_valid then
if out_data = f_value_d1 then f_sampled_out_d1 <= '1'; end if;
if out_data = f_value_d2 then f_sampled_out_d2 <= '1'; end if;
end if;
if rst = '1' then
f_sampled_in_d1 <= '0'; f_sampled_in_d2 <= '0';
f_sampled_out_d1 <= '0'; f_sampled_out_d2 <= '0';
end if;
end if;
end process p_sampled;

데이터 값을 비제약 상수로 선언해 솔버가 임의 비트 패턴 선택 가능하게:

signal f_value_d1 : std_logic_vector(ram_width - 1 downto 0);
signal f_value_d2 : std_logic_vector(ram_width - 1 downto 0);
attribute anyconst : boolean;
attribute anyconst of f_value_d1 : signal is true;
attribute anyconst of f_value_d2 : signal is true;

순서 제약 인코딩:

f_fifo_ordering_in : assume always {f_sampled_in_d2} |-> {f_sampled_in_d1};
f_fifo_ordering_out : assert always {f_sampled_out_d2} |-> {f_sampled_out_d1};

형식 검증 실행

sby 도구용 axi_fifo.sby 스크립트 생성:

[tasks]
bmc
[options]
bmc: mode bmc
bmc: depth 10
[engines]
smtbmc
[script]
ghdl --std=08 -gram_width=4 -gram_depth=8 axi_fifo.vhd axi_fifo.psl -e axi_fifo prep -top axi_fifo
[files]
axi_fifo.psl
axi_fifo.vhd

검증 실행:

sby --yosys ";yosys -m ghdl" -f axi_fifo.sby

성공 시 출력:

[axi_fifo_bmc] DONE (PASS, rc=0)

depth를 FIFO 깊이 초과로 조정해 솔버가 풀 용량 시나리오 탐색 보장.

변이 테스트

속성 세트 완전성 검증 위해 의도적으로 작은 버그 주입(예: out_valid 구동 로직 제거) 후 FV 재실행. 솔버가 단언 실패 보고하면 해당 에러를 잡을 만큼 속성이 표현력 있음 입증.

실패 메시지 예:

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable

생성된 trace.vcd를 GTKWave로 열어 정확한 위반 사이클 확인.

Cover 문장

Cover 문장은 특정 시나리오 도달 가능성 단언에 유용. 예: FIFO가 채워졌다 비워지는 것 검증:

f_full_to_empty : cover { rst = '1'; rst = '0'[*]; rst = '0' and count = ram_depth-1; rst = '0'[*]; rst = '0' and count = 0};

sby 스크립트에 cover 태스크 포함:

[tasks]
bmc
cover
[options]
bmc: mode bmc
bmc: depth 10
cover: mode cover

성공적 커버리지 결과:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.

count = ram_depth-1을 count = ram_depth로 변경하면 커버 불가능해져 도구의 속성 정확도 민감성 입증.

다음 단계

VUnit 101: 자동화된 VHDL 검증을 위한 실용 가이드 Xilinx Vivado 마스터하기: ILA(통합 로직 분석기) & VIO(가상 입출력) 디버깅

VHDL