[논문]임베디드 시스템을 위한 동기적 언어 기반 하드웨어/소프트웨어 통합 설계 및 검증

이수영; 김진현; 최진영

문제 정의

C++를 기반으로 하기 때문에 C++에 익숙한 프로그래머들이 사용하기에 편리한 하드웨어와 소프트웨어를 통합 설계하는 방법이다. SpecC^ C의 확장으로서 시스템 레벨 설계와 수작업을 통해 수정하는 것을 목적으로 한다. 둘 다 시스템 레벨 개발을 위한 생산성의 중요한 요소가 되는 단일 프레임워크와 통합 시뮬레이션 내에서 소프트웨어와 하드웨어 구성 요소들을 기술한다.
기존의 P이is나 SystemC를 이용한 하드웨어/소프트웨어 홍합 개발은 하드웨어/소프트웨어의 분할이 어렵다거나 하뜨웨어/소프트웨어의 정형검증이 어려웠다. 따라서 본 논문은 일반적인 임베디드 시스템 개발과정에서 하드웨어와 소프트웨어를 각각 정형명세 언어인 Est아el을 통해 하드웨어/소프트웨어 설계률 정형적으로 명세하고 Este「el의 검증도구플 이용하여 정형검증을 함으로써 하드웨어/소프트웨어 통함 개발을 위한 새로운 방법론을 제시하였다. 결론적으로, 본 논문은 설계 과정의 어떤 시점에서 개발 중의 가상 하드웨어가 아닌 실제 임베디드시스템 개발과정에서 괘발 완료된 하드웨어의 코드룰 정형 명세 언어로 설계하여 이를 기반으로 하는 소프트웨어를 개발하는, 현실적인 임베디드 시스템 개발을 위해 더 耋과적인 하드웨어/소프트웨어 통합 개발 방법론을 제시하여 그 萱율성을 높였다.
본 논문에서 제안한 하드웨어/소프트웨어 통합 설계 및 검증은 일반적인 임베디드 시스템 개발 방법론오로는 하드웨어와 소프트웨어를 각각 개발 시 복잡한 하드웨어와 소프트웨어의 구조로 인한 인터페이스상의 문제점이나 시뮬레이션의 문제점들을 해결하고자 제안하였다. 기존의 P이is나 SystemC를 이용한 하드웨어/소프트웨어 홍합 개발은 하드웨어/소프트웨어의 분할이 어렵다거나 하뜨웨어/소프트웨어의 정형검증이 어려웠다.
검증 특성이 시뮬레이션에 의해 비정형적으로 타당한지, static analysis 수행에 의해 정형적으로 타당한지를 보이도록 체크할 수 있다. 본 논문에서는 시뮬레이션을 통해 타당성을 검증 받은 홍합 설계의 정형 검증을 위해 검증 튝성을 주어 올바른 행위률 수행하고 있음을 검증해보고자 한다. 우선 설계한 시스템이 만족해야핥요구 조건을 Esterel 언어에서 ass이히cm로서 기술하고 이룰 검증기를 동해 조건이 참인지 거짓인지를 관찰한다.
이에 하드웨어와 소프트웨어룔 통합 설계하고 검증하는 다양한 방법들이 많은 연구기관들에 의해 제시되어 왔다. 본 논문에서는 임베디드 시스템 개발을 위해 동기적 언어인 Este「a을 이용하여 하드웨어/소프트웨어 통합 설계 및 통합 검증을 제안하고자 한다. 보통 하드웨어/소프트웨어 통합 개발을 할 경우, 시스템 레벨에서 하드웨어/소프트웨어를 명세하고 검증 한 뒤 하드웨어/소프트웨어를 분할하여 각각 하드웨어와 소프트웨어로 개발한다.
따라서 소프트웨어를 실현하는 부분과 하드웨어로 실현하는 부분의 분할이 어렵다. 본 논문은 하드웨어와 소프트웨어가 처음부터 클리어하게 분할되어 있는 상태에서 설계률 한다. 즉, 이미 만들어져 있는 하드웨어 스펙으로부터 정형 명세 언어인 Esterel[1] 을 이용하여 하드웨어를 설계하고 검증한 후, 마찬가지로 소프트웨어를 Este「이로 설계, 이를 하드웨어와 통합한다.

제안 방법

