Automatic Generation of Verified Concurrent Hardware Using VHDL

The complexity of development and analysis is inherent to systems in general, especially in concurrent systems. When working with critical systems this becomes much more evident, as inconsistencies are 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 strategies to reduce the difficulty and problems faced in this process. One of these strategies is the use of formal methods, which can, for instance, make use of process algebras to specify and analise concurrent systems, improving its understanding and enabling the identification of eventual concurrency problems and inconsistencies even in the initial stages of the project, ensuring the accuracy and correction of the system specification. This article presents a strategy for automatically translating the main operators of the process algebra CSP (Communicating Sequential Processes) into the VHSIC hardware description language (VHDL). The former is a language that allows us to make a formal description of a concurrent system and the latter is a hardware description language that can be compiled on a Field Programmable Gate Arrays (FPGA) board. Our automatic translator is validated by a case study of a smart elevator control system. We present its formal specification in CSP and then its translation into VHDL code, generated by our tool, which we synthesised on an FPGA board.