PSL을 사용한 VHDL 형식 검증

안전이 중요한 FPGA 애플리케이션을 위해 VHDL을 설계할 때 최선을 다해 테스트벤치를 작성하는 것만으로는 충분하지 않습니다. 모듈이 의도한 대로 작동하고 바람직하지 않은 부작용 없이 작동한다는 증거를 제시해야 합니다.

형식 검증 기술을 사용하면 요구 사항을 테스트에 매핑하여 VHDL 모듈이 사양을 준수하는지 증명할 수 있습니다. 의료 애플리케이션을 검증하거나 항공 FPGA 솔루션에 대한 DO-254 인증을 획득하기 위한 도구입니다.

VHDLwhiz는 공식적인 검증을 이해하기 위해 Michael Finn Jørgensen의 도움을 받아 이 게스트 게시물을 작성했습니다. Michael은 해당 주제에 대한 상당한 경험이 있으며 GitHub 페이지에서 많은 팁을 공유합니다.

이 기사의 다운로드 가능한 예제에서 테스트 중인 장치는 기존 튜토리얼에서 가져온 것입니다.
준비/유효한 핸드셰이크를 사용하여 블록 RAM에서 AXI FIFO를 만드는 방법

Michael이 여기에서 인계하고 이 블로그 게시물의 나머지 부분에서 공식 확인에 대해 설명하겠습니다.

공식 확인이란 무엇입니까?

공식 검증(FV)의 목적은 모듈이 의도한 대로 작동하는지 확인하는 것입니다!

FV는 모듈을 합성하기 전에 개발 프로세스의 일부로 수행하는 것입니다. 때로는 "속성 검사"라고 하는 것이 더 나은 설명이라고 생각합니다.

FV에서는 속성을 지정합니다. 모듈이 있어야 하며, 그러면 도구("만족도 솔버"라고 함)가 증명할 것입니다. 모듈이 가능한 모든 입력 시퀀스에 대한 속성을 충족하는지 확인 .

즉, 도구는 유효한 상태(모든 속성이 충족되는 경우)를 무효 로 상태(하나 이상의 속성이 위반되는 경우). 이러한 전환이 없는 경우, 즉 유효하지 않은 상태로 전환할 방법이 없는 경우 속성이 항상 충족되는 것으로 입증되었습니다.

FV의 과제는 도구가 이해할 수 있는 언어로 모듈의 속성을 표현하는 것입니다.

공식 검증은 수동으로 작성된 테스트벤치의 대안입니다. 공식 검증과 수동 테스트벤치의 목표는 디자인에서 버그를 제거하는 것이지만 공식 검증은 속성을 검사하고 다양한 테스트벤치를 자동으로 생성하여 이를 수행합니다.

도구는 두 가지 방법을 사용합니다.

BMC(Bounded Model Checking) . 재설정부터 시작하여 고정된 수의 클록 주기를 검사합니다.
귀납 증명 . 임의의 유효한 상태에서 시작하여 모든 후속 상태도 유효한지 확인합니다.

귀납 증명은 모든 속성을 명시해야 하는 반면 BMC는 몇 가지 속성으로 실행할 수 있으며 여전히 유용한 결과를 제공합니다.

공식 인증을 사용하는 이유

공식 검증은 찾기 힘든 버그를 잡는 데 아주 좋습니다! 공식 검증은 가능한 입력의 전체 공간을 자동으로 검색하기 때문입니다.

이는 손으로 자극을 만들어야 하는 전통적인 테스트벤치 작성과 대조적입니다. 수동으로 작성된 테스트벤치를 사용하여 전체 상태 공간을 탐색하는 것은 사실상 불가능합니다.

또한 공식 검증이 버그를 발견하면 버그를 보여주는 매우 짧은 파형을 생성하고 수동으로 작성된 테스트벤치를 기반으로 시뮬레이션을 실행할 때보다 훨씬 빠르게 수행합니다. 이 짧은 파형은 일반적으로 시뮬레이션에서 발생하는 매우 긴 파형보다 디버그하기가 훨씬 쉽습니다.