소프트웨어로부터 직접적으로 RX와 TX Wi「e를 통한 읽기와 제어기능을 UART 서킷의 RS232 serial po「t룳 통해 읽고 쓰도록 한다. RS232 인터페이스의 전송과 수신부분은 Estsel의 Safe State Machine 부호를 이용하여 그래픽하게 기술되도록 Es怕「題의 그래픽컬한 표현언어인 SyncChafts⑸를 이용하여 기술하였다. RS232 전송자를 위한 모델은 그림 2 와 같다.
즉, 이미 만들어져 있는 하드웨어 스펙으로부터 정형 명세 언어인 Esterel[1] 을 이용하여 하드웨어를 설계하고 검증한 후, 마찬가지로 소프트웨어를 Este「이로 설계, 이를 하드웨어와 통합한다. 그 후 임베디드 시스템의 하드웨어와 소프트웨어가 가질 수 있는 오류 가능성을 고려하여 구현한 모델을 통합 검증을 하도록 정형기법을 도입한 임베디드 시스템개발 방법론을 제시한다.
정형 명세한 하드웨어 디자인을 하드웨어가 요구하는 특성을 검중 특성으로 주어 정형 검증한다為 이렇게 하드웨어를 완전하게 구현하는데, 이것은 Estwel이 RTL 레벨의 하드웨어 언어이기 때문에 VHDL로 코드제너레이션 하여 바로 하드웨어를 만들 수가 있다. 그리고 소프트웨어 요구사항을 분석하여 이를 구현된 하드웨어 디자인에 소프트웨어를 cone니「「ent 하게 통합 설계한다. 이 통합 설계는 시뮬레이션과 통합 정형검증을 수행한다.
본 논문에서는 하드웨어는 이미 구현되어 있는 것으로부터 명세한 설계이기 때문에 소프트웨어 설계만을 추출하여 C코드를 자동생성하였다. 그리고 이를 타겟 보드인 Intel 80c196kc 마이크로프로세서가 탑재된 보드에 포팅 및 실행해보았다.
Esterel에서 사용하는 정형 검증 기법은 모델체킹 기법으로, 명세한 시스템 율 시스템 사용시 맔생 가능한 모든 상태를 표현하는 유한 상태 기계로 바꾼다. 등가관계 기법과 BDD 기법, SAT 기법을 이용하여 유한 상태를 최소화 시켜 유한상태 기계의 모든 상태를 찾아다니며, 출력 시二1널의 상태를 확인하는 삼태 탐색 기법을 이용하여 검증한다. Este「el예서 검증 방법론은 동기적 observe들의 개념을 기반으로 한다.
그림 1은 본 논문에서 제안한 하드웨어/소프트웨어 통합 설계 및 통합 검증 과정을 나타내고 있다. 먼저, 시스템 요구사항 오로부터 하드웨어 요구사항을 분석하여 하드웨어를 정형 명세 한다. 정형 명세한 하드웨어 디자인을 하드웨어가 요구하는 특성을 검중 특성으로 주어 정형 검증한다為 이렇게 하드웨어를 완전하게 구현하는데, 이것은 Estwel이 RTL 레벨의 하드웨어 언어이기 때문에 VHDL로 코드제너레이션 하여 바로 하드웨어를 만들 수가 있다.
소프트웨어는 UART 디바이스 드라이버 역할을 하는 모듈과 如이ication 태스크이다. 본 논문에서 제안하는 UART 디바이스 드라이出는 비동기 시리얼 통신의 하위 레벨 작업을 핸들링하는 통합된 서킷인 UART의 드라이버이다. UART 디바이스 드라이버는 데이터를 단순히 UART로부터 한 바이트의 데이터를 읽거나 쓰는 동작을 하며, Parity bit check e「「。「시 재전송 인터럽트를 발생시켜 데이터를 재전송한다.
위한 C 코드룔 생성한다. 본 논문에서는 하드웨어는 이미 구현되어 있는 것으로부터 명세한 설계이기 때문에 소프트웨어 설계만을 추출하여 C코드를 자동생성하였다. 그리고 이를 타겟 보드인 Intel 80c196kc 마이크로프로세서가 탑재된 보드에 포팅 및 실행해보았다.
본 논문은 다른 검증 특성으로 시리얼 통신의 parity bit checkAI 오류가 발생하면 이률 컨트롤하는지를 정형 검증해보았다, 데이터룰 수신 중 수신기는 Parity bit check를 한다, 이를 통해 데이터가 유실되었는지롤 확인한다. 만약 유실되었다면 유실된 데이터를 다시 재전송하도록 application task, 즉, 소프트웨어 레벨에서 전송기에 요구한다.
본 장에서는 3.3장에서 명세한 하드웨어/소프트웨어 통합 모델을 가지고 정형 검증하고자 한다. Esterel에서 사용하는 정형 검증 기법은 모델체킹 기법으로, 명세한 시스템 율 시스템 사용시 맔생 가능한 모든 상태를 표현하는 유한 상태 기계로 바꾼다.
문석된 반례는 다시 시뮬레이터를 통해 그 발생 경로를 추적 후 수정하게 되고, 시스템 모델의 오류수정 후 시스템의 재검사 작업이 이루어진다. 본 장에서는 명세한 UART HW/SW의 통합 설계에 대한 동작의 신뢰성을 확인하기 위해 시뮬레이션과 검증 기법을 이용해서 설계의 오류가 없는지를 확인해본다. 검증에 대한 확인 과정은 검증 특성을 가지고 만족하는 결과를 보이는지를 확인해본다.
본 절에서는 UART 하드웨어를 선택하여 Este「el로 정형 명세하였다. UART 하드웨어는 RX, TX, CTS, RTS 등의 Wire를 가진 RS232 인터페이스룔 통해 호스트와타겟 간의 통신을 수행한다.
본 절에서는 하드웨어와 소프트웨어률 통합 검증하기 위해 정형 명세 및 검증이 완료된 하드웨어 설계와 소프트웨어를 통합 설계한다. 소프트웨어는 UART 디바이스 드라이버 역할을 하는 모듈과 如이ication 태스크이다.
본 논문에서는 시뮬레이션을 통해 타당성을 검증 받은 홍합 설계의 정형 검증을 위해 검증 튝성을 주어 올바른 행위률 수행하고 있음을 검증해보고자 한다. 우선 설계한 시스템이 만족해야핥요구 조건을 Esterel 언어에서 ass이히cm로서 기술하고 이룰 검증기를 동해 조건이 참인지 거짓인지를 관찰한다. 만족하는 경우에는 시스템이 본래 의도대로 제대로 설계되었다는 것을 의미하고, 위반하는 경우는 검증기 분석에 의한 해당 검증 조건의 반례(counter example)를발생한다.
이렇게 하드웨어/소프트웨어 통합 검증을 위해 Ester이로 UART 하드웨어와 소프트웨어릃 다음 그림 8과 같이 메인 모듈에서 패러렐하게 동작하도록 구현하였다. 그림 8 과 같이 정형 명세한 임베디드 시스템의 하드웨어/소프트웨어 통합 설계는 모듈들 간에 브로드캐스팅 (Broadcasting)Sfe 시그널들을 통해서 동기화 되며 주어진 작업을 수행한다.
하드웨어에서 버퍼 레지스터는 버퍼가 f네인 경우에만 Serial interrupt 산호를 발생하여 버퍼로부터 데이터를 읽을 수 있도록 해야 한다. 이를 검증 특성으로 다음과 같이 LTL[7]을 이용하여기호화하고 그림 5와 같이 Ester이에서 asswtion으로 정의하여 정형 명세하였다.
이번 절에서는 UART HW/SW 통합 설계가 갖추어야 할 검증 특성으로 하드웨어와 소프트웨어간의 mtwaction을검증하기 위해 하드웨어 레벨에서 발생하는 시리얼 인터럽트가 소프트웨어 레벨에서 제대로 인터럽트를 처리하는지를 검증하기 위해 다음과 같은 검증 조건을 두었다. 인터럽트에 의해서만 소프트웨어 태스크가 동기화가 되어야 한다를 만족하기 위해서는 IF and Only If 조건을 만족해야 한다, 즉, 소프트웨어 태스크가 동기화 되면 시리얼 인터럽트 신호는 발생해야 하며 이는 하드웨어/소프트웨어 설계의 모든 스테이트에서 만족되어야 한다.
하지만 하드웨어와 소프트웨어의 분할이 어렵다는 문제점이 있다, 본 논문은 처음부터 하드웨어와 소프트웨어가 클리어하게 분할되어 있는 상태에서 하드웨어를 설계 및 검증하고 그 후 소프트웨어릃 통합 설계하여 하드웨어/소프트웨어의 통합 검증을 한다. 즉, 본 논문은 만들어진 하드웨어에서 하드웨어와 interact하는 소프트웨어를 개발하는 방법으로 접근하였다.
본 논문은 하드웨어와 소프트웨어가 처음부터 클리어하게 분할되어 있는 상태에서 설계률 한다. 즉, 이미 만들어져 있는 하드웨어 스펙으로부터 정형 명세 언어인 Esterel[1] 을 이용하여 하드웨어를 설계하고 검증한 후, 마찬가지로 소프트웨어를 Este「이로 설계, 이를 하드웨어와 통합한다. 그 후 임베디드 시스템의 하드웨어와 소프트웨어가 가질 수 있는 오류 가능성을 고려하여 구현한 모델을 통합 검증을 하도록 정형기법을 도입한 임베디드 시스템개발 방법론을 제시한다.
P이is는 시스템 수준에서 하드웨어/소프트웨어의 정형적인 통합 설계 및 정형검증을 하고 나서 하드웨어와 소프트웨어률 분할 및 구현한다. 하지만 하드웨어와 소프트웨어의 분할이 어렵다는 문제점이 있다, 본 논문은 처음부터 하드웨어와 소프트웨어가 클리어하게 분할되어 있는 상태에서 하드웨어를 설계 및 검증하고 그 후 소프트웨어릃 통합 설계하여 하드웨어/소프트웨어의 통합 검증을 한다. 즉, 본 논문은 만들어진 하드웨어에서 하드웨어와 interact하는 소프트웨어를 개발하는 방법으로 접근하였다.

