초록

AI-Helper

하드웨어 개발에 있어서 데이터의 신속한 처리와 공정의 저렴한 비용을 위해 회로의 많은 부분이 게이트 레벨에서 구현된다. 기능 검사는 하드웨어 개발에 있어서 설계의 기능을 분석하는 중요한 설계 흐름이다. 기존의 기능 검사는 사용자의 요구에 의해 하드웨어 시스템이 복잡해지고 개발 주기가 점점 빨라지는 시장의 특성으로 인해 설계자에게 시간적 경제적인 부담감을 준다. 본 연구에서는 설계자에게 가중되는 부담을 극복하고 보다 효율적인 기능 검사를 위해 모델 체킹을 동치성 검사에 적용하는 방법을 제안하고자 한다.

하드웨어 개발에 있어서 데이터의 신속한 처리와 공정의 저렴한 비용을 위해 회로의 많은 부분이 게이트 레벨에서 구현된다. 기능 검사는 하드웨어 개발에 있어서 설계의 기능을 분석하는 중요한 설계 흐름이다. 기존의 기능 검사는 사용자의 요구에 의해 하드웨어 시스템이 복잡해지고 개발 주기가 점점 빨라지는 시장의 특성으로 인해 설계자에게 시간적 경제적인 부담감을 준다. 본 연구에서는 설계자에게 가중되는 부담을 극복하고 보다 효율적인 기능 검사를 위해 모델 체킹을 동치성 검사에 적용하는 방법을 제안하고자 한다.

AI 본문요약

엑셀 다운로드 AI-Helper

* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.

• 연구 주제
• 연구 방법
• 연구 결과

문제 정의

• 본 논문에서는 모델 체킹을 이용하여 게이트 레벨에서 구현되는 회로의 기능 검사를 수행하기 위해서, 어떠한 전자 회로가 언제나 주어진 속성을 만족하는지 에 사용되 는 동치 성 검사 (Equivalence Checking)[2] 에 모델 체킹을 적용함으로써 모델체킹의 적용분야를 확장하고자 한다.
• 본 논문은 연구의 동기와 정형적인 하드웨어의 검증에 관련되어 진행되고 있는 연구에 대해 논하고, 모델 체킹에 동치성 검사를 적용하여 개발하고자 하는 회로의 기능 검사를 수행하는 연구 방법과 결과 및 적용 사례를 보여준다. 마지막으로 본 연구의 향후 연구에 대해 논하면서 논문을 마무리 한다.
• 본 연구에서는 설계자에게 가중되는 무담을 극복하고보다 효율적인 기능 검사를 위해 동치성 검사에 정형적인 모델 체킹을 이용하는 방법을 제안하고 있다. 동치성 검사에 모델 체킹을 적용하면 다음과 같은 특징을 지닌다.

제안 방법

