Верификация инфрақұрылымының аналитикалық моделі

Пән: Физика
Жұмыс түрі: Реферат
Тегін: Антиплагиат
Көлемі: 8 бет
Таңдаулыға:

МАЗМҰНЫ

КІРІСПЕ3
НЕГІЗГІ БӨЛІМ

Верификация инфрақұрылымының аналитикалық моделі . . . 4

ҚОРЫТЫНДЫ . . . 11

ҚОЛДАНЫЛҒАН ӘДЕБИЕТТЕР ТІЗІМІ. . . 12

КІРІСПЕ

Жүйені жобалаудың әр түрлі аспектілері үшін әр түрлі тілдер жүзеге асырылды. C/C++ кірістірілген жүйелердің бағдарламалық қамсыздандыруын жүргізуде айрықша басымдылықпен қолданылды.

HDL - тілдері аппаратураны сипатту үшін, VUDL және Verilog сандық сұлбаларды жобалау мен синтездеуде пайдаланылды. Vera верификациялау тілі- ASIC- жобаларының ішкі верификациясы үшін қолданылатын, Sun Micro System бірлестігінің тудырған өнімі. Кейін VERA компиляторымен VERA тілі System Science фирмасына сатылып, соның салдарынан Synopsys бірлестігіне көшеді. Қазіргі таңда, Synopsys бірлестігісVCS компиляторымен қолданатын, Vera тілінің жаңа нұсқасын - Open Vera -ны шығарды. Верификация, валидация, ассерция сияқты басты ұғымдар арасындағы қатынастарды түсіну үшін келесі анықтамалар енгізіледі.

Верификациялау - жобалаудың әрбір кезеңінде кіріс суреттелуінің шығысқа формальды түрденуінің дұрыстығын анықтау үшін компоненттер немесе жүйе анализінің процесі.

Валидация - әрбір кезеңдегі жобалау орындалғаннан кейін, спецификацияның басты талаптарына сәйкестігін тексеру жолымен, жүйенің және оның компоненттерінің жұмыс істеу қабілетін анықтау процесі.

Сертификаттау - спецификацияның оның тағайындалуы бойынша қолданылуы кезіндегі, талаптарына жүйе анықтылығының экспертті кепілдігі.

Ассерция - синтезді орындауға дейін және кейін тестті әрекетте жобаны модельдеу кезінде, спецификация талаптарына қатысты жобалау қателерін ерте анықтау үшін арналған жүйелік деңгейдің инверсты HDL-пікірі.

Верификация инфрақұрылымының аналитикалық моделі

HDL моделінің жалпыланған күйін идентификациялау үшін эталонды реакциялар критикалық нүктеде уақыт бойынша және ортада жасалады. Содан кейін HDL моделі үшін оны салыстыру жолымен эталонды және экспериментальды реакцияларды тексеріп, ассерционды векторды жасауға керек, яғни уақыт бойынша және ортада обьекттердің компоненттерін салыстыру күйін бейнелейді. Ассерционды векторды HDL моделінің жобалауынан тәуелсіз етіп жасау. Ассерционды және функционалды модельдерді паралельді және бір-біріне тәуелсіз модельдеу ортасында жүзеге асырады.

Ассерционды модель эталонды құрылымның кеңістік-уақыттық бірнеше маңызды нүктелердің обьекттерде тәртібінің ауытқуын анықтайды. Верификация инфрақұрылымының аналитикалық моделі келесі түрде көрсетілген (P - жоба спецификациясы, S - soft-модель, A - ассерционды модель, T - Testbench, F - фукнционалды жабулардың себеті, d - қателерді диагностикадан өткізу модулі және C - қателерді диагностикадан өткізу шарты) . Ассерция форматы HDL жобалау моделінің форматымен сәйкес келуі қажет. Ассерциялар Testbench және MUV қолдану арқылы HDL моделінің семантикалық қателіктерін тексеруге арналған. Верификация инфрақұрылымының аналитикалық моделі келесі түрде болады:

$M = \{ P, \ S, \ A, \ T, \ F, \ d, \ C\}$

Мұнда P- жобалау спецификациясы; S- программалық модель,

$S = f_{1}(P) = \left( S_{1}, \ S_{2}, \ \ldots, \ S_{i}, \ldots, S_{n}\ \right) ;$

F- функционалды жапқыштың кәрзеңкесі,

$F = f_{2}(P, \ S) = \left( F_{1}, \ F_{\ 2}, \ \ldots, \ F_{i\ }, \ \ldots, \ F_{n} \right) ;$

T- Testbench,

$T = f_{3}(P, \ S, \ F) = \left( T_{1}, T_{2}, \ldots, \ T_{i\ }, \ \ldots, \ T_{n} \right) ;$

А- ассерционды модель,

$A = f_{4}(P, \ S, \ F, \ T) = \left( A_{1}, A_{2}, \ldots, \ A_{i\ }, \ \ldots, \ A_{n} \right) ;$

$d$ және С- қателіктерді тексеретін шарттар мен модульдер,

$d = f_{5}(P, \ S, \ F, \ T, \ A) = \left( L_{1}, L_{2}, \ldots, \ L_{i\ }, \ \ldots, \ L_{n} \right) \in \left\{ L_{s}, L_{h} \right\},$

$C = \left\lbrack \bigcup_{i = 1}^{n}{F_{i} \in F = P} \right\rbrack \land \left\lbrack \bigcup_{i = 1}^{n}{T_{i} \in T = F} \right\rbrack\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (1)$

Мұнда

$L_{s} = (T, \ F) \oplus (S, \ A) ;$ (2)

$L_{h} = (T) \oplus (S, \ B) .$ (3)

(1) формула спецификацияға қатысты функционалдығын тексеретін тесттің (testbench) толық шартын анықтайды. (2) теңдеу верификациялық инфрақұрылымның атрибуттарын қолдану арқылы жүйеліктен регистрлеуге өткенде жобалау қателігін есептейтін функция. (3) теңдік сандық кристалдағы жүйені экслуатациясы кезінде ақауын табуға реттелген.

Ассерцияның қасиеттері мен типтері. 1) Ассерцияның шекаралық мәні жобаның диверсиялық моделі, іс жүзінде ассерциялық операторлардың саны - жоба кодының 5%-ы. 2) Лездік және біртактілік ассерциялар жоба моделіне жатады, инверсты if-операторлар нысанында бағдарлама мәтініне қойылады. 3) Параллельді ассерциялар (циклдық немесе көп тактілі) - орындалатын жоба моделіне тәуелсіз және параллельді модельденеді.

1-сурет. Валидация және верификация процесстерінің әрекеттестігі

Ассерционды артықтық спецификациямен анықталған функционалды компоненттердің уақыттық фреймдерінің саны шектік санға тең болатын HDL моделінің критикалық нүктесінің функциясы болып табылады. Априорлы координаттарға ассерция векторы Х мәнін біріктіреді. Содан кейін критикалық координатасы анықталады, яғни сандары берілген тексеру тереңдігімен программалық блоктартардың қателіктерін іздеу кезіндегі верификациялық эксперимент жүргізгенде ғана жеткілікті болады. Мұндай координаталар бірліктерде сәйкестенеді. А векторының Әрбір координатасына сәйкесінше бағдарламалық кодтың транзакциялық кескінінің барлық жоғарыдағы бастамашылардың тізімі қойылады. Вектор координаталарына кез келген басқа пішінде берілген ұлы бастамашылардың тізімі немесе транзакциялық кескіннің қол жеткізу матрицасы сәйкес келеді. Нақты А векторы элементтерінің екілік күйі келесі теңдеумен анықталатын, L ақаулы бағдарламалық блоктар d(A) тізімін сөзсіз диагностикадан өткізу рәсімін жүрзізеді.

$L_{s}(A) = \left( \bigcap_{\forall i(A_{i} = 1) }^{}A_{i} \right) \backslash\left( \bigcup_{\forall i(A_{i} = 0) }^{}A_{i} \right) ; \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (4)$