대상 데이터

이를 위해 가상의 parity bit check 오류를 발생시킨다. 즉, test 신호는 가상의 parity bit check 오류 신호이다. 이 test 신호가 발생하면 재전송 신호가 발생해야 한다.

데이터처리

같이 주어친 검증특성을 가지고 Esters stu예。[6] 검증기를 통해 정형 검증하였다. 하드웨어에서 버퍼 레지스터는 버퍼가 f네인 경우에만 Serial interrupt 산호를 발생하여 버퍼로부터 데이터를 읽을 수 있도록 해야 한다.
Stu히。의 검증 시뮬레이션 도구휼 이용하여 동합설계의 타당성 검증을 수행하였다. Esterel studio 의 시율 레이션은 시스템에 어떤 입력값을 주고 그 입력 값에 따른 상태 다이어그램의 상태 변화와 츟력되는 시그널을 통해서 결과가 처음에 의도한대로 몰바르게 나오는지를 확인해보는 방법이다.
그리고 이를 Esterel stu치。의 검증기를 통해 정형 검증하였다. 그림 6은 검증결과로 버퍼가 f 니I인 경우 SERIALJNT 가 발생한다는 가정이 항상 t「ue임을 확인할 수 있다.
그리고 소프트웨어 요구사항을 분석하여 이를 구현된 하드웨어 디자인에 소프트웨어를 cone니「「ent 하게 통합 설계한다. 이 통합 설계는 시뮬레이션과 통합 정형검증을 수행한다. 통합 정형검증에 대해서는 3.