그러나 공식적인 검증은 테스트벤치 작성을 대체할 수 없습니다. 내 경험에 따르면 형식 검증은 단위 테스트에 적합하지만 손으로 만든 테스트 벤치를 사용하여 통합 테스트를 수행하는 것이 좋습니다. 공식 검증의 런타임이 모듈의 크기에 따라 기하급수적으로 증가하기 때문입니다.

공식 검증과 관련된 학습 곡선이 실제로 있지만 시간을 할애할 가치가 있으며 이 블로그 게시물이 학습 곡선을 극복하는 데 도움이 되기를 바랍니다. 디자인을 더 빨리 완료하고 버그가 줄어들 것입니다!

PSL에서 속성을 작성하는 방법

형식 검증을 할 때 PSL(Property Specification Language)을 사용하여 모듈의 속성을 표현해야 합니다. 속성은 일반적으로 끝이 .psl인 별도의 파일에 있습니다. , 이 파일은 정식 검증 시에만 사용됩니다.

이 섹션에서는 일반적인 용어로 PSL 언어의 주요 기능을 설명하고 이후 섹션에서는 구체적인 예를 통해 작업하겠습니다.

PSL에는 다음과 같은 세 가지 명령문이 있습니다.

assert
assume
cover

assert 키워드는 이미 익숙할 것입니다. 테스트벤치를 작성할 때. 이 동일한 키워드는 PSL에서도 사용되지만 구문이 약간 다릅니다. assert 키워드는 이 모듈이 항상 만족한다고 약속하는 속성을 설명하는 데 사용됩니다. 특히 assert 키워드는 모듈의 출력 또는 내부 상태에도 적용됩니다.

assume 키워드는 이 모듈이 입력에 부과하는 모든 요구 사항을 설명하는 데 사용됩니다. 즉, assume 키워드는 모듈에 대한 입력에 적용됩니다.

cover 키워드는 어떤 방식으로든 달성할 수 있어야 하는 속성을 설명하는 데 사용됩니다.

신호 선언 및 프로세스(동기 및 조합 모두)를 포함하여 PSL 파일에 일반 VHDL 코드를 작성할 수도 있습니다.

PSL 파일의 첫 번째 줄은

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {

여기 ENTITY_NAME 및 ARCHITECTURE_NAME 확인 중인 모듈을 참조하십시오. INSTANCE_NAME 당신이 좋아하는 무엇이든 될 수 있습니다. 파일은 닫는 중괄호로 끝나야 합니다. } .

.psl의 다음 줄 파일은 다음과 같아야 합니다.

default clock is rising_edge(clk);

이렇게 하면 각 속성 설명에서 클록 신호를 참조해야 하는 지루한 작업을 피할 수 있습니다.

assert 구문 및 assume 문은 다음과 같습니다.

