Automated generation of RTL designs based on formal descriptions using Chisel HDL

LUBIS EDA GmbH has the goal of creating software that aids engineers developing digital computing hardware, mainly in the field of formal verification. A software tool developed by the company produces formal properties from abstract system descriptions written in SystemC. In addition, it offers the Operation Level Synthesis (OLS), a feature which enables the generation of RTL designs based on the same system descriptions, which automatically fulfill those properties. The current state of the OLS directly outputs the resulting RTL design written in SystemVerilog without invoking any additional optimization tools. This thesis explores the possibility of supporting the hardware description language Chisel, which utilizes advantages of the programming language Scala, combining its object-oriented and functional programming features to enhance the RTL design process. On top of that, Chisel also offers a possibility to convert its design to SystemVerilog for synthesis and simulation with additional optimizations. In the first part of this thesis a subset of small test designs, used by the company in their integration testing, was manually converted to Chisel as a proof-of-concept, which confirmed that the generated properties also hold for the RTL designs created from Chisel. During the second step real-world examples have also been re-written in Chisel, the corresponding properties were checked on the resulting RTL designs, which were synthesized on an FGPA board. The synthesis results were compared against the ones of the original OLS tool and their handwritten RTL implementations. The experiments showed potential improvement in resource consumption when using Chisel, so an output plugin for the automated generation of such designs has been developed for DeSCAM in the third part of this project. After developing and testing the software, the designs generated with the automation have also been synthesized and it was proven, that the resource effectiveness seen in the previous step has been maintained. This proved not only that the plugin now can accelerate the development of projects in Chisel but can also be used as an intermediate representation for the optimization of SystemVerilog models.