이론/모형

인터럽트에 의해서만 소프트웨어 태스크가 동기화가 되어야 한다를 만족하기 위해서는 IF and Only If 조건을 만족해야 한다, 즉, 소프트웨어 태스크가 동기화 되면 시리얼 인터럽트 신호는 발생해야 하며 이는 하드웨어/소프트웨어 설계의 모든 스테이트에서 만족되어야 한다. 검증 조건은 LTL(Line由 Temporal logic)을 이용하여 기호화하고 이를 그림 10과 같이 Esterel 내에서 assertion 을 적용하여 명세하였다.

성능/효과

검증에 대한 확인 과정은 검증 특성을 가지고 만족하는 결과를 보이는지를 확인해본다. 검증 특성이 요구하는 결과를 만족한다면 시스템이 알고리즘의 원칙대로 동작한다는 사실을 알 수 있고 이룔 토대로 시스템이 올바르게 설계되었음을 확인해 볼 수 있다.
따라서 본 논문은 일반적인 임베디드 시스템 개발과정에서 하드웨어와 소프트웨어를 각각 정형명세 언어인 Est아el을 통해 하드웨어/소프트웨어 설계률 정형적으로 명세하고 Este「el의 검증도구플 이용하여 정형검증을 함으로써 하드웨어/소프트웨어 통함 개발을 위한 새로운 방법론을 제시하였다. 결론적으로, 본 논문은 설계 과정의 어떤 시점에서 개발 중의 가상 하드웨어가 아닌 실제 임베디드시스템 개발과정에서 괘발 완료된 하드웨어의 코드룰 정형 명세 언어로 설계하여 이를 기반으로 하는 소프트웨어를 개발하는, 현실적인 임베디드 시스템 개발을 위해 더 耋과적인 하드웨어/소프트웨어 통합 개발 방법론을 제시하여 그 萱율성을 높였다. 그러나 개발 대상을 이해하고모델링을 거쳐 명세 및 검증하는 과정에서 실제 임베디드 시스템에 대해 시스템 모델을 정하기 위한 완벽한 이해가 필요하다.
확인할 수 있었다. 따라서 검증 조건 2에 의한 검증 결과는 Parity bit check 오류시 재전송이 이루어짐을 확인할 수 있었다. 이룰 통해 error con廿이을 보장함을 확인했다.
있었다. 땨라서, 검증 조건 1에 의한 검증 결과는 Interrupt 신호가 발생하지 않으면 동기화 되지 않으며, Interrupt 신호가 발생하면 항상 동기화된다는 사실을 확인 할 수 있었다.
Esterel studio 의 시율 레이션은 시스템에 어떤 입력값을 주고 그 입력 값에 따른 상태 다이어그램의 상태 변화와 츟력되는 시그널을 통해서 결과가 처음에 의도한대로 몰바르게 나오는지를 확인해보는 방법이다. 본 논문에서는 그림 9와 같이 하드웨어/소프트웨어 통합 설계가 을바르게 수행함을 확인하였다. 이렇게 명세한 임베디드 시스템의 하드웨어/소프트웨어의 통합 설계를 가지고 3.

