AUTOMATED GENERATION OF VERIFIED COMPETITIVE HARDWARE
Formal Methods. CSP. VHDL. Code Generation.
The complexity of development and analysis is inherent to systems in general, especially to concurrent systems. When we work with critical systems this becomes much more evident, as an inconsistency is usually associated with a high cost. Thus, the sooner we can identify an inconsistency in the design of a system and remove it, the lower its cost. For this reason, it is common to use the most varied strategies to reduce the difficulty and problems faced in this process. One of these strategies is the use of formal methods, which can use process algebra to specify and analyze competing systems, improving the understanding of the project and enabling the identification of possible inconsistencies even in the initial stages of the project, ensuring the accuracy and correction of the system. specified. This work presents a tool for automatic translation of the main operators of the Communicating Sequential Processes (csp) process algebra into the hardware description language vhsic hardware description language (vhdl). csp is a language that allows us to perform a formal description of a concurrent system. vhdl is a hardware description language that can be compiled on a Field Programmable Gate Arrays (FPGA) board. Our automatic hardware generation tool is validated by a case study of an intelligent elevator control system. We present its formal specification in csp and then its translation into a vhdl.