• 그리고 제안한 방식이 적용된 도구는 CTL 모델 체커인 VIS를 사용하여 구현된 화로의 기능을 검증하였다.
• 이때 설계자는 데이터의 신속한 처리와 공정의 저렴한 비용을 위해 IP 코어의 많은 부분을 게이트 레벨에서 재설계한다. 기능 검사를 통해 이미 공개된 IP와 개선된 IP와의 동치성 검사를 일반적인 기능검사를 통해 수행한다. 기능 검사를 위한 도구개발이나 연구들은 초기의 환경을 벗어나지 못하고 있다.
• 논문에서 제안한 모텔 체킹을 이용한 동치성 검사에 대한 효율성을 알아보기 위해 n-bit adder를 이용하여 실험하였다. 다양한 실험을 위해 n-bit adder 인수의 크기를 2, 4, 8, 16, 32, 64, 128—bit로 실험하였다.
• 다양한 실험을 위해 n-bit adder 인수의 크기를 2, 4, 8, 16, 32, 64, 128—bit로 실험하였다.
• 하드웨어 시스템의 개발 단계는 Abstract - RTL - Structural - Transistor 4단계로 이루어지고, Abstract 단계에서 기존의 기능 검사를 통해 회로의 정확성을 확인한다. 동치성 검사는 RTL - Structural - Transistor 단계에서 이전 단계의 모델과 동치를 확인하여 각 단계의 기능 검사를 수행한다.[4] 동치성 검사는 Abstract 단계에서 올바른 모델을 얻기 전까지 기능검사를 수행할 수 없는 단점이 있다.
• 두 회로가 동치임을 증명한다. 두 회로 가동 일한 입력 신호에 대해서 동일한 결과를 출력한다는 것을 증명하기 위해 mite「를 구성하고 SA「를 통해 두 회로가 동치인지 아닌지를 증명한다. mite「는 두 회로의 대칭되는 입력들을 연결하고 대칭되는 출력들을 XOR, OR 게이트를 이용하여 두 회로가 동치이면 '0', 동치가 아니면 T'을 출력하도록 구성한다.
• 둘째, 오토마타로 구현되는 property mod니e에 대한모텔 체킹을 통해 정확한 속성을 검증한다.
• 그리고 모든 입력에 대해 두 회로가 동치임을 모델 체킹을 통해서 확인한다. 모델 체킹 도구 (VIS)는 하드웨어 명세 언어인 ve「ilog-HDL로 구현된 모델을 상태 전이 시스템으로 받아들이고, 검증하고자 하는 시스템의 속성을 Computational Tree Logic (CTL)으로 표현하여 검증한다.
• 본 논문에서는 [그림 1] 과 같이 정확한 모델을 기억소자를 가진 모델로 구현하고 개발하고자 하는 게이트 레벨의 회로와 miter 구조를 구성한다. 그리고 모든 입력에 대해 두 회로가 동치임을 모델 체킹을 통해서 확인한다.
• 하드웨어의 BMC 도구는 hw-CBMC[1 이가 있다. 실험을 통해 기존의 기능 검사와 본 논문 제안한 방법의 탐색 공간과 수행시간을 비교하고자 한다.
• 검사를 수행한다. 한 입력에 대한 신호를 출력하는 것을 step 이라 하고 사용자가 지정한 step까지 SA「를 통해 입력에 대한 올바른 신호를 출력하는지 확인한다. CNF의 표현은 positive/negative literal (variable) 들의 disj 니 nction 으로 이루어진이a니s들의 conjunction^^ 구성되다.
• 회로 설계시 설계자가 범할 수 있는 다양한 오류를 8- bit adde「에 삽입하여 실험한 하였다. 오류를 삽입한 실험에서 ica「니s-ve「ilog-HDL의 환경을 vis의 환경과 동일한 조건으로 맞추기 위해서 랜덤한 값을 삽입한 후, 두 회로의 결과가 틀리면 기능 검사를 중단하도록 system task를 구현하였다, icanjs-verilog-HDL에서는 0.

이론/모형

• 기존의 기능 검사는 리눅스 환경의 verilog-HDL 시뮬레이터인 icarus-verilog [12]를 사용했다. 그리고 제안한 방식이 적용된 도구는 CTL 모델 체커인 VIS를 사용하여 구현된 화로의 기능을 검증하였다.

성능/효과

• adde「에 삽입하여 실험한 하였다. 오류를 삽입한 실험에서 ica「니s-ve「ilog-HDL의 환경을 vis의 환경과 동일한 조건으로 맞추기 위해서 랜덤한 값을 삽입한 후, 두 회로의 결과가 틀리면 기능 검사를 중단하도록 system task를 구현하였다, icanjs-verilog-HDL에서는 0.057s에 오류를 발견하였고, VIS에서는 두 회로 가동 치성이 어긋나며 그 결과에 대한 counter exam이e을 0.2s만에 확인 할 수 있었다,
• 결과이다. 일반적인 기능 검사 도구인 icarus- verilog—HDL 는 모델의 크기에 상관없이 compile 시간이 거의 변함이 없는 것을 확인 할 수 있었고, 모델 체킹을 하기 위해 모델을 BDD (Binary Decision Daig「am) 으로 변환하는 VIS 에서는 모델의 크기가 커질수록 compile 시간이 늘어남을 확인 할 수 있다. Event-Driven 방식을 사용하는 icanjs-verilog-HDL는 32-bit adde「에서 수행 시간이 5060m23.
• 첫째, 재설계된 회로에 대한 정확성 확인을 자동으로 수행할 수 있는 방법론을 제시함으로 기존의 하드웨어 시스템 개발 절차를 간결하게 하였다.

후속연구

• 향후 연구로는 조합회로의 기능검사를 수행하기 위한 miter 구조를 자동으로 구현해주는 방법을 모색하겠다.

본문요약 정보가 도움이 되었나요? 예 아니오 제출

이 논문을 인용한 문헌

더보기