UDC 004.05, 004.4[2+9], 004.94, 519.7
INSERTION SEMANTICS OF VHDL AS ELECTRONIC DESIGN LANGUGE
Abstract. The paper considers the problem of insertion semantics of hardware specifications, in particular the VHDL language. The creation of semantics is necessary to represent the primary code of the VHDL language in the form of an insertion model using algebra of behaviors. This presentation allows the widespread use of formal methods of insertion modeling to verify electronic designs of safety critical systems. The main constructions of VHDL language and their insertion semantics such as process, architecture, parallel operators are considered. The control flow of the VHDL program is built in the form of behavioral equations. Consecutive operators are represented as actions of behavior algebra. The problem of signal races and methods of its detection through detection of permutability properties is considered.
Keywords: Hardware Description Language, signal races, permutability, symbolic modeling, behavior algebra, insertion model, safety critical system.
FULL TEXT
REFERENCES
- 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.