LABEL : assert always {PRECONDITION} |-&gt; {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-&gt; {POSTCONDITION}

이 문은 다음과 같습니다. PRECONDITION 홀드(모든 클록 주기에서) 다음 POSTCONDITION 동일한 조건을 충족해야 합니다. 클록 주기.

일반적으로 사용되는 또 다른 형식이 있습니다.

LABEL : assert always {PRECONDITION} |=&gt; {POSTCONDITION}

이 문은 다음과 같습니다. PRECONDITION 홀드(모든 클록 주기에서) 다음 POSTCONDITION 다음에서 충족되어야 합니다. 클록 주기.

두 형식 모두 광범위하게 사용됩니다.

PRE- 내 및 POST-CONDITIONS , 키워드 stable를 사용할 수 있습니다. . 이 키워드는 this의 값을 의미합니다. 클럭 주기는 이전의 값과 동일합니다. 클록 주기.

PRE- 내 및 POST-CONDITIONS , 다음과 같이 작성하여 시퀀스도 사용할 수 있습니다.

{CONDITION_1 ; CONDITION_2}

즉, CONDITION_1 이에 만족해야 합니다. 클록 주기 및 해당 CONDITION_2 다음에 만족해야 합니다. 클록 주기.

표지 구문은 다음과 같습니다.

LABEL : cover {CONDITION}

이 블로그 뒷부분의 작업 예제에서 이러한 모든 명령문의 많은 예제를 볼 수 있습니다.

필요한 도구 설치

ModelSim을 비롯한 주요 도구 공급업체는 형식 검증을 지원합니다. 불행히도 ModelSim의 학생용 에디션은 공식 검증을 지원하지 않습니다. 실제로 다음과 같은 오류가 발생합니다.

따라서 정식 인증을 위해 ModelSim을 사용하려면 유료 라이선스가 필요합니다.

대신 공식 검증을 수행할 수 있는 오픈 소스(무료) 도구가 있습니다. 이 섹션에서는 이러한 도구의 설치 과정을 안내해 드리겠습니다.

이 가이드에서는 Linux 플랫폼에서 실행 중이라고 가정합니다. Windows 플랫폼을 사용하는 경우 Linux용 Windows 하위 시스템(WSL)을 사용하는 것이 좋습니다. 다음 가이드는 Ubuntu 20.04 LTS를 사용하여 검증되었습니다.

전제조건

먼저 최신 패치를 받으려면 시스템을 업데이트해야 합니다.

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

요시스 외.

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 외.

GHDL용으로 미리 패키징된 바이너리가 있지만 최신 소스 파일을 다운로드하여 다음과 같이 컴파일하는 것이 좋습니다.

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 ..

예제 프로젝트 다운로드

이 기사의 다음 섹션에서는 기존 VHDL 프로젝트에 대한 공식 검증을 구현하는 방법을 안내합니다. 아래 양식에 이메일 주소를 입력하면 전체 코드를 다운로드할 수 있습니다.

공식 검증을 사용한 예제

다음 섹션에서는 이 블로그에서 이전에 작성된 axi_fifo 모듈을 공식적으로 확인하는 방법을 설명합니다.

공식 검증을 시작하려면 FIFO에 어떤 속성이 있는지 자문해야 합니다. 4가지 범주의 속성을 확인했습니다.

재설정 처리:재설정 후 모듈이 잘 정의된 상태로 깨어나도록 합니다.
FIFO 가득 참 및 비어 있음 신호:FIFO가 가득 차고 비어 있는 상태를 올바르게 표시하는지 확인합니다.
AXI 프로토콜:모듈이 AXI 유효/준비 핸드셰이크의 요구 사항을 충족하는지 확인합니다.
FIFO 정렬:FIFO는 이를 통과하는 요소를 삭제/복제/재정렬하지 않습니다.

다음에서 이러한 각 속성에 대해 설명하겠습니다.

초기화 처리

먼저 모듈이 한 클럭 주기 동안 재설정될 것으로 예상한다고 선언합니다.

f_reset : assume {rst};

always 키워드가 없다는 점에 유의하세요. . always 없이 키워드, 명령문은 첫 번째 클록 주기 동안만 유지됩니다.

각 공식 성명에 레이블을 지정하는 것이 일반적이며 매우 유용합니다. 공식 검증을 실행할 때 도구는 실패를 보고할 때 이러한 레이블을 다시 참조합니다. 이러한 모든 레이블 앞에 f_을 사용하는 규칙을 사용합니다. .

그런 다음 재설정 후 FIFO가 비어 있어야 한다고 명시합니다.

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

내부 포트뿐만 아니라 모듈의 신호. 여기서 count를 참조합니다. , 현재 채우기 수준, 즉 현재 FIFO에 있는 요소 수입니다. PSL 파일의 첫 번째 줄에 있는 아키텍처 이름을 참조하기 때문에 가능한 것입니다.

또는 FIFO로 들어오고 나가는 요소 수를 계산하는 PSL 파일에 별도의 프로세스를 가질 수 있습니다. 그것이 선호되지만 내부 카운트 신호를 사용하여 이 블로그 게시물을 짧고 요점으로 유지하겠습니다.

FIFO 가득 참 및 비어 있음 신호

AXI FIFO 신호가 가득 차고 비어 있는 방식은 out_valid을 사용하는 것입니다. 및 in_ready 신호. out_valid 신호는 FIFO가 비어 있지 않고 in_ready 신호는 FIFO가 가득 차지 않을 때마다 표시됩니다. 다음 속성을 확인해 보겠습니다.

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

AXI 프로토콜

유효한/준비된 AXI 핸드셰이크는 데이터 전송이 valid 및 ready 동시에 주장됩니다. 이 프로토콜로 작업할 때 발생하는 일반적인 오류 중 하나는 유효한(및 수반되는 데이터)를 주장하고 준비를 확인하지 않는 것입니다. 즉, valid이면 주장되고 ready 그렇지 않은 경우 valid 다음 클록 주기가 계속 주장되어야 하며 데이터는 변경되지 않은 상태로 유지되어야 합니다. 이는 FIFO로 들어가는 데이터와 FIFO에서 나오는 데이터 모두에 적용됩니다. FIFO에 들어가는 데이터의 경우 assume를 사용합니다. 키워드를 사용하고 FIFO에서 나오는 데이터의 경우 assert를 사용합니다. 키워드.

f_in_data_stable : assume always
   {in_valid and not in_ready and not rst} |=&gt;
   {stable(in_valid) and stable(in_data)};

f_out_data_stable : assert always
   {out_valid and not out_ready and not rst} |=&gt;
   {stable(out_valid) and stable(out_data)};

여기서 stable 사용에 유의하세요. |=>과 조합된 키워드 운영자. 이러한 명령문은 두 개의 연속적인 클록 주기를 참조합니다. 첫 번째 클록 주기에서 valid 주장되고 ready 주장되지 않습니다. 그런 다음 다음(초) 클록 주기(|=>로 표시됨)에서 연산자), valid 값 및 data 이전(즉, 첫 번째) 클록 주기와 같아야 합니다.

