Асерційна верифікація моделей пристроїв реального часу з недетермінованими зовнішніми подіями

Автор(и)

  • Марина Анатоліївна Мірошник Харківський національний університет імені В. Н. Каразіна, Україна https://orcid.org/0000-0002-2231-2529
  • Юрій Васильович Пахомов Харківський національний університет міського господарства імені О. М. Бекетова, Україна https://orcid.org/0000-0002-2267-8600
  • Кирило Юрійович Пшеничний Харківський національний університет радіоелектроніки, Україна https://orcid.org/0009-0007-0799-6604
  • Андрій Вікторович Шафранський Харківський національний університет імені В. Н. Каразіна, Україна https://orcid.org/0009-0004-7725-3556

DOI:

https://doi.org/10.18664/ikszt.v29i1.300988

Ключові слова:

автоматизація проєктування, моделювання, верифікація, системи реального часу, події, темпоральний граф переходів

Анотація

Запропоновано метод верифікації моделей пристроїв реального часу з обробкою зовнішніх подій із недермінованою тривалістю, що описані з використанням мов опису  апаратури (Hardware Description Language, HDL). У методології використано апарат асерцій для опису темпоральної природи вищезазначених моделей.

Біографії авторів

Марина Анатоліївна Мірошник, Харківський національний університет імені В. Н. Каразіна

д.т.н., професор, професор кафедри теоретичної та прикладної системотехніки

Юрій Васильович Пахомов , Харківський національний університет міського господарства імені О. М. Бекетова

к.т.н., доцент кафедри комп’ютерних наук та інформаційних технологій

Кирило Юрійович Пшеничний, Харківський національний університет радіоелектроніки

аспірант кафедри автоматизації проектування обчислювальної техніки

Андрій Вікторович Шафранський , Харківський національний університет імені В. Н. Каразіна

аспірант кафедри теоретичної та прикладної системотехніки

Посилання

Список використаних джерел

Bergeron Janick. Writing testbenches: functional verification of HDL models. Boston: Kluwer Academic Publishers. 2001. 354 c.

Design timed FSM with VHDL Moore pattern / M. A. Mіrosсhnyk, A. S. Shkil, E. N. Kulak, D. Y. Rakhlis, A. M. Mіroshnyk, N. V. Malahov. Radio 3. Electronics, Computer Science, Control. 2020. № 2(53). P. 137-148.

Іabah Al-Fedaghi. Modeling Physical. Digital Systems: Formal Event-B vs. Diagrammatic Thinging Machine. International Journal of Computer Science and Network Security. 2020. No. 20 (4). Р. 208–220. hal-02614504, version 1 (20-05-2020).

Miroshnyk A. M., Kulak G., Pshenychnyi K. Y. Assertion Based Design of Timed Finite State Machine. 2021 IEEE East-West Design & Test Symposium (EWDTS). Batumi, Georgia. 2021. Р. 1-4.

Temporal events processing models in finite state machines / M. A. Miroshnyk, S. I. Shmatkov, O. S. Shkil, K. Y. Pshenychnyi (2023). Radio Electronics, Computer Science, Control. (4), 49.

Проєктування та самодіагностика кіберфізичних пристроїв керування на платформі SoC / О. С. Шкіль, Д. Ю. Рахліс, І. В. Філіпенко, В. Р. Корнієнко. Сучасний стан наукових досліджень та технологій в промисловості. 2023. No 4 (26). С. 122–134.

Components of a complete assertions-based verification solution. Cadence. 2005. URL: www.cadence.com/products/functional_ver/abv_dt.aspx.

IEEE Std 1076-2002, IEEE Standard VHDL Language Reference Manual. 124 p.

IEEE Std 1364-2001, IEEE Standard for Verilog Hardware Description Language. Electrical and Electronics Engineers, Inc.USA. 2003. P. 1-23.

Хаханов В. І., Каминська М. А., Зайченко С. О. Верифікація цифрових пристроїв на основі використання аналіза тестопридатності та асерційних бібліотек (російською мовою). АСУ та прилади автоматики. Харків, 2007. № 140. С. 75–83.

##submission.downloads##

Опубліковано

2024-03-01

Номер

Том 29 № 1 (2024): Інформаційно-керуючі системи на залізничному транспорті

Розділ

Статті

Ліцензія

Creative Commons License

Ця робота ліцензується відповідно до Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.