УДК 004.05, 004.42
МОДЕЛЬНЫЙ СПОСОБ РАЗРАБОТКИ АЛГОРИТМОВ ЦИФРОВЫХ СИСТЕМ
НА ПРОГРАММИРУЕМЫХ ЛОГИЧЕСКИХ ИНТЕГРАЛЬНЫХ СХЕМАХ
Аннотация. Рассмотрены современные тенденции в области автоматизированной разработки аппаратного обеспечения, в частности разработки цифровых систем с использованием программируемых логических интегральных схем на примере вентильних матриц, программируемых пользователем. Предложен модельный метод разработки, в котором использована алгебраическая модель спецификаций дизайна, требований и бинарного кода для применения формальных методов верификации, модельного тестирования и методов алгебраического сопоставления. В качестве спецификаций алгебраической модели аппаратного обеспечения служит алгебра поведений, определенная на множестве действий и поведений.
Ключевые слова: программируемые пользователем вентильные матрицы, символьное моделирование, алгебраическое сопоставление, алгебра поведений.
ПОЛНЫЙ ТЕКСТ
Летичевський Олександр Олександрович,
доктор фіз.-мат. наук, завідувач відділу Інституту кібернетики ім. В.М. Глушкова НАН України, Київ,
oleksandr.letychevskyi@litsoft.com.ua
Песчаненко Володимир Сергійович,
доктор фіз.-мат. наук, професор, завідувач кафедри Херсонського державного університету,
volodymyr.peschanenko@litsoft.com.ua
Харченко В’ячеслав Сергійович,
доктор техн. наук, професор, завідувач кафедри Національного аерокосмічного університету
ім. М.Є. Жуковського «Харківський авіаційний інститут», v.kharchenko@csn.khai.edu
Волков Владислав Анатолійович,
кандидат фіз.-мат. наук, старший науковий співробітник Інституту кібернетики ім. В.М. Глушкова НАН України, Київ, vlad_volkov_98@yahoo.com
Одарущенко Олег Миколайович,
кандидат техн. наук, доцент, провідний науковий співробітник Науково-виробничого підприємства «Радікс», Кропивницький, odarushchenko@gmail.com
СПИСОК ЛИТЕРАТУРЫ
- FPGA. URL: www.intel.com/content/www/us/en/products/programmable/fpga/new-to-fpgas/resource -center/overview.html.
- V-model. URL: https://www.testingexcellence.com/v-model-in-software-testing/.
- VHDL. URL: www.intel.com/content/www/us/en/programmable/support/support-resources/design-examples/ design-software/vhdl.html.
- SystemVerilog. URL: www.asic-world.com/systemverilog/tutorial.html.
- Cadence. URL: www.cadence.com/.
- Xilinx. URL: www.xilinx.com.
- Synopsis. URL: www.synopsys.com.
- Potium. URL: www.cadence.com/en_US/home/tools/system-design-and-verification/fpga-basedpro totyping/protium-s1-fpga-based-prototyping-platform.html.
- Quartus. URL: www.intel.com/content/www/us/en/programmable/downloads/download-center.html
- BPMN. URL: www.bpmn.org/.
- ITU-T Recommendation, Z.151, User Requirements Notation (URN) — Language definition.
- UML. URL: www.uml.org/.
- 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. 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.
- Z3 decision procedure. URL: https://github.com/Z3Prover/z3.
- CVC4 decision procedure. URL: http://cvc4.cs.stanford.edu.
- 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.
- 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.
- 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.
- 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 September 2011, Sevastopol, Ukraine). Sevastopol, 2011. P. 1–6.
- 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.
- 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.
- 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.
- 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.
- 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.