둘째, AXI 프로토콜의 경우 ready 신호가 안정적입니다. 이것이 의미하는 바는 FIFO가 데이터(ready 어설션됨) 데이터가 입력되지 않음(valid 어설션되지 않음), 다음 클록 주기에서 ready 주장된 상태를 유지해야 합니다.

f_out_ready_stable : assume always
   {out_ready and not out_valid and not rst} |=&gt;
   {stable(out_ready)};

f_in_ready_stable : assert always
   {in_ready and not in_valid and not rst} |=&gt;
   {stable(in_ready)};

FIFO 주문

FIFO의 또 다른 중요한 속성은 데이터가 복제/삭제/교환되지 않는다는 것입니다. 이 속성을 PSL로 표현하는 것은 상당히 복잡하며 이 형식 검증에서 가장 어려운 부분입니다. 이 속성을 단계별로 주의 깊게 살펴보겠습니다.

일반적으로 데이터 D1이 다른 데이터 D2보다 먼저 FIFO에 들어가면 출력 측에서 동일한 데이터 D1이 D2보다 먼저 FIFO를 떠나야 한다고 일반적으로 말할 수 있습니다.

이것을 PSL로 표현하려면 몇 가지 보조 신호가 필요합니다. f_sampled_in_d1 , f_sampled_in_d2 , f_sampled_out_d1 및 f_sampled_out_d2 . 이 신호는 리셋 시 지워지고 D1 또는 D2가 FIFO에 들어가거나 나갈 때마다 표명됩니다. 일단 주장된 신호는 주장된 상태로 유지됩니다.

따라서 우리는 FIFO 순서 속성을 두 부분으로 표현합니다. 첫 번째는 가정입니다. D2가 FIFO에 들어가면 D1은 이미 이전에 입력한 것입니다.

f_fifo_ordering_in : assume always
   {f_sampled_in_d2} |-&gt;
   {f_sampled_in_d1};

두 번째로 주장 D2가 FIFO를 떠나면 D1은 이미 이전에 떠났습니다.

f_fifo_ordering_out : assert always
   {f_sampled_out_d2} |-&gt;
   {f_sampled_out_d1};

위에서 언급한 샘플링 신호를 선언하고 채워야 합니다. 입력 샘플링 신호에 대해 다음과 같이 수행합니다.

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 &lt;= '1';
         end if;
         if in_data = f_value_d2 then
            f_sampled_in_d2 &lt;= '1';
         end if;
      end if;

      if out_valid then
         if out_data = f_value_d1 then
            f_sampled_out_d1 &lt;= '1';
         end if;
         if out_data = f_value_d2 then
            f_sampled_out_d2 &lt;= '1';
         end if;
      end if;

      if rst = '1' then
         f_sampled_in_d1  &lt;= '0';
         f_sampled_in_d2  &lt;= '0';
         f_sampled_out_d1 &lt;= '0';
         f_sampled_out_d2 &lt;= '0';
      end if;
   end if;
