Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах
Розглянуто сучасні тенденції в галузі автоматизованого розроблення апаратного забезпечення, зокрема, розроблення цифрових систем з використанням програмованих логічних інтегральних схем на прикладі програмованих користувачем вентильних матриць. Запропоновано модельний метод розроблення, в якому вико...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2020 |
| Main Authors: | , , , , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2020
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/190448 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах / О.О. Летичевський, В.С. Песчаненко, В.С. Харченко, В.А. Волков, О.М. Одарущенко // Кибернетика и системный анализ. — 2020. — Т. 56, № 5. — С. 29–37. — Бібліогр.: 25 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859741387455463424 |
|---|---|
| author | Летичевський, О.О. Песчаненко, В.С. Харченко, В.С. Волков, В.А. Одарущенко, О.М. |
| author_facet | Летичевський, О.О. Песчаненко, В.С. Харченко, В.С. Волков, В.А. Одарущенко, О.М. |
| citation_txt | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах / О.О. Летичевський, В.С. Песчаненко, В.С. Харченко, В.А. Волков, О.М. Одарущенко // Кибернетика и системный анализ. — 2020. — Т. 56, № 5. — С. 29–37. — Бібліогр.: 25 назв. — укр. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Розглянуто сучасні тенденції в галузі автоматизованого розроблення апаратного забезпечення, зокрема, розроблення цифрових систем з використанням програмованих логічних інтегральних схем на прикладі програмованих користувачем вентильних матриць. Запропоновано модельний метод розроблення, в якому використано алгебраїчну модель специфікацій дизайну, вимог та бінарного коду для застосування формальних методів верифікації, модельного тестування та методів алгебраїчного зіставлення. Специфікаціями алгебраїчної моделі апаратного забезпечення слугує алгебра поведінок, визначена на множині дій та поведінок.
Рассмотрены современные тенденции в области автоматизированной разработки аппаратного обеспечения, в частности разработки цифровых систем с использованием программируемых логических интегральных схем на примере вентильних матриц, программируемых пользователем. Предложен модельный метод разработки, в котором использована алгебраическая модель спецификаций дизайна, требований и бинарного кода для применения формальных методов верификации, модельного тестирования и методов алгебраического сопоставления. В качестве спецификаций алгебраической модели аппаратного обеспечения служит алгебра поведений, определенная на множестве действий и поведений.
The paper considers the current trends in the field of automated hardware development, in particular, the development of digital systems using programmable logic integrated circuits on the example of FPGA (Field-Programmable Gate Array). A model-driven development method is proposed that uses an algebraic model of design specifications, requirements, and binary code to apply formal verification methods, model testing, and algebraic matching methods. The specifications of an algebraic hardware model is a behavior algebra defined over set of actions and behaviors.
|
| first_indexed | 2025-12-01T18:40:52Z |
| format | Article |
| fulltext |
ÓÄÊ 004.05, 004.42
Î.Î. ËÅÒÈ×ÅÂÑÜÊÈÉ, Â.Ñ. ÏÅÑ×ÀÍÅÍÊÎ, Â.Ñ. ÕÀÐ×ÅÍÊÎ,
Â.À. ÂÎËÊÎÂ, Î.Ì. ÎÄÀÐÓÙÅÍÊÎ
ÌÎÄÅËÜÍÈÉ ÑÏÎѲÁ ÐÎÇÐÎÁËÅÍÍß ÀËÃÎÐÈÒ̲Â
ÖÈÔÐÎÂÈÕ ÑÈÑÒÅÌ ÍÀ ÏÐÎÃÐÀÌÎÂÀÍÈÕ
ËÎò×ÍÈÕ ²ÍÒÅÃÐÀËÜÍÈÕ ÑÕÅÌÀÕ
Àíîòàö³ÿ. Ðîçãëÿíóòî ñó÷àñí³ òåíäåíö³¿ â ãàëóç³ àâòîìàòèçîâàíîãî ðîçðîá-
ëåííÿ àïàðàòíîãî çàáåçïå÷åííÿ, çîêðåìà, ðîçðîáëåííÿ öèôðîâèõ ñèñòåì
ç âèêîðèñòàííÿì ïðîãðàìîâàíèõ ëîã³÷íèõ ³íòåãðàëüíèõ ñõåì íà ïðèêëàä³
ïðîãðàìîâàíèõ êîðèñòóâà÷åì âåíòèëüíèõ ìàòðèöü. Çàïðîïîíîâàíî ìîäåëü-
íèé ìåòîä ðîçðîáëåííÿ, â ÿêîìó âèêîðèñòàíî àëãåáðà¿÷íó ìîäåëü ñïå-
öèô³êàö³é äèçàéíó, âèìîã òà á³íàðíîãî êîäó äëÿ çàñòîñóâàííÿ ôîðìàëüíèõ
ìåòîä³â âåðèô³êàö³¿, ìîäåëüíîãî òåñòóâàííÿ òà ìåòîä³â àëãåáðà¿÷íîãî ç³ñòàâ-
ëåííÿ. Ñïåöèô³êàö³ÿìè àëãåáðà¿÷íî¿ ìîäåë³ àïàðàòíîãî çàáåçïå÷åííÿ ñëóãóº
àëãåáðà ïîâåä³íîê, âèçíà÷åíà íà ìíîæèí³ ä³é òà ïîâåä³íîê.
Êëþ÷îâ³ ñëîâà: ïðîãðàìîâàí³ êîðèñòóâà÷åì âåíòèëüí³ ìàòðèö³, ñèìâîëüíå
ìîäåëþâàííÿ, àëãåáðà¿÷íå ç³ñòàâëåííÿ, àëãåáðà ïîâåä³íîê.
ÂÑÒÓÏ
Ìîäåëüíèé ñïîñ³á ðîçðîáëåííÿ ïåðåäáà÷ຠâèêîðèñòàííÿ ìîäåëåé ð³çíîãî
ð³âíÿ àáñòðàêö³¿ íà êîæíîìó åòàï³ ðîçðîáëåííÿ àïàðàòíèõ àáî ïðîãðàìíèõ
ñèñòåì. Ó ðàç³ çàñòîñóâàííÿ öüîãî ï³äõîäó ñóòòºâî çðîñòຠìîæëèâ³ñòü àâòîìà-
òèçàö³¿ ïðîºêòóâàííÿ, ùî ñïðèÿº çíà÷íîìó ï³äâèùåííþ íàä³éíîñò³ ñèñòåìè òà
íàäຠçìîãó çä³éñíèòè îïòèì³çàö³þ òåñòóâàííÿ ñèñòåìè, ¿¿ ôîðìàëüíó âå-
ðèô³êàö³þ òà ïåðåâ³ðêó â³äïîâ³äíîñò³ âèìîãàì.
Ó ö³é ñòàòò³ ðîçãëÿíóòî ïðîöåñ ðîçðîáëåííÿ öèôðîâèõ ñèñòåì ç âèêîðèñòàí-
íÿì ïðîãðàìîâàíî¿ ëîã³÷íî¿ ³íòåãðàëüíî¿ ñõåìè (Ï˲Ñ), çîêðåìà, ¿¿ ð³çíîâèäó —
ïðîãðàìîâàíî¿ êîðèñòóâà÷åì âåíòèëüíî¿ ìàòðèö³ (ÏÊÂÌ), â³äîìî¿ ÿê FPGA
(Field-Programmable Gate Array) [1].
Äëÿ ïðîºêòóâàííÿ öèôðîâèõ ñèñòåì íà ÏÊÂÌ ðåàë³çóþòü ÷³òêî âèçíà÷åíèé
ïðîöåñ ðîçðîáëåííÿ ñèñòåìè òà ¿¿ êîìïîíåíò. Âèêîðèñòîâóþòü ð³çí³ ìîäåë³
æèòòºâîãî öèêëó ðîçðîáëåííÿ çã³äíî ç â³äïîâ³äíîþ ïîñë³äîâí³ñòþ òà âèìîãàìè
ñòàíäàðò³â. Çàçâè÷àé ïðîöåñ ðîçðîáëåííÿ íà ÏÊÂÌ äëÿ êðèòè÷íèõ ñèñòåì ´ðóí-
òóºòüñÿ íà òàê çâàí³é V-ìîäåë³ [2], ÿêà ñêëàäàºòüñÿ ç åòàï³â, çàçíà÷åíèõ íà ðèñ. 1.
Íà åòàï³ ðîçðîáëåííÿ âèìîã çä³éñíþºòüñÿ çá³ð âèìîã äî ìàéáóòíüîãî ïðè-
ñòðîþ, ùî ìຠáóòè ðåàë³çîâàíèé íà ÏÊÂÌ. Âèìîãè ìîæóòü áóòè ç³áðàí³ ó âèãëÿä³
òåêñòîâèõ àáî òàáëè÷íèõ äàíèõ,
ÿêèìè ñêîðèñòàþòüñÿ ï³ä ÷àñ ðîç-
ðîáëåííÿ ³íæåíåðè òà òåñòóâàëü-
íèêè. Ñïåö³àëüíî¿ ìîâè ïðåäñòàâ-
ëåííÿ âèìîã äî àëãîðèòì³â íåìàº,
àëå ï³äòðèìêó àâòîìàòèçàö³¿ äåÿ-
êèõ åòàï³â âèñîêîð³âíåâîãî ðîç-
ðîáëåííÿ òà â³äïîâ³äíî¿ ãåíåðàö³¿
êîäó ç ð³âíÿ âèìîã ðåàë³çîâàíî ó
Mathworks, Intel (HLS Compiler),
Xilinx (HDL coder). Åòàï äèçàéíó
ïîëÿãຠâ êîíñòðóþâàíí³ àðõ³òåê-
òóðè ìàéáóòíüîãî ïðîäóêòó òà
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5 29
Çá³ð âèìîã
Äèçàéí/âåðèô³êàö³ÿ
äèçàéíó
Ãåíåðàö³ÿ
á³íàðíîãî êîäó
Âåðèô³êàö³ÿ
âëàñòèâîñòåé
Âåðèô³êàö³ÿ
åêâ³âàëåíòíîñò³,
òåñòóâàííÿ
Âàë³äàö³ÿ, òåñòóâàííÿ
Ðèñ. 1. Îñíîâí³ åòàïè ðîçðîáëåííÿ àïàðàòíîãî çàáåç-
ïå÷åííÿ
© Î.Î. Ëåòè÷åâñüêèé, Â.Ñ. Ïåñ÷àíåíêî, Â.Ñ. Õàð÷åíêî, Â.À. Âîëêîâ, Î.Ì. Îäàðóùåíêî, 2020
éîãî êîìïîíåíò çà äîïîìîãîþ ìîâ HDL (Hardware Design Level). Äî òàêèõ ìîâ
â³äíîñÿòü VHDL [3], System Verilog [4].
Îñíîâí³ êîìïàí³¿, ùî î÷îëþþòü íàïðÿì àâòîìàòèçàö³¿ äèçàéíó åëåêòðîí³êè
(EDA — Electronic Automation Design), òàê³ ÿê Cadence [5], Xilinx [6] òà
Synopsis [7], çàñòîñîâóþòü âëàñí³ ³íñòðóìåíòè ñèìóëÿö³¿ òà ðîçðîáëåííÿ. Îñîá-
ëèâî ïîïóëÿðíèìè º êîìïëåêñí³ ð³øåííÿ òà ïëàòôîðìè, íàïðèêëàä ñåðåäîâèùå
Potium [8] ô³ðìè Cadence. Çäåá³ëüøîãî äëÿ ïîòðåá äèçàéíó ÏÊÂÌ âèêîðèñòîâó-
þòü ³íòåãðîâàí³ ñåðåäîâèùà ðîçðîáíèê³â, ùî ì³ñòÿòü çàñîáè â³çóàë³çàö³¿, íàëàø-
òóâàííÿ òà òðàíñëÿö³¿ òàêèõ ìîâ ðîçðîáëåííÿ, ÿê VHDL òà System Verilog.
³äïîâ³äí³ òðàíñëÿòîðè â á³íàðíèé êîä, ðîçðîáëåí³, íàïðèêëàä, êîìïàí³ºþ Intel
(Quartus [9]), âèêîðèñòîâóþòü äëÿ ñòâîðåííÿ êîäó, ùî çàâàíòàæóºòüñÿ áåçïîñåðåäíüî
ó ÏÊÂÌ. Íà åòàï³ òåñòóâàííÿ òàêîæ çàñòîñîâóþòü âåðèô³êàö³éí³ ³íñòðóìåíòè
àíàë³çó ÷àñîâèõ âëàñòèâîñòåé òà æèâëåííÿ. Äëÿ ðîçðîáíèê³â àïàðàòíîãî çàáåçïå÷åí-
íÿ º âàæëèâèì çä³éñíåííÿ ïåðåâ³ðêè åêâ³âàëåíòíîñò³ ñïåöèô³êàö³é íà ð³çíèõ ð³âíÿõ
àáñòðàêö³¿, ÿêà ìîæå áóòè ïîðóøåíà ï³ä ÷àñ òðàíñëÿö³¿ àáî îïòèì³çàö³¿.
Ìè ðîçãëÿäàºìî äîïîâíåííÿ EDA ìîäåëüíèì ìåòîäîì ðîçðîáëåííÿ, ùî
ï³äâèùóº ñòóï³íü íàä³éíîñò³ òà áåçïåêè àïàðàòíîãî çàáåçïå÷åííÿ. Öåé ìåòîä ïå-
ðåäáà÷ຠâèêîðèñòàííÿ ôîðìàëüíèõ àëãåáðà¿÷íèõ ìîäåëåé òà ãåíåðàö³þ êàðêàñó
ñïåöèô³êàö³é íà êîæíîìó åòàï³ ðîçðîáëåííÿ.
ϳä ÷àñ ðîçãëÿäó ôîðìàëüíî¿ ìîäåë³ âèìîã ñòâîðþþòü ìîäåëü íàéâèùîãî
ð³âíÿ àáñòðàêö³¿, ÿêà âèêîðèñòîâóºòüñÿ â ñèñòåìíîìó òåñòóâàíí³. Äëÿ ìîäåë³
ìîæíà çàñòîñîâóâàòè â³äïîâ³äí³ ôîðìàëüí³ ìîâè, íàïðèêëàä BPMN (Business
Process Model and Notation) [10], UCM (Use Case Maps) [11], UML (Unified
Modeling Language) [12]. Ìàþ÷è ôîðìàëüíó ìîäåëü, ìîæíà âæå íà ïî÷àòêîâîìó
åòàï³ çàáåçïå÷èòè âåðèô³êàö³þ âèìîã òà ãåíåðàö³þ òåñò³â äëÿ âèêîðèñòàííÿ ¿õ ó
ñèñòåìíîìó òåñòóâàíí³ òà òåñòóâàíí³ ìîäåë³ äèçàéíó. Ãåíåðàö³ÿ êàðêàñà äèçàéíó
ç ôîðìàëüíèõ âèìîã çàáåçïå÷óº ñòâîðåííÿ êîäó ó ôîðìàëüí³é ìîâ³ äèçàéíó äëÿ
ïîäàëüøî¿ äåòàë³çàö³¿ ðîçðîáíèêîì. Äåòàë³çîâàíèé êîä ìîæíà ïåðåâ³ðèòè çà äîïî-
ìîãîþ òåñò³â, çãåíåðîâàíèõ íà â³äïîâ³äíîìó åòàï³, òà âåðèô³êóâàòè â³äïîâ³äíî äî
íåîáõ³äíèõ âëàñòèâîñòåé. Ç ìîäåë³ äèçàéíó àâòîìàòè÷íî ãåíåðóºòüñÿ á³íàðíèé
êîä, ÿêèé ïåðåâ³ðÿþòü çà äîïîìîãîþ òåñò³â ð³âíÿ âèìîã, âåðèô³êóþòü â³äïîâ³äíî
äî ïåâíèõ âëàñòèâîñòåé òà äîñë³äæóþòü íà âðàçëèâîñò³.
Ðîçãëÿíåìî ïðîöåñ ðîçðîáëåííÿ àïàðàòíîãî çàáåçïå÷åííÿ, â ÿêîìó ìîâó àë-
ãåáðè ïîâåä³íîê âèêîðèñòàíî ÿê ìîâó ìîäåëåé, à ¿¿ ìåòîäè çàñòîñîâàíî äëÿ âå-
ðèô³êàö³¿, òåñòóâàííÿ òà àíàë³çó áåçïåêè òà âðàçëèâîñòåé.
ÀËÃÅÁÐÀ ÏÎÂÅIJÍÎÊ ßÊ ÔÎÐÌÀËÜÍÀ ÌÎÂÀ ÌÎÄÅËÅÉ
Ðîçãëÿíåìî ìîäåë³ â êîíòåêñò³ ³íñåðö³éíîãî ìîäåëþâàííÿ [13], äå ìîäåëüîâàí³
ñóòíîñò³ âèçíà÷àþòüñÿ ÿê àãåíòè, ùî âçàºìîä³þòü ó äåÿêîìó ñåðåäîâèù³. Ñå-
ðåäîâèùå º àòðèáóòíèì, òîáòî âèçíà÷àºòüñÿ ñòàíàìè àãåíò³â òà âëàñíå ñåðåäî-
âèùà çà äîïîìîãîþ ôîðìóë íàä òèï³çîâàíèìè àòðèáóòàìè.
Àëãåáðà ïîâåä³íîê [14] º àëãåáðîþ, åëåìåíòè ÿêî¿ — öå 䳿 òà ïîâåä³íêè
àãåíò³â. Îïåðàö³ÿìè â àëãåáð³ ïîâåä³íîê º ïðåô³êñ³íã («.»), íåäåòåðì³íîâàíèé
âèá³ð («+»), ïîñë³äîâíà («;») òà ïàðàëåëüíà («||») êîìïîçèö³ÿ.
Ðîçãëÿíåìî ïðèêëàä ôðàãìåíòà ïðîºêòó FPGA, ùî ðåàë³çóº äåÿêèé àëãî-
ðèòì, ó òåðì³íàõ àëãåáðè ïîâåä³íîê. Íà ðèñ. 2 íàâåäåíî ñõåìó, ÿêà â³äîáðàæàº
âçàºìîä³þ ïðîãðàìîâàíèõ åëåìåíò³â. Ïðîãðàìîâàí³ åëåìåíòè º àãåíòàìè, ùî
âçàºìîä³þòü îäèí ç îäíèì çà äîïîìîãîþ ñèãíàë³â, ÿê³ çì³íþþòü ñòàíè ñåðåäîâè-
ùà. Ç âèêîðèñòàííÿì îïåðàö³é àëãåáðè ïîâåä³íîê ìîæíà îïèñàòè çàãàëüíó
ïîâåä³íêó ôðàãìåíòà àëãîðèòìó.
30 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5
Ïîâåä³íêà âèçíà÷àºòüñÿ òàêèì ð³âíÿííÿì àëãåáðè ïîâåä³íîê B0:
B0 = P1 || P2 || P3.
Öå ð³âíÿííÿ º ïàðàëåëüíîþ êîìïîçèö³ºþ òðüîõ ³íøèõ ïîâåä³íîê P1, P2 òà
P3. Êîæíà ïîâåä³íêà ÿâëÿº ñîáîþ â³äïîâ³äíå ð³âíÿííÿ, ùî ì³ñòèòü êîìïîçèö³¿
³íøèõ ïîâåä³íîê òà ä³é àãåíò³â. Ðîçãëÿíåìî ïîâåä³íêó Ð1:
P1 = (Aor2(or2_1, ENV, ENV, and) || Aor2(or2_2, ENV, ENV, and));
Aand (and, or2_1, or2_2, ENV).
Ïîâåä³íêè òà 䳿 ìîæóòü áóòè ïàðàìåòðèçîâàí³ ³ìåíàìè àãåíò³â, ÿê³ áåðóòü
ó÷àñòü ó 䳿 àáî ïîâåä³íö³. ²ì’ÿ ìîæå íàëåæàòè êëþ÷îâîìó àãåíòó, òîáòî òàêîìó,
ùî âèêîíóº ä³þ, òà ³íøèì àãåíòàì, ç ÿêèìè êëþ÷îâèé àãåíò âçàºìî䳺. Ó Ð1 ìè
ðîçãëÿäàºìî äâà âèäè 䳿 Aor2 òà ä³þ Aand. ÄⳠ䳿 Aor2 âèêîíóþòüñÿ ïàðàëåëüíî,
à äàë³ ïîñë³äîâíî âèêîíóºòüñÿ Aand. ²ìåíà àãåíò³â, ùî âçàºìîä³þòü ó öüîìó
ôðàãìåíò³, º òàêèìè: or2_1, or2_2, and, tctc_filter, cmpc_fp_gr, switch_mp, mul_fp,
or4. Òàêîæ ìè ìàºìî àãåíò ENV, ÿêèé âò³ëþº âñå, ùî º ïîçà ìåæàìè ôðàãìåíòó.
Òîä³, íàïðèêëàä, ïàðàìåòðèçîâàíà ä³ÿ Aor2(or2_1, ENV, ENV, and) îçíà÷àº, ùî â
ïàðàìåòðàõ º êëþ÷îâèé àãåíò or2_1, ùî âèêîíóº ä³þ, âõîäîì 䳿 º äâà ñèãíàëè ³ç
çîâí³øíüîãî ñåðåäîâèùà ENV, à âèõ³äíèé ñèãíàë ïðèéìຠàãåíò and. Àíàëîã³÷íî
ðîçïèøåìî ³íø³ ïîâåä³íêè Ð2 ³ Ð3:
P2 = Atctc_filtered(tctc_filter, ENV, ENV, 3000) +
Atctc_not_filtered(tctc_filter, ENV, ENV, 3000),
P3 = Amul_fp(mul_fp, ENV, ENV, cmpc_fp_gr, switch_fp, or4, or4, or4);
Acmpc_fp_gr (cmpc_fp_gr, mul_fp, switch_fp, or4, 5000, 0);
(Aor4(or4, cmpc_fp_gr, mul_fp, mul_fp, mul_fp, ENV) ||
Aswitch_fp(switch_fp, cmpc_fp_gr, mul_fp, ENV, ENV))
Óñ³ ïîâåä³íêè P1, Ð2, Ð3 ïðåäñòàâëåíî ÿê êîìïîçèö³þ ä³é â³äïîâ³äíèõ
àãåíò³â, õî÷à âîíè ìîæóòü ì³ñòèòè êîìïîçèö³þ ä³é ç ³íøèìè ïîâåä³íêàìè, ÿê³ òà-
êîæ ìîæíà ïàðàìåòðèçóâàòè. Ñåìàíòèêà ä³é ìຠáóòè òàêîæ ïðåäñòàâëåíà ó ôîð-
ìàëüí³é ìîâ³ ó âèãëÿä³ òàêî¿ òð³éêè: ïåðåäóìîâà, ïðîöåñíà êîìïîíåíòà òà ï³ñëÿó-
ìîâà. Öþ ñåìàíòèêó íàâåäåíî ó òàáë. 1.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5 31
out
outln
ln_1
or
or
and
ln_2
out
ln_1
ln_2ln_1
ln_2
tctc_filter
time: 3000 ms
mul_fp
ln_1
ln_2
out
out
nan
overflow
underflow
ln
cmpc_fp_gr
setpoint: 5e+3
hysteresis: 0
out
nan
ln_x2
ln_x1
ln_1 out
outsel
or
ln_2
ln_3
ln_4
switch_fp
Ðèñ. 2. Ôðàãìåíò àëãîðèòìó FPGA
Êîæíà ä³ÿ º ïàðàìåòðèçîâàíîþ â³äíîñíî àãåíòà, ÿêèé ¿¿ âèêîíóº, òà âõ³äíèõ ³
âèõ³äíèõ äàíèõ. Ïåðåäóìîâà âèçíà÷àº, ÷è ìîæíà çàñòîñóâàòè ïåâíó ä³þ çà ïåâ-
íèõ çíà÷åíü ïàðàìåòð³â. ßêùî ïàðàìåòðè º êîíêðåòíèìè, òî ïåðåäóìîâà 䳿 ìàº
áóòè ³ñòèííîþ, à ÿêùî — ñèìâîëüíèìè àáî äîâ³ëüíèìè, òî ïåðåäóìîâà ìຠáóòè
âèêîíóâàíîþ äëÿ äåÿêèõ çíà÷åíü ïàðàìåòð³â ïåðåäóìîâè. ϳñëÿóìîâà âèçíà÷àº,
ÿê çì³íèòüñÿ ñåðåäîâèùå, çîêðåìà âèõ³äí³ äàí³. Ïðîöåñíà êîìïîíåíòà 䳿
³ëþñòðóº ä³þ îòðèìàííÿì àáî ïîñèëàííÿì ñèãíàëó äî ³íøèõ àãåíò³â.
ÀËÃÅÁÐÀ¯×ÍÈÉ Ï²ÄÕ²Ä Ó ÌÎÄÅËÜÍÎÌÓ ÌÅÒÎIJ ÐÎÇÐÎÁËÅÍÍß
Íàÿâí³ñòü àëãåáðà¿÷íî¿ ìîäåë³ íà êîæíîìó ç åòàï³â íàäຠçìîãó âèêîðèñòîâó-
âàòè ìåòîäè àëãåáðè ïîâåä³íêè äëÿ âåðèô³êàö³¿ òà àíàë³çó âëàñòèâîñòåé ìîäå-
ëåé. Íà ðèñ. 3 íàâåäåíî æèòòºâèé öèêë ðîçðîáëåííÿ ç âèêîðèñòàííÿì àëãåá-
ðà¿÷íî¿ ìîäåë³.
Íà åòàï³ âèìîã àëãåáðà¿÷íó ìîäåëü ìîæíà îòðèìàòè ó äâà ñïîñîáè — àáî
ñòâîðèòè âðó÷íó ó âèãëÿä³ ð³âíÿííÿ àëãåáðè ïîâåä³íîê ³ç ä³ÿìè, àáî òðàíñëþâàòè
ç ìîâ âåðõíüîãî ð³âíÿ, ÿêèìè çàïèñóþòü âèìîãè. Îòæå, íà öüîìó åòàï³ ìîæíà âè-
êîðèñòîâóâàòè ìåòîäè àëãåáðè ïîâåä³íêè äëÿ âåðèô³êàö³¿ âëàñòèâîñòåé âèìîã,
ïðè öüîìó ìîäåëü ìîæå ñëóãóâàòè òåñòîâîþ íà çàâåðøàëüíîìó åòàï³ ðîçðîáëåí-
32 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5
Ò à á ë è ö ÿ 1
ijÿ ç ïàðàìåòðàìè Ïåðåäóìîâà Ïðîöåñíà êîìïîíåíòà ϳñëÿóìîâà
Acmpc_fp_gr(s, x1, x2, y,
setpoint : real, hysteresis : real)
Ëîêàëüí³ ïàðàìåòðè 䳿:
(in : real, out : bool,
nan : bool)
1
receive(x1 : signal(in)),
send(x2 : signal (out),
signal (y : nan))
out = (in > setpoint
– hysteresis)
Aor2(s, x1, x2, x3) Ëîêàëüí³
ïàðàìåòðè 䳿: (in_1, in_2,
out : bool)
1
receive(x1 : signal (in_1)),
receive(x2 : signal (in_2)),
send(y : signal(out))
out = (in_1 || in_2)
Aor4(s, x1, x2, x3, x4, out)
Ëîêàëüí³ ïàðàìåòðè 䳿:
(in_1, in_2, in_3, in_4,
out : bool)
1
receive(x1 : signal (in_1)),
receive(x2 : signal (in_2)),
receive(x3 : signal (in_3)),
receive(x4 : signal (in_4)),
send(y : signal(out))
out = (in_1 || in_2 ||
in_3 || in_4)
Aand(s, x1, x2, y)
Ëîêàëüí³ ïàðàìåòðè 䳿:
(in_1, in_2, out : bool)
1
receive(x1 : signal (in_1)),
receive(x2 : signal (in_2)),
send(y : signal(out))
out = (in_1 && in_2)
Amul_fp(s, x1, x2, y0, y1,
y2, y3, y4)
Ëîêàëüí³ ïàðàìåòðè 䳿:
(in_1 : real, in_2 : real,
out : real, overflow : bool, un-
derflow : bool, nan : bool)
1
receive(x1 : signal(in_1)),
receive(x2 : signal(in2)),
send(y0 : signal(out)),
send(y1 : signal(out)),
send(y2 : signal(overflow)),
send(y3 : signal(under-
flow)), send(y4 : sig-
nal(nan))
out = (in_1 * in_2);
overflow =
(out > maxReal32);
underflow = (out
< minReal32)
Atctc_filtered(s, x, y, n)
Ëîêàëüí³ ïàðàìåòðè 䳿:
(in, out : bool)
(TIMER == 0)
receive(x : signal (in)),
send(y : signal (out))
in == out
Atctc_filtered(s, x, y, n)
Ëîêàëüí³ ïàðàìåòðè 䳿:
(in, out : bool)
(TIMER == 1) receive(x : signal (in)) 1
Aswitch_fp(s, x1, x2, x3, y)
Ëîêàëüí³ ïàðàìåòðè 䳿:
(sel : bool, in_x1 : real,
in_x2 : real, out : real)
1
receive(x1 : signal(in_x1)),
receive(x2 : signal(in_x2)),
receive(x3 : signal(sel)),
send(y : signal(out))
(sel == 0) && (out
== in_x1) || (sel ==
1) && (out ==
in_x2)
íÿ, ÿêèì º òåñòóâàííÿ òà âàë³äàö³ÿ (ïåðåâ³ðêà ñèñòåìíî¿ ôóíêö³îíàëüíîñò³). Ìàþ-
÷è ìîäåëü, ìîæíà ãåíåðóâàòè êàðêàñ ìîâîþ äèçàéíó äëÿ ïîäàëüøî¿ äåòàë³çàö³¿,
ÿêùî ìîâè äèçàéíó òà âèìîã íå çá³ãàþòüñÿ.
Àëãåáðà¿÷íà ìîäåëü, îòðèìàíà íà åòàï³ äèçàéíó ìåòîäîì òðàíñëÿö³¿ ç ìîâè
äèçàéíó, ìîæå ñëóãóâàòè ÿê îá’ºêòîì âåðèô³êàö³¿, òàê ³ òåñòîâîþ ìîäåëëþ äëÿ
òåñòóâàííÿ á³íàðíîãî êîäó. Îòðèìàíèé á³íàðíèé êîä òåæ ìîæíà òðàíñëþâàòè â
àëãåáðà¿÷íó ìîäåëü äëÿ àíàë³çó áåçïåêè, âðàçëèâîñòåé òà âëàñòèâîñòåé, ÿê³ ïå-
ðåâ³ðÿþòü íà íàéíèæ÷îìó ð³âí³, òîáòî íàïðóãè, òåìïåðàòóðè, åëåêòðîìàãí³òíèõ
âëàñòèâîñòåé òîùî.
Óñ³ òðè ìîäåë³ ð³çíèõ ð³âí³â àáñòðàêö³¿ ìîæíà ïåðåâ³ðèòè çà äîïîìîãîþ
ôîðìàëüíèõ ìåòîä³â íà åêâ³âàëåíòí³ñòü.
ÂÅÐÈÔ²ÊÀÖ²ß ÌÎÄÅËÅÉ
Âåðèô³êàö³ÿ ìîäåë³ ïîëÿãຠâ äîñë³äæåíí³ ïîâåä³íêîâèõ âëàñòèâîñòåé áåçïåêè
àáî æèòòºçäàòíîñò³.
Ôîðìàëüí³ ìåòîäè àëãåáðè ïîâåä³íîê, ÿê³ âèêîðèñòîâóþòüñÿ äëÿ äîâåäåííÿ
äîñÿæíîñò³ âëàñòèâîñòåé, ùî ïåðåâ³ðÿþòüñÿ, ìîæóòü áóòè ñòàòè÷íèìè, äè-
íàì³÷íèìè, êîìá³íîâàíèìè òà ÷àñòêîâî äèíàì³÷íèìè. Âõîäîì ó ïðîöåäóðó âå-
ðèô³êàö³¿ º ìîäåëü ó âèãëÿä³ àëãåáðè ïîâåä³íîê òà ôîðìóëà âëàñòèâîñò³, ùî ïå-
ðåâ³ðÿºòüñÿ, à âèõîäîì º âåðäèêò, ÿêèé ï³äòâåðäæóº ¿¿ äîñÿæí³ñòü, òà ñöåíàð³é,
ðåàë³çàö³ÿ ÿêîãî ïðèçâîäèòü äî â³äïîâ³äíîãî ñòàíó.
Äî ñòàòè÷íèõ ìåòîä³â â³äíîñÿòü òàê³, äëÿ ÿêèõ äîñòàòíüî äîâåäåííÿ âëàñòè-
âîñò³ âèêîíóâàíîñò³, ùî çàäàíà ôîðìóëîþ â áàçîâ³é ìîâ³, òîáòî ³ñíóþòü òàê³ çíà-
÷åííÿ àòðèáóò³â ôîðìóëè, äëÿ ÿêèõ ôîðìóëà ìîæå áóòè ³ñòèííîþ. Äîâåäåííÿ
âëàñòèâîñò³ âèêîíóâàíîñò³ çä³éñíþºòüñÿ çà äîïîìîãîþ òàêèõ ìàøèí ðîçâ’ÿçóâàí-
íÿ, ÿê Microsoft Z3 [15] òà cvc4 [16].
Äèíàì³÷í³ ìåòîäè çàñòîñîâóþòü äî ïîâåä³íêîâèõ âëàñòèâîñòåé, òîáòî âëàñ-
òèâîñòåé, äå ôîðìóëà ïðåäñòàâëåíà çà äîïîìîãîþ âèðàç³â àëãåáðè ïîâåä³íêè, òà
ñåìàíòèêè ä³é, äå ôîðìóëà ïðåäñòàâëåíà ÿê âèðàç â áàçîâ³é ìîâ³. Òàê³ ìåòîäè ïî-
òðåáóþòü ñèìâîëüíîãî ìîäåëþâàííÿ òà ðîçâ’ÿçàííÿ ñèñòåìè ïîâåä³íêîâèõ
ð³âíÿíü. Óñ³ çàçíà÷åí³ ìåòîäè àëãåáðè ïîâåä³íêè íàâåäåíî â ðîáîòàõ [17, 18].
Êîìá³íîâàíèìè ìåòîäàìè º ò³, äëÿ ÿêèõ äîâåäåííÿ âèêîíóâàíîñò³ ôîðìóë íå º
äîñòàòí³ì ³ ïîòð³áíî äîâåñòè äîñÿæí³ñòü ôîðìóëè ñèìâîëüíèì ìîäåëþâàííÿì.
×àñòêîâî â äèíàì³÷íèõ ìåòîäàõ âèêîðèñòîâóþòü òåõí³êó ãåíåðàö³¿ ³íâàð³àíò³â [19]
â àëãåáð³ ïîâåä³íîê.
Îñíîâíèìè ìåòîäàìè âåðèô³êàö³¿, ùî çàñòîñîâóþòüñÿ äëÿ àïàðàòíîãî çàáåç-
ïå÷åííÿ â ìåæàõ àëãåáðè ïîâåä³íîê, º òàê³:
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5 33
Çá³ð âèìîã
Äèçàéí/âåðèô³êàö³ÿ äèçàéíó
Ãåíåðàö³ÿ á³íàðíîãî êîäó Âåðèô³êàö³ÿ âëàñòèâîñòåé
Âåðèô³êàö³ÿ åêâ³âàëåíòíîñò³,
òåñòóâàííÿ
Âàë³äàö³ÿ, òåñòóâàííÿ
VHDL, SystemVerilog,
OpenVera, SystemC
RTL
pof, sof-files Ñèìóëÿö³ÿ
á³íàðíèõ ôàéë³â
Àëãåáðà¿÷íà
ìîäåëü 1
Àëãåáðà¿÷íà
ìîäåëü 2
Àëãåáðà¿÷íà
ìîäåëü 3
Ãåíåðàö³ÿ òåñò³â
Ãåíåðàö³ÿ
òåñò³â
Ãåíåðàö³ÿ ìîäåë³
Ãåíåðàö³ÿ ìîäåë³
Ãåíåðàö³ÿ
êàðêàñó äèçàéíó
Ãåíåðàö³ÿ ìîäåë³
Àëãåáðà¿÷íå
ç³ñòàâëåííÿ
Ïåðåâ³ðêà
åêâ³âàëåíòíîñò³
ìîäåëåé
VHDL, SystemVerilog,
Mathworks, Intel (HLS
Compiler), Xillinx
(HDL coder)
Ðèñ. 3. Ñïîñ³á ðîçðîáëåííÿ ç âèêîðèñòàííÿì àëãåáðà¿÷íèõ ìîäåëåé
— ñòàòè÷íà ïåðåâ³ðêà íåñóì³ñíîñò³ (íåäåòåðì³í³çìó) â àëãîðèòìàõ ñõåì
øëÿõîì ïåðåâ³ðêè âèêîíóâàíîñò³ ôîðìóëè � �
i
a i( ) 0, äå à ³( ) — ïåðåäóìîâà 䳿;
— ïåðåâ³ðêè íåïîâíîòè (òóïèêè) â àëãîðèòìàõ ñõåì øëÿõîì ïåðåâ³ðêè âèêî-
íóâàíîñò³ ôîðìóëè � �
i
a i( ) 0;
— ïåðåâ³ðêà ñóì³ñíîñò³ ÷àñîâèõ âëàñòèâîñòåé òà ïðîáëåì ñèíõðîí³çàö³¿. Ö³
âëàñòèâîñò³ ïåðåâ³ðÿþòü øëÿõîì ñèìâîëüíîãî ìîäåëþâàííÿ ïîâåä³íêîâèõ
ð³âíÿíü ³ç äåÿêîãî ïî÷àòêîâîãî ñòàíó, çàäàíîãî ôîðìóëîþ íàä àòðèáóòíèì ñåðå-
äîâèùåì. ϳä ÷àñ ìîäåëþâàííÿ ïåðåäóìîâó ðàçîì ³ç ïîòî÷íèì ñòàíîì ñåðåäîâè-
ùà ïåðåâ³ðÿþòü íà âèêîíóâàí³ñòü. ßêùî âîíà º, òî ñòàí ñåðåäîâèùà çì³íþºòüñÿ
â³äïîâ³äíî äî ï³ñëÿóìîâè;
— ïåðåâ³ðêà äîñÿæíîñò³ êðèòè÷íèõ ñòàí³â, çàäàíèõ ôîðìóëîþ íàä àòðèáóò-
íèì ñåðåäîâèùåì, ùî âèðàæàþòü ñòàí «ãîëîäóâàííÿ», êîëè âñ³ àãåíòè ÷åêàþòü
îòðèìàííÿ ñèãíàë³â, ñòàí ïîðóøåííÿ îáìåæåíü àáî ³íø³ âëàñòèâîñò³ áåçïåêè, ùî
ìîæóòü áóòè çàäàí³ êîðèñòóâà÷åì. Òàê³ âëàñòèâîñò³ ìîæóòü áóòè ÿê ëîêàëüíèìè
(àíîòàö³¿ â êîä³ äèçàéíó, àíãë. assertion), òàê ³ ãëîáàëüíèìè;
— ïåðåâ³ðêà ïåðåãîí³â ñèãíàë³â, êîëè ð³çíà ïîñë³äîâí³ñòü îòðèìàííÿ ñèã-
íàë³â ñòâîðþº ð³çí³ ñòàíè ñåðåäîâèùà, çà äîïîìîãîþ ñèìâîëüíîãî ìîäåëþâàííÿ
àáî ãåíåðàö³¿ ³íâàð³àíò³â;
— ïåðåâ³ðêà âëàñòèâîñòåé æèòòºä³ÿëüíîñò³, ùî âèðàæàþòü äîñÿæí³ñòü áàæà-
íîãî ñòàíó, çà äîïîìîãîþ ñèìâîëüíîãî ìîäåëþâàííÿ.
ÌÎÄÅËÜÍÅ ÒÅÑÒÓÂÀÍÍß
Àëãåáðà¿÷íà ìîäåëü ìîæå ñëóãóâàòè ìîäåëëþ äëÿ ãåíåðàö³¿ òðàñ, ÿê³ âèêîðèñ-
òîâóþòüñÿ äëÿ ñòâîðåííÿ òåñòîâîãî íàáîðó ó â³äïîâ³äíîìó ñåðåäîâèù³ òåñòó-
âàííÿ. Ïåðåâ³ðêó â³äïîâ³äíîñò³ àðòåôàêò³â ìîäåë³ ìîæíà çä³éñíþâàòè íà
êîæí³é ôàç³ ðîçðîáëåííÿ. Òåñòóâàòè ìîæíà ÿê ñïåöèô³êàö³¿ äèçàéíó, òàê ³
á³íàðíèé êîä. Îñíîâíèìè ìåòîäàìè ãåíåðàö³¿ òåñò³â º ïðÿìå òà îáåðíåíå ñèì-
âîëüíå ìîäåëþâàííÿ. Âèìîãè äî ãåíåðàö³¿ òåñò³â âèçíà÷àþòü íåîáõ³äíå ïî-
êðèòòÿ òåñòàìè ðÿäê³â êîäó.
Ïîêðèòòÿ òàêîæ âèçíà÷àºòüñÿ ìîäåëëþ, ÿêà ìîæå ïåðåäáà÷àòè âè÷åðïíå òåñ-
òóâàííÿ, òîáòî ãåíåðàö³þ âñ³õ ìîæëèâèõ ñòàí³â ïîâåä³íêè ìîäåë³, ïîêðèòòÿ ä³é ó
ìîäåë³ àáî ïîêðèòòÿ âñ³õ ïåðåõîä³â ì³æ ä³ÿìè. Äëÿ àïàðàòíîãî çàáåçïå÷åííÿ òåñ-
òîì ââàæàþòü ïîñë³äîâí³ñòü ïðèéîì³â òà â³äïðàâëåíü ñèãíàë³â ì³æ àãåíòàìè. ϳä
÷àñ âèêîíàííÿ òåñò³â ðîçð³çíÿþòü ³íñòàíö³þ, ùî òåñòóº, òà ³íñòàíö³þ, ùî òåñ-
òóºòüñÿ. Ó öüîìó ïðîöåñ³ çä³éñíþþòü â³äïðàâëåííÿ ñèãíàë³â íà ³íñòàíö³þ, ùî
òåñòóºòüñÿ, òà ïîð³âíþþòü ðåçóëüòàò ç î÷³êóâàíèì.
Ó ðàç³ âèêîðèñòàííÿ àëãåáðè ïîâåä³íîê ðîçãëÿäàþòü òàê³ âèäè òåñòóâàííÿ:
— òåñòóâàííÿ ìåòîäîì «÷îðíî¿ ñêðèíüêè», òîáòî çà äîïîìîãîþ íàáîðó
òåñò³â, äå êîä ³íñòàíö³¿, ùî òåñòóºòüñÿ, º íåâ³äîìèì;
— òåñòóâàííÿ ìåòîäîì «á³ëî¿ ñêðèíüêè», äå ïðîöåñ âèçíà÷àºòüñÿ ñèìâîëü-
íèì âèêîíàííÿì ïàðàëåëüíî¿ êîìïîçèö³¿ ìîäåë³ òà êîäó. ϳä ÷àñ òåñòóâàííÿ
ïîð³âíþþòü íà åêâ³âàëåíòí³ñòü ñòàíè ñåðåäîâèùà.
ʲÁÅÐÁÅÇÏÅÊÀ: ÏÎØÓÊ ÂÐÀÇËÈÂÈÕ ÏÎÂÅIJÍÎÊ
Çà äîïîìîãîþ ìîäåëåé àëãåáðè ïîâåä³íîê ìîæíà îö³íþâàòè çäàòí³ñòü àëãîðèò-
ìó âèòðèìóâàòè àòàêè çëîâìèñíèê³â òà â³äïîâ³äíî çíàõîäèòè âðàçëèâ³ ïî-
âåä³íêè â ìîäåëÿõ. Äî òàêèõ óðàçëèâîñòåé â³äíîñÿòü âèò³ê äàíèõ àáî ìîæ-
ëèâ³ñòü ïåðåçàïèñó ³íôîðìàö³¿ ó ÏÊÂÌ. ϳä ÷àñ îö³íþâàííÿ îï³ðíîñò³ äî
àòàê, ùî ïðèçâîäÿòü äî ïîìèëîê, àíàë³çóþòü çäàòí³ñòü ñèñòåìè çáåð³ãàòè
êîíô³äåíö³éíó ³íôîðìàö³þ.
34 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5
Óðàçëèâó ïîâåä³íêó àáî ïîâåä³íêó çëîâìèñíèêà ìîäåëþþòü çà äîïîìîãîþ
øàáëîí³â. Øàáëîíîì º âèðàç â àëãåáð³ ïîâåä³íîê, ùî ì³ñòèòü 䳿, ÿê³ ïðåäñòàâëÿ-
þòü óðàçëèâîñò³, òà íåâ³äîì³ ïîâåä³íêè, ùî ïðèçâîäÿòü äî íèõ. Íàïðèêëàä, ÿêùî
ìàºìî 䳿 ÷èòàííÿ ³íôîðìàö³¿ À òà îòðèìàííÿ ñèãíàëó, ùî ì³ñòèòü ïðî÷èòàíó
³íôîðìàö³þ, òî øàáëîí ìຠâèä òàêî¿ ïîâåä³íêè:
S read A X send A� ( ). ; ( ),
äå Õ — äîâ³ëüíà ïîâåä³íêà.
Çàäà÷à ïîëÿãຠâ ïîøóêó ïîâåä³íêè X ó ìîäåë³, òà òèõ øëÿõ³â, ùî âåäóòü äî
öèõ ä³é. Òàêó çàäà÷ó ðîçâ’ÿçóþòü çà äâà åòàïè. Ïåðøèé åòàï — öå ðîçâ’ÿçàííÿ
ð³âíÿííÿ àëãåáðè ïîâåä³íîê, ùî âèçíà÷ຠìîäåëü. Íàïðèêëàä, íåõàé B0 — ñèñòå-
ìà ð³âíÿíü àëãåáðè ïîâåä³íîê:
B R a a B B0 1 2 1 2� � �( , , , , , , ),
B R a a B B1 11 12 11 12� � �( , , , , , ) , …,
äå B B B B1 2 11 12, , , ,� � — ïîâåä³íêè, a a1 2, ,� — 䳿.
Ïîòð³áíî çíàéòè òàêó ïîâåä³íêó Y , ùî B Y0 � ;S i S — øàáëîí óðàçëèâîñò³.
Ðåçóëüòàòîì ìîæå áóòè ïîñë³äîâí³ñòü ä³é, ÿêà âåäå äî âðàçëèâîñò³, ùî ñêëàäàº
äåÿêó òðàñó àáî ìíîæèíó òðàñ. Âèçíà÷èâøè òðàñó, ìàºìî ùå äîâåñòè, ùî òàêèé
ñöåíàð³é ïîâåä³íêè º äîñÿæíèì, òîáòî º â³äïîâ³äí³ çíà÷åííÿ àòðèáóò³â ñåðåäîâè-
ùà. Äîâåäåííÿ äîñÿæíîñò³ º äðóãèì åòàïîì çàäà÷³ òà ðåàë³çóºòüñÿ ç âèêîðèñòàí-
íÿì ìåòîäó ñèìâîëüíîãî ìîäåëþâàííÿ. Ìàþ÷è òðàñó ç â³äïîâ³äíèìè ôîðìóëàìè
ñòàí³â ñåðåäîâèùà, ìîæíà çãåíåðóâàòè êîíêðåòí³ çíà÷åííÿ òà îòðèìàòè åêñïëîéò
(exploit), òîáòî äàí³, äëÿ ÿêèõ çä³éñíåííÿ àòàêè º ìîæëèâèì.
Îòæå, àëãåáðà ïîâåä³íîê º âàæëèâîþ òåõíîëî㳺þ â ìîäåëüíîìó ñïîñîá³ ðîç-
ðîáëåííÿ ³ ïîð³âíÿíî ³ç ñèìóëÿö³ºþ, ÿêó íàé÷àñò³øå âèêîðèñòîâóþòü äëÿ âå-
ðèô³êàö³¿ ÏÊÂÌ, çàáåçïå÷óº á³ëüøå ìîæëèâîñòåé äëÿ àíàë³çó íàä³éíîñò³ àïàðàò-
íîãî çàáåçïå÷åííÿ. Âèêîðèñòàííÿ àëãåáðà¿÷íèõ ìåòîä³â ñïðèÿº çíà÷íîìó çìåíøåí-
íþ â³äñîòêîâî¿ ÷àñòêè ïîìèëêîâî ïîçèòèâíèõ àðòåôàêò³â ³ ï³äâèùåííþ òî÷íîñò³
âèÿâëåííÿ âðàçëèâîñòåé òà àðòåôàêò³â âåðèô³êàö³¿. Àëãåáðà¿÷í³ ìîäåë³ â ðîçðîá-
ëåíí³ ñèñòåì íà ÏÊÂÌ ìîæíà ïåðåâ³ðÿòè íà åêâ³âàëåíòí³ñòü çà äîïîìîãîþ ôîð-
ìàëüíèõ ìåòîä³â, ùî ãàðàíòóº ïðàâèëüíèé ðåçóëüòàò íà â³äì³íó â³ä ñèìóëÿö³¿.
Íàñòóïíèì ëîã³÷íèì êðîêîì äîñë³äæåíü º ïîºäíàííÿ ìîäåëüíèõ ìåòîä³â ç
ìåòîäàìè âåðèô³êàö³¿, ÿê³ ´ðóíòóþòüñÿ íà ³í’ºêòóâàíí³ äåôåêò³â ³/àáî âðàçëèâîñ-
òåé ó ïðîºêòè ÏÊÂÌ, à òàêîæ âèçíà÷åíí³ â³äïîâ³äíèõ ìåòðèê äëÿ îö³íþâàííÿ
ïîâíîòè ³ äîñòîâ³ðíîñò³ ïåðåâ³ðêè [20–22]. Äî òîãî æ, ö³êàâèì ç òåîðåòè÷íîãî
³ ïðàêòè÷íîãî ïîãëÿäó º âèêîðèñòàííÿ ôîðìàëüíèõ ìåòîä³â äëÿ ñòâîðåííÿ äèâåð-
ñíèõ ïðîºêò³â òà ïåðåâ³ðêè íàÿâíèõ ïðîºêò³â íà äèâåðñí³ñòü [23, 24].
ÂÈÑÍÎÂÊÈ
Àïðîáàö³þ ìåòîäó çä³éñíåíî ó ìåæàõ âèêîíàííÿ ïðîìèñëîâèõ ïðîºêò³â ÍÂÏ
«Ðàä³é», ì. Êðîïèâíèöüêèé. ϳä ÷àñ ðîçâ’ÿçàííÿ çàäà÷ ôîðìàëüíî¿ âåðèô³êàö³¿
îòðèìàíî òàê³ âàãîì³ ðåçóëüòàòè:
� ïîáóäîâàíî àëãåáðà¿÷íèé îïèñ îáðàíîãî ôðàãìåíòà ñïåöèô³êàö³¿ âèìîã
äëÿ åëåêòðîííèõ êîìïîíåíò ïðîºêòó, ÿê³ ðåàë³çîâàíî ìîâîþ VHDL. Äëÿ ôðàã-
ìåíòà ñïåöèô³êàö³¿ âèìîã âèêîíàíî àíàë³ç íàÿâíîñò³ ïîðóøåíü õàðàêòåðèñòèê íå-
ñóïåðå÷ëèâîñò³, ïîâíîòè òà ³í., ùî º îñîáëèâî âàæëèâèì äëÿ ïðîöåñ³â âå-
ðèô³êàö³¿ öèôðîâèõ ïðèñòðî¿â. Îäåðæàíî òåñòîâ³ íàáîðè äëÿ çä³éñíåííÿ
ôóíêö³îíàëüíî¿ (ïîâåä³íêîâî¿) ñèìóëÿö³¿ ðîáîòè îáðàíîãî á³áë³îòå÷íîãî êîìïî-
íåíòà. Öåé ðåçóëüòàò íàäຠçìîãó çíèçèòè ñóá’ºêòèâí³ ðèçèêè âèêîíàííÿ ïî-
âåä³íêîâîãî òåñòóâàííÿ, òîáòî ðèçèêè ÿêîñò³ ôîðìóëþâàííÿ âèìîã ðîçðîáíèêîì
òà ¿õíüîãî ðîçóì³ííÿ òåñòóâàëüíèêîì, à òàêîæ ÿêîñò³ òà ê³ëüêîñò³ òåñòîâèõ íà-
áîð³â, ÿê³ ðîçðîáëÿþòüñÿ òà âèêîíóþòüñÿ ç öèôðîâèì ïðèñòðîºì.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5 35
� âèêîíàíî àëãåáðà¿÷íèé îïèñ íàáîðó ñöåíàð³¿â ëîã³ê êîðèñòóâà÷à User
Application Logic (UAL), ÿê³ âèêîíóþòüñÿ ïðîãðàìîâàíèì ëîã³÷íèì êîíòðîëåðîì
(ÏËÊ), ïðè öüîìó âèçíà÷åíî éìîâ³ðí³ êðèòè÷í³ øëÿõè âèêîíàííÿ öèõ ëîã³ê.
Çàãàëîì îòðèìàí³ ðåçóëüòàòè º âàæëèâèìè òà êîðèñíèìè äëÿ ï³äâèùåííÿ
íàä³éíîñò³ òà ôóíêö³îíàëüíî¿ áåçïåêè [25] öèôðîâî¿ ³íôîðìàö³éíî-êåðóâàëüíî¿
ïëàòôîðìè RadICS (âèðîáíèöòâî ÍÂÏ «Ðàä³é», ì. Êðîïèâíèöüêèé) ï³ä ÷àñ
ðåàë³çàö³¿ ïðîöåñ³â ¿¿ ðîçðîáëåííÿ, òåñòóâàííÿ, ñåðòèô³êàö³¿ òà ë³öåíçóâàííÿ íà
â³äïîâ³äí³ñòü íîðìàì ì³æíàðîäíèõ ñòàíäàðò³â.
ÑÏÈÑÎÊ Ë²ÒÅÐÀÒÓÐÈ
1. FPGA. URL: www.intel.com/content/www/us/en/products/programmable/fpga/new-to-fpgas/resource
-center/overview.html.
2. V-model. URL: https://www.testingexcellence.com/v-model-in-software-testing/.
3. VHDL. URL: www.intel.com/content/www/us/en/programmable/support/support-resources/design-examples/
design-software/vhdl.html.
4. SystemVerilog. URL: www.asic-world.com/systemverilog/tutorial.html.
5. Cadence. URL: www.cadence.com/.
6. Xilinx. URL: www.xilinx.com.
7. Synopsis. URL: www.synopsys.com.
8. Potium. URL: www.cadence.com/en_US/home/tools/system-design-and-verification/fpga-basedpro
totyping/protium-s1-fpga-based-prototyping-platform.html.
9. Quartus. URL: www.intel.com/content/www/us/en/programmable/downloads/download-center.html
10. BPMN. URL: www.bpmn.org/.
11. ITU-T Recommendation, Z.151, User Requirements Notation (URN) — Language definition.
12. UML. URL: www.uml.org/.
13. Letichevsky A., Letychevskyi O., Peschanenko V. Insertion modeling and its applications. Computer
Science Journal of Moldova. 2016. Vol. 24, Iss. 3. P. 357–370.
14. Letichevsky A., Gilbert D. A model for interaction of agents and environments. In: Recent Trends in
Algebraic Development Technique. LNCS. Bert D., Choppy C. (Eds.). Berlin; Heidelberg: Springer-Verlag,
2000. Vol. 1827. P. 311–328.
15. Z3 decision procedure. URL: https://github.com/Z3Prover/z3.
16. CVC4 decision procedure. URL: http://cvc4.cs.stanford.edu.
17. Letichevsky A. Algebra of behavior transformations and its applications. In: Structural Theory of
Automata, Semigroups, and Universal Algebra, NATO Science Series II: Mathematics, Physics and
Chemistry. Kudryavtsev V.B., Rosenberg I.G. (Eds.). Dordrecht: Springer, 2005. Vol. 207. P. 241–272.
18. Letychevskyi O., Letichevsky A. Predicate transformers and system verification. Proc. Third
International Workshop on Symbolic Computation in Software Science (SCSS 2010). (29–30 July
2010, Hagenberg, Austria). Hagenberg, 2010. P. 148-149.
19. Letychevskyi O., Letichevsky A., Godlevsky A., Guba A., Peschanenko V., Kolchin A. Invariants in
symbolic modeling and verification of requirements. Proc. 9th Conference Computer Science and
Information Technologies (CSIT 2013). (23–27 September 2013, Yerevan, Armenia). Yerevan,
2013. P. 23–27.
19. Reva L., Kulanov L., Kharchenko V. Design fault injection-based technique and tool for FPGA
projects verification. Proc. 9th East-West Design & Test Symposium (EWDTS 2011). (9–12 Sep-
tember 2011, Sevastopol, Ukraine). Sevastopol, 2011. P. 1–6.
21. Kharchenko V., Odarushchenko O., Sklyar V., Ivasyuk A. Fault insertion testing of FPGA-based
NPP I&C systems: SIL certification issues. Proc. International Conference on Nuclear Engineering
(ICONE 22). (11–14 July 2014, Prague, Czech Republic). Prague, 2014. Vol. 6. P. 1–8.
https://doi.org/10.1115/ICONE22-31163.
22. Yasko A., Babeshko E., Kharchenko V. Verification of FPGA based NPP I&C systems considering
multiple faults: Technique and automation tool. Proc. International Conference on Nuclear
Engineering (ICONE 25). (2–6 July 2017, Shanghai, China). Shanghai, 2017. Vol. 9. P. 1–9. https://
doi.org/10.1115/ICONE25-67065.
36 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5
23. Kharchenko V., Illiashenko O. Diversity for security: case assessment for FPGA-based safety-critical
systems. MATEC Web of Conferences. 2016. Vol. 76. P. 1–9. https://doi.org/10.1051/matecconf/
20167602051.
24. Illiashenko O., Kharchenko V., Panarin A., Sklyar V. Hardware diversity for safety of critical
instrumentation and control systems. Proc. 9th IEEE International Conference on Intelligent Data
Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS 2017).
(21–23 September 2017, Bucharest, Romania). Bucharest, 2017. P. 907–911.
25. IEC 61508:2010. Functional safety of electrical/electronic/programmable electronic safety-related
systems. IEC Standards, 2010. 594 p. URL: https://www.iec.ch/functionalsafety/standards/page2.htm.
Íàä³éøëà äî ðåäàêö³¿ 27.02.2020
À.À. Ëåòè÷åâñêèé, Â.Ñ. Ïåñ÷àíåíêî, Â.Ñ. Õàð÷åíêî,
Â.À. Âîëêîâ, Î.Í. Îäàðóùåíêî
ÌÎÄÅËÜÍÛÉ ÑÏÎÑÎÁ ÐÀÇÐÀÁÎÒÊÈ ÀËÃÎÐÈÒÌÎÂ ÖÈÔÐÎÂÛÕ ÑÈÑÒÅÌ
ÍÀ ÏÐÎÃÐÀÌÌÈÐÓÅÌÛÕ ËÎÃÈ×ÅÑÊÈÕ ÈÍÒÅÃÐÀËÜÍÛÕ ÑÕÅÌÀÕ
Àííîòàöèÿ. Ðàññìîòðåíû ñîâðåìåííûå òåíäåíöèè â îáëàñòè àâòîìàòèçèðî-
âàííîé ðàçðàáîòêè àïïàðàòíîãî îáåñïå÷åíèÿ, â ÷àñòíîñòè ðàçðàáîòêè öèôðî-
âûõ ñèñòåì ñ èñïîëüçîâàíèåì ïðîãðàììèðóåìûõ ëîãè÷åñêèõ èíòåãðàëüíûõ
ñõåì íà ïðèìåðå âåíòèëüíèõ ìàòðèö, ïðîãðàììèðóåìûõ ïîëüçîâàòåëåì.
Ïðåäëîæåí ìîäåëüíûé ìåòîä ðàçðàáîòêè, â êîòîðîì èñïîëüçîâàíà àëãåáðàè-
÷åñêàÿ ìîäåëü ñïåöèôèêàöèé äèçàéíà, òðåáîâàíèé è áèíàðíîãî êîäà äëÿ
ïðèìåíåíèÿ ôîðìàëüíûõ ìåòîäîâ âåðèôèêàöèè, ìîäåëüíîãî òåñòèðîâàíèÿ è
ìåòîäîâ àëãåáðàè÷åñêîãî ñîïîñòàâëåíèÿ.  êà÷åñòâå ñïåöèôèêàöèé àëãåáðà-
è÷åñêîé ìîäåëè àïïàðàòíîãî îáåñïå÷åíèÿ ñëóæèò àëãåáðà ïîâåäåíèé, îïðå-
äåëåííàÿ íà ìíîæåñòâå äåéñòâèé è ïîâåäåíèé.
Êëþ÷åâûå ñëîâà: ïðîãðàììèðóåìûå ïîëüçîâàòåëåì âåíòèëüíûå ìàòðèöû, ñèì-
âîëüíîå ìîäåëèðîâàíèå, àëãåáðàè÷åñêîå ñîïîñòàâëåíèå, àëãåáðà ïîâåäåíèé.
O.O. Letychevskyi, V.S. Peschanenko, V.S. Kharchenko,
V.A. Volkov, O.M. Odarushchenko
MODEL-DRIVEN DEVELOPMENT OF DIGITAL SYSTEM ALGORITHMS
ON PROGRAMMABLE LOGIC INTEGRATED CIRCUITS
Abstract. The paper considers the current trends in the field of automated
hardware development, in particular, the development of digital systems using
programmable logic integrated circuits on the example of FPGA
(Field-Programmable Gate Array). A model-driven development method is
proposed that uses an algebraic model of design specifications, requirements,
and binary code to apply formal verification methods, model testing, and
algebraic matching methods. The specifications of an algebraic hardware model
is a behavior algebra defined over set of actions and behaviors.
Keywords: Field-Programmable Gate Array, symbolic modeling, algebraic
matching, behavior algebra.
Ëåòè÷åâñüêèé Îëåêñàíäð Îëåêñàíäðîâè÷,
äîêòîð ô³ç.-ìàò. íàóê, çàâ³äóâà÷ â³ää³ëó ²íñòèòóòó ê³áåðíåòèêè ³ì. Â.Ì. Ãëóøêîâà ÍÀÍ Óêðà¿íè,
Êè¿â, e-mail: oleksandr.letychevskyi@litsoft.com.ua.
Ïåñ÷àíåíêî Âîëîäèìèð Ñåðã³éîâè÷,
äîêòîð ô³ç.-ìàò. íàóê, ïðîôåñîð, çàâ³äóâà÷ êàôåäðè Õåðñîíñüêîãî äåðæàâíîãî óí³âåðñèòåòó,
e-mail: volodymyr.peschanenko@litsoft.com.ua.
Õàð÷åíêî Â’ÿ÷åñëàâ Ñåðã³éîâè÷,
äîêòîð òåõí. íàóê, ïðîôåñîð, çàâ³äóâà÷ êàôåäðè Íàö³îíàëüíîãî àåðîêîñì³÷íîãî óí³âåðñèòåòó
³ì. Ì.ª. Æóêîâñüêîãî «Õàðê³âñüêèé àâ³àö³éíèé ³íñòèòóò», e-mail: v.kharchenko@csn.khai.edu.
Âîëêîâ Âëàäèñëàâ Àíàòîë³éîâè÷,
êàíäèäàò ô³ç.-ìàò. íàóê, ñòàðøèé íàóêîâèé ñï³âðîá³òíèê ²íñòèòóòó ê³áåðíåòèêè ³ì. Â.Ì. Ãëóøêîâà
ÍÀÍ Óêðà¿íè, Êè¿â, e-mail: vlad_volkov_98@yahoo.com.
Îäàðóùåíêî Îëåã Ìèêîëàéîâè÷,
êàíäèäàò òåõí. íàóê, äîöåíò, ïðîâ³äíèé íàóêîâèé ñï³âðîá³òíèê Íàóêîâî-âèðîáíè÷îãî ï³äïðèºìñòâà
«Ðàä³êñ», Êðîïèâíèöüêèé, e-mail: odarushchenko@gmail.com.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 5 37
|
| id | nasplib_isofts_kiev_ua-123456789-190448 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1019-5262 |
| language | Ukrainian |
| last_indexed | 2025-12-01T18:40:52Z |
| publishDate | 2020 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Летичевський, О.О. Песчаненко, В.С. Харченко, В.С. Волков, В.А. Одарущенко, О.М. 2023-06-08T15:06:26Z 2023-06-08T15:06:26Z 2020 Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах / О.О. Летичевський, В.С. Песчаненко, В.С. Харченко, В.А. Волков, О.М. Одарущенко // Кибернетика и системный анализ. — 2020. — Т. 56, № 5. — С. 29–37. — Бібліогр.: 25 назв. — укр. 1019-5262 https://nasplib.isofts.kiev.ua/handle/123456789/190448 004.05, 004.42 Розглянуто сучасні тенденції в галузі автоматизованого розроблення апаратного забезпечення, зокрема, розроблення цифрових систем з використанням програмованих логічних інтегральних схем на прикладі програмованих користувачем вентильних матриць. Запропоновано модельний метод розроблення, в якому використано алгебраїчну модель специфікацій дизайну, вимог та бінарного коду для застосування формальних методів верифікації, модельного тестування та методів алгебраїчного зіставлення. Специфікаціями алгебраїчної моделі апаратного забезпечення слугує алгебра поведінок, визначена на множині дій та поведінок. Рассмотрены современные тенденции в области автоматизированной разработки аппаратного обеспечения, в частности разработки цифровых систем с использованием программируемых логических интегральных схем на примере вентильних матриц, программируемых пользователем. Предложен модельный метод разработки, в котором использована алгебраическая модель спецификаций дизайна, требований и бинарного кода для применения формальных методов верификации, модельного тестирования и методов алгебраического сопоставления. В качестве спецификаций алгебраической модели аппаратного обеспечения служит алгебра поведений, определенная на множестве действий и поведений. The paper considers the current trends in the field of automated hardware development, in particular, the development of digital systems using programmable logic integrated circuits on the example of FPGA (Field-Programmable Gate Array). A model-driven development method is proposed that uses an algebraic model of design specifications, requirements, and binary code to apply formal verification methods, model testing, and algebraic matching methods. The specifications of an algebraic hardware model is a behavior algebra defined over set of actions and behaviors. uk Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кібернетика Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах Модельный способ разработки алгоритмов цифровых систем на программируемых логических интегральных схемах Model-driven development of digital system algorithms on programmable logic integrated circuits Article published earlier |
| spellingShingle | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах Летичевський, О.О. Песчаненко, В.С. Харченко, В.С. Волков, В.А. Одарущенко, О.М. Кібернетика |
| title | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах |
| title_alt | Модельный способ разработки алгоритмов цифровых систем на программируемых логических интегральных схемах Model-driven development of digital system algorithms on programmable logic integrated circuits |
| title_full | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах |
| title_fullStr | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах |
| title_full_unstemmed | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах |
| title_short | Модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах |
| title_sort | модельний спосіб розроблення алгоритмів цифрових систем на програмованих логічних інтегральних схемах |
| topic | Кібернетика |
| topic_facet | Кібернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/190448 |
| work_keys_str_mv | AT letičevsʹkiioo modelʹniisposíbrozroblennâalgoritmívcifrovihsistemnaprogramovanihlogíčnihíntegralʹnihshemah AT pesčanenkovs modelʹniisposíbrozroblennâalgoritmívcifrovihsistemnaprogramovanihlogíčnihíntegralʹnihshemah AT harčenkovs modelʹniisposíbrozroblennâalgoritmívcifrovihsistemnaprogramovanihlogíčnihíntegralʹnihshemah AT volkovva modelʹniisposíbrozroblennâalgoritmívcifrovihsistemnaprogramovanihlogíčnihíntegralʹnihshemah AT odaruŝenkoom modelʹniisposíbrozroblennâalgoritmívcifrovihsistemnaprogramovanihlogíčnihíntegralʹnihshemah AT letičevsʹkiioo modelʹnyisposobrazrabotkialgoritmovcifrovyhsistemnaprogrammiruemyhlogičeskihintegralʹnyhshemah AT pesčanenkovs modelʹnyisposobrazrabotkialgoritmovcifrovyhsistemnaprogrammiruemyhlogičeskihintegralʹnyhshemah AT harčenkovs modelʹnyisposobrazrabotkialgoritmovcifrovyhsistemnaprogrammiruemyhlogičeskihintegralʹnyhshemah AT volkovva modelʹnyisposobrazrabotkialgoritmovcifrovyhsistemnaprogrammiruemyhlogičeskihintegralʹnyhshemah AT odaruŝenkoom modelʹnyisposobrazrabotkialgoritmovcifrovyhsistemnaprogrammiruemyhlogičeskihintegralʹnyhshemah AT letičevsʹkiioo modeldrivendevelopmentofdigitalsystemalgorithmsonprogrammablelogicintegratedcircuits AT pesčanenkovs modeldrivendevelopmentofdigitalsystemalgorithmsonprogrammablelogicintegratedcircuits AT harčenkovs modeldrivendevelopmentofdigitalsystemalgorithmsonprogrammablelogicintegratedcircuits AT volkovva modeldrivendevelopmentofdigitalsystemalgorithmsonprogrammablelogicintegratedcircuits AT odaruŝenkoom modeldrivendevelopmentofdigitalsystemalgorithmsonprogrammablelogicintegratedcircuits |