$L_{m}(A) = \left( \bigcup_{\forall i(A_{i} = 1) }^{}A_{i} \right) \backslash\left( \bigcup_{\forall i(A_{i} = 0) }^{}A_{i} \right) . \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (5)$

(4), (5) теңдеулер жүйесі ассерционды күйдегі векторларды қолданып, жалғыз және еселі қателіктерді іздеуге арналған. Ассерционды вектордың ұзындығы графтағы биіктік санына немесе HDL кодының функционалды-логикалық құрылымындағы программалық блок санына тең. Верификация ортасындағы векторлық модель келесі түрге ие:

$\left \begin{matrix} \begin{matrix} T_{1} \\ T_{2} \end{matrix} \\ T_{i} \\ T_{n} \end{matrix} \right \oplus \left \begin{matrix} \begin{matrix} S_{1} \\ S_{2} \end{matrix} \\ S_{i} \\ S_{n} \end{matrix} \right = \left \begin{matrix} \begin{matrix} A_{1} \\ A_{2} \end{matrix} \\ A_{i} \\ A_{n} \end{matrix} \right\overset{d}{\rightarrow}\left \begin{matrix} \begin{matrix} L_{1} \\ L_{2} \end{matrix} \\ L_{i} \\ L_{n} \end{matrix} \right.$ (6)

Модельдеу үдерісінде Testbench және HDL модельдерінің реакцияларын салыстырады, яғни ассерционды вектордың координата күйін жасайды:

$A_{i} = f\left( T_{i}, \ S_{i} \right) = T_{i} \oplus S_{i}, \ A_{i} = \left\{ 0, \ 1, \ X \right\}.$

Содан кейін маңызды {0, 1} ассерция векторының координатасына конъюнкция операциясын (4), (5) анықталған тәртіптердің біреуін қолдана отырып, программалық блоктардың тізімін алу үшін қолданады.

Келесі мысалда ақаулы блоктарды диагностика технологиясын қарастырамыз. HDL моделінің функционалды-логикалық графы берілсін

Өзара байланысқан граф құрылымын келесі қол жетімді матрицадан көреміз:

Диагностикалаудың векторлық моделі (6) теңдікте берілген, қолжетісді матрицадан алынған кез келген граф биіктігін блоктар-бастамасының тізімін қамтиды. Кез келген граф биіктігінде ассерцияға байланысты қойылады, яғни модельдеу процесі {0, 1} мәндері арқылы алдын-ала анықталуы мүмкін. Қазіргі жағдайда векторлық модель қателікті программалық блоктар (6) теңдей (7) граф түріне өзгереді:

Келесі мысалда алғашқы екі вектордан ассерционды вектордың координатасының негізгі анализінен ақаулы блоктардың тізімінен мардымсыз процесті өңдеуді шығарамыз. Жалғыз дефекттің тізімінің есептелу процедурасы келесі түрге ие:

Көптеген ақаулы блоктар үшін осындай ассерция векторы дефектті модульдің көп сандарын қамтиды.

Верификация және тестілеу стратегияларының, time-to-market параметрін қысқартуға бағдарланған, технология қосымшалары үшін әртүрлі модельдері бар. Верификацияның итеративті процесі өнім спецификациясынан алынған HDL-жүйелік деңгей моделінің қателерін жөндеуге бағдарланған.

2-сурет. Жобаны жасау стратегиясы

HDL-моделді верификациялау және тестілеу инфрақұрылымы 3-суретте келтірілген. Онда жоғарғы деңгейдің формалды тілінде суреттелген жоба спецификациясы функционалдық жабу түріндегі тест сапасын бағалау метрикасын құру, жобаның HDL-модельдері, эталонды реакциялы - Testbench, басты модельге қосымша болатын, жоба дұрыстығы мен тексеруін тездету үшін қажетті, ассерционды құрылым үшін бастапқы ақпарат болып табылады.