Hard-Wiring CSP Hiding: Implementing Channel Abstraction to Generate Verified Concurrent Hardware

Throughout the development of concurrent systems, complexity may easily grow exponentially yielding a very complex and error-prone process. By using formal languages like CSP we may simplify this task increasing the level of confidence on the resulting system. Unfortunately, such languages are not executable: the gap between the specification language and an executable program must be solved. In previous work, we presented a tool, csp2hc, that translates a considerable subset of CSP into Handel-C source code, which can itself be converted to produce files to program FPGAs. This subset restricts the use of data structures and CSP hiding. In this paper, we present an extension to csp2hc that includes sequences in the set of acceptable data structures and completely deals with the CSP hiding operator. Finally, we validate our extension by applying the translation approach to a industrial scale case study, the steam boiler.