end process p_sampled;

여기서 우리는 두 개의 다른 신호 f_value_d1를 참조합니다. 및 f_value_d2 . 여기에는 데이터 값 D1 및 D2가 포함됩니다. 이러한 신호에는 모든 임의가 포함될 수 있습니다. 값이며 공식 검증 도구에 이를 표시하는 특별한 방법이 있습니다.

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;

anyconst 속성은 공식 검증 도구에서 인식됩니다. 이는 도구가 그 자리에 상수 값을 삽입할 수 있음을 나타냅니다.

위와 같이 FIFO의 속성을 지정했습니다.

공식 인증 실행

공식 검증 도구를 실제로 실행하기 전에 작은 스크립트 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

섹션 [tasks] Bounded Model Checking을 원한다고 명시합니다. 섹션 [options] BMC가 10클럭 사이클 동안 실행되어야 함을 지정합니다. 기본값은 20입니다. 섹션 [engines] 여러 다른 솔버 중 사용할 솔버를 선택합니다. 특정 설계에 따라 가능한 다른 엔진의 실행 속도에 차이가 있을 수 있습니다. 지금은 이 값을 변경하지 않고 그대로 둡니다.

[script] 섹션은 흥미로운 부분입니다. 여기에서 VHDL 표준(2008), 제네릭 값, 처리할 파일 및 최상위 엔티티 이름을 지정합니다. 마지막으로 [files] 섹션에 파일 이름이 다시 포함됩니다.

이 스크립트가 준비되면 다음 명령을 사용하여 실제 형식 확인을 실행할 수 있습니다.

sby --yosys &quot;;yosys -m ghdl&quot;; -f axi_fifo.sby

공식 검증 도구를 실행하는 것은 다음과 같은 예의 없는 진술로 끝납니다.

[axi_fifo_bmc] DONE (PASS, rc=0)

이는 우리가 지정한 모든 속성이 최대 10클럭 사이클 동안 모든 임의 입력에 대해 만족한다는 것을 의미합니다. 깊이를 늘리면 솔버의 실행 시간이 길어집니다. 그러나 깊이는 FIFO의 깊이보다 큽니다. 즉, BMC는 일부 입력 시퀀스에 대해 FIFO 전체 상황에 직면하게 됩니다. 예를 들어 5개의 클록 주기만 선택했다면 공식 검증은 FIFO가 가득 찬 경우가 발생하지 않으며 이와 관련된 버그를 포착하지 못할 것입니다.

속성이 모든에 대해 충족됨을 증명할 수 있습니다. 유도 증명을 사용하는 클록 사이클. 그러나 속성을 작성하려면 더 많은 작업이 필요합니다. 문제는 지금까지 일부 속성. 그러나 유도를 위해서는 all을 지정해야 합니다. 속성 (또는 적어도 충분히 많은). 시간이 많이 걸리므로 대신 자신감을 높일 수 있는 다른 전략에 대해 논의하겠습니다.

돌연변이

이제 axi_fifo 모듈은 만족해야 하며 우리 도구는 이러한 속성을 신속하게 확인합니다. 즉, 만족함을 증명합니다. 그러나 우리는 여전히 다음과 같은 불안한 느낌을 가질 수 있습니다. 버그가 없는 것이 확실합니까? axi_fifo의 모든 속성을 실제로 표현했습니까? 모듈?

이러한 질문에 답하는 데 도움이 되고 지정된 속성의 완전성에 대한 확신을 더 얻기 위해 돌연변이라는 기술을 적용할 수 있습니다. :우리는 의도적으로 구현에 약간의 변경을 가합니다. 즉, 의도적으로 버그를 도입한 다음 공식 검증으로 버그를 잡을 수 있는지 확인합니다!

이러한 변경 중 하나는 out_valid를 제어하는 일부 논리를 제거하는 것입니다. 신호. 예를 들어 다음 세 줄을 주석 처리할 수 있습니다.

if count = 1 and read_while_write_p1 = '1' then
  out_valid_i &lt;= '0';
end if;

이제 공식 검증을 실행할 때 메시지와 함께 실패가 발생합니다.

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable
Writing trace to VCD file: engine_0/trace.vcd

도구 GTKwave를 사용하여 수반되는 파형을 볼 수 있으며 다음과 같이 보입니다.