후속연구

그러나 개발 대상을 이해하고모델링을 거쳐 명세 및 검증하는 과정에서 실제 임베디드 시스템에 대해 시스템 모델을 정하기 위한 완벽한 이해가 필요하다. 향후 연구 과제로는 SoC와 같은 목잡한임베디드 시스템을 통합 설계 및 통합 검증하기 위한 개발 방법론을 연구할 계획이다.

내보내기 구분	파일저장 인쇄 메일전송
구성항목	기본정보 상세정보 관리번호, 논문명, 저널/프로시딩명, 저자 , 발행년, 권, 호, 시작페이지, 끝페이지, 발행기관 관리번호, 논문명, 대등논문명, 저자 , 저널/프로시딩명, 발행기관, 발행년, 발행언어, 권, 호, 시작페이지, 끝페이지, ISBN, ISSN, 주제분야, 키워드, 초록(한글), 초록(영문), 저자(소속기관)
저장형식	Text(ASCII format) Excel format RefWorks Direct Export RIS format (for Reference Manager, ProCite, EndNote), Scholar's Aids, Mendeley
메일정보	받는사람 (필수) @ 보내는사람 (선택) @ 제목 내용 KISTI 검색결과 이메일 서비스
안내	총 건의 자료가 검색되었습니다. 다운받으실 자료의 인덱스를 입력하세요. (1-10,000) 검색결과의 순서대로 최대 10,000건 까지 다운로드가 가능합니다. 데이타가 많을 경우 속도가 느려질 수 있습니다.(최대 2~3분 소요) 다운로드 파일은 UTF-8 형태로 저장됩니다. 파일의 내용이 제대로 보이지 않을실 때는 웹브라우저 상단의 보기 -> 인코딩 -> 자동선택 여부를 확인하십시오. ~ Text(ASCII format) Excel format

연합인증

임베디드 시스템을 위한 동기적 언어 기반 하드웨어/소프트웨어 통합 설계 및 검증
Hardware/Software Co-design and Verification by Synchronous language for Embedded System 원문보기

초록
AI-Helper

AI 본문요약
AI-Helper

문제 정의

제안 방법

대상 데이터

데이터처리

이론/모형

성능/효과

후속연구

이 논문을 인용한 문헌

관련 콘텐츠

원문 보기

이 논문과 함께 이용한 콘텐츠

AI-Helper ※ AI-Helper는 오픈소스 모델을 사용합니다.

선택된 텍스트

연합인증

임베디드 시스템을 위한 동기적 언어 기반 하드웨어/소프트웨어 통합 설계 및 검증 Hardware/Software Co-design and Verification by Synchronous language for Embedded System 원문보기

초록 용어보기논문에서 용어와 풀이말을 자동 추출한 결과로, 시범 서비스 중입니다. AI-Helper

AI 본문요약 엑셀 다운로드 AI-Helper

문제 정의

제안 방법

대상 데이터

데이터처리

이론/모형

성능/효과

후속연구

이 논문을 인용한 문헌

관련 콘텐츠

원문 보기

이 논문과 함께 이용한 콘텐츠

AI-Helper ※ AI-Helper는 오픈소스 모델을 사용합니다.

선택된 텍스트

임베디드 시스템을 위한 동기적 언어 기반 하드웨어/소프트웨어 통합 설계 및 검증
Hardware/Software Co-design and Verification by Synchronous language for Embedded System 원문보기

초록
AI-Helper

AI 본문요약
AI-Helper