УДК 004.05, 004.4[2+9], 004.94, 519.7
О.О. ЛЕТИЧЕВСЬКИЙ,
Інститут кібернетики ім. В.М. Глушкова НАН України, Київ, Україна,
oleksandr.letychevskyi@litsoft.com.ua
О.М. ОДАРУЩЕНКО,
Науково-виробниче підприємство «Радікс», Кропивницький, Україна,
odarushchenko@gmail.com
В.С. ПЕСЧАНЕНКО,
Херсонський державний університет, Херсон, Україна,
volodymyr.peschanenko@litsoft.com.ua
В.С. ХАРЧЕНКО,
Національний аерокосмічний університет ім. М.Є. Жуковського «Харківський авіаційний інститут», Харків, Україна,
v.kharchenko@csn.khai.edu
В.В. МОСКАЛЕЦЬ,
Науково-виробниче підприємство «Радікс», Кропивницький, Україна,
viktoriia.moskalets@gmail.com
ІНСЕРЦІЙНА СЕМАНТИКА VHDL-МОВИ ЕЛЕКТРОННОГО ДИЗАЙНУ
Анотація. Досліджено проблему інсерційної семантики специфікацій апаратного забезпечення, зокрема мови VHDL. Побудова семантики потрібна для представлення первинного коду мови VHDL у вигляді інсерційної моделі за допомогою алгебри поведінок. Це представлення дає змогу широко застосовувати формальні методи інсерційного моделювання для верифікації електронних проєктів критичних систем. У статті розглянуто основні конструкції мови VHDL, зокрема процес, архітектуру, паралельні оператори, та їхню інсерційну семантику. У вигляді поведінкових рівнянь побудовано потік керування VHDL-програми. Послідовні оператори представлено як дії алгебри поведінок. Розглянуто проблему перегонів сигналів та методів її виявлення через визначення властивості переставності (permutability).
Ключові слова: мови дизайну апаратного забезпечення, перегони сигналів, переставність, символьне моделювання, алгебра поведінок, інсерційні моделі, системи, що є критичними до безпеки.
ПОВНИЙ ТЕКСТ
СПИСОК ЛІТЕРАТУРИ
- Kharchenko V., Letychevskyi O., Odarushchenko O., Peschanenko V., Volkov V. Modeling method for development of digital system algorithms based on programmable logic devices. Cybernetics and Systems Analysis. Vol. 56, N 5. P. 710–717 (2020). https://doi.org/10.1007/s10559-020-00289-8.
- Booch G., Rumbaugh J., Jacobson I. Unified Modeling Language User Guide. Boston: Addison-Wesley, 2005, 512 p.
- Coelho D. The VHDL Handbook. New York: Springer Science & Business Media, 1989. 406 p.
- System Verilog Tutorial. URL: www.asic-world.com/systemverilog/tutorial.html.
- VC Formal. URL: https://www.synopsys.com/verification/static-and-formal-verification/ vc-formal.html.
- Vivado Verification. URL: https://www.xilinx.com/products/design-tools/vivado/verification.html.
- Jasper RTL Apps. (JasperGold platform). URL: https://www.cadence.com/ko_KR/home/tools/ system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform.html.
- Letichevsky A., Letychevskyi O., Peschanenko V. Insertion modeling and its applications. Computer Science Journal of Moldova. 2016. Vol. 24, Iss. 3. P. 357–370.
- Letichevsky A., Gilbert D. 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.
- 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.
- ITU-T Recommendation, Z.120, Message Sequence Charts (MSC). URL: https://www.itu.int/ rec/T-REC-Z.120.
- Ehlers T., Nowotka D., Sieweck P. Finding race conditions in real-time code byusing formal software verification. 2014. URL: https://www.researchgate.net/publication/288563365_ Finding_ race_conditions_in_real-time_code_by_using_formal_software_verification.
- Didier J.-Y., Mallem M. A new approach to detect potential race conditions in component-based systems. 2014. URL: https://hal.archives-ouvertes.fr/hal-01024478.
- Beckman N.E. A survey of methods for preventing race conditions. 2006. URL: http://www. docdatabase.net/more-a-survey-of-methods-for-preventing-race-conditions-212068.html.
- Letichevsky A., Letychevskyi O., Peschanenko V. An interleaving reduction for reachability checking in symbolic modeling. Proc. 11th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer (ICTERI 2015) (14–16 May 2015, Lviv, Ukraine). Lviv, 2015. P. 338–353. URL: ceur-ws.org/Vol-1356/paper_74.pdf.
- Letychevskyi O., Peschanenko V., Volkov V. Algebraic virtual machine project. Proc. 17th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer (ICTERI 2021) (28 Sep. – 02 Oct. 2021, Kherson, Ukraine). Kherson, 2021. URL: icteri.org/icteri-2021/proceedings/volume-2.
- Kharchenko V. Independent Verification and Diversity: Two echelons of cyber physical systems safety and security assurance. Proc. 2nd Int. Workshop on Information-Communication Technologies & Embedded Systems (ICTES 2020) (12 November 2020, Mykolaiv, Ukraine). Mykolaiv, 2020. P. 19–29. URL: ceur-ws.org/Vol-2762/invited2.pdf.