여기서 우리는 40ns에서 out_valid 신호는 0으로 가야 하지만 그렇지 않습니다. 실패한 어설션은 50ns에서 발생합니다. 여기서 out_valid 여전히 높지만 out_data 중복 데이터를 나타내는 신호 변경. out_ready 때문에 이 특정 추적에서 복제된 데이터가 실제로 전송되지 않았습니다. 40ns로 낮지만 공식 검증은 그럼에도 불구하고 버그를 감지합니다.

표지 설명

마지막으로 공식 검증 도구의 다른 응용 프로그램인 Cover statement를 살펴보겠습니다. 커버 문의 목적은 특정 속성을 만족하는 입력 시퀀스가 있는지 확인하는 것입니다. FIFO를 다루고 있으므로 완전히 채웠다가 다시 비울 수 있는지 봅시다. 이것은 단일 표지 문장으로 표현할 수 있습니다:

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

정말 한 입 가득! {} 내의 세미콜론에 유의하십시오. . 가독성을 위해 각 섹션을 별도의 줄에 배치했습니다. 이 표지의 내용은 다음과 같습니다. 다음을 만족하는 입력 시퀀스를 찾으십시오.

리셋은 한 클럭 주기 동안 적용됩니다.
모든 클록 주기(리셋이 지정되지 않은 경우)는 통과할 수 있습니다.
리셋이 지정되지 않고 FIFO가 가득 찬 1클록 주기
모든 클록 주기(리셋이 지정되지 않은 경우)는 통과할 수 있습니다.
리셋이 지정되지 않고 FIFO가 비어 있는 한 클록 주기

따라서 구문 [*] 이전 조건 반복(0회 이상)을 의미합니다. 3행에서 rst = '0' 조건을 제거할 수 있었습니다. [*] 앞 . 결과는 동일할 것입니다. 그 이유는 형식 검증자가 가장 짧은 커버 문을 만족시키는 시퀀스와 FIFO를 채우는 동안 리셋을 주장하는 것은 단지 그것을 지연시킬 것입니다. 그러나 5행에서 FIFO를 비울 때 재설정이 주장되지 않는 것이 필수적입니다.

이제 형식 검증기를 실행하려면 axi_fifo.sby 스크립트를 약간 수정해야 합니다. . 상단 섹션을 다음으로 교체:

[tasks]
bmc
cover

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

이제 솔버가 BMC를 실행한 다음 덮개 분석을 실행합니다. 출력에 다음 두 줄이 표시됩니다.

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.
Writing trace to VCD file: engine_0/trace5.vcd

이것은 표지 문장이 실제로 15개의 클록 사이클 시퀀스로 충족될 수 있고 솔버가 이 표지 문장에 대한 파형을 생성했음을 의미합니다.

여기서 우리는 80ns에서 FIFO가 가득 차고 in_ready임을 알 수 있습니다. 주장 해제됩니다. 그리고 150ns에서 FIFO는 비어 있고 out_valid 주장 해제됩니다. 30ns ~ 80ns 기간 동안 out_ready 낮게 유지됩니다. 이는 FIFO가 가득 차도록 하는 데 필요합니다.

count = ram_depth-1 조건을 바꾸면 count = ram_depth 사용 , 표지 문을 만족할 수 없습니다. 그러면 도구에서 오류를 보고합니다.

Unreached cover statement at i_axi_fifo.f_full_to_empty.

따라서 오류 메시지에는 실패한 표지의 레이블이 포함됩니다. 이것이 라벨이 매우 유용한 이유 중 하나입니다! 위의 오류는 FIFO가 ram_depth을 보유할 수 없음을 나타내는 것으로 해석됩니다. 요소의 수. 이는 원래 AXI FIFO 블로그 게시물에 명시된 것과 동일합니다.

여기서 어디로 가야 하나요

PSL 언어 입문서
공식 인증 소개
공식 인증 시작을 위한 일련의 소규모 동영상
공식 인증 관련 블로그
공식 검증에 대한 고급 주제가 포함된 일련의 기사
공식 검증을 사용한 작은 예 모음

VUnit 시작하기 통합 로직 분석기(ILA) 및 가상 입출력(VIO) 사용

VHDL