This section contains future work that should be added to Vericert to make it into a better high-level synthesis tool.
The next interesting optimisations that should be looked at are the following:
Globals are an important feature to add, as have to be handled carefully in HLS, because they have to be placed into memory, and are often used in HLS designs. Proper handling of globals would allow for a larger subset of programs to be compiled, even allowing for larger benchmarks to be used, such as CHStone.
Vericert is a formally verified high-level synthesis (HLS) tool written in Coq, which translates C code into Verilog hardware designs. One challenge in HLS is supporting different memory architectures and interacting with memory in an optimal way.
Vericert currently lacks support for multiple memories, and instead only constructs one large memory which contains all elements of the stack. Due to this limitation, Vericert mainly inlines all function calls and does not support global variables. This project would be about adding support for multiple memories to Vericert and proving the correctness of the improved translation. This would then allow globals to be compiled, which greatly increases the kinds of programs that can be translated.
This project would be ideal for students interested in hardware and theorem proving in Coq.
Type Support #
It would also be useful to have support for other datatypes in C, such as
short, as using
these small datatypes is also quite popular in HLS to make the final designs more efficient.
Vericert is a formally verified high-level synthesis (HLS) tool written in Coq, which translates C code into Verilog hardware designs. However, it currently only supports 32-bit integer types, which limits the effectiveness of HLS, as smaller types cannot be supported and are therefore not represented properly.
This project would address this problem by adding support for multiple different types in Vericert, and prove the new translation correct in Coq. Furthermore, the current memory in Vericert also only supports 32-bits, so this project could also address that by generalising the memory module and supporting smaller memory types.
Register Allocation #
Register allocation is an optimisation which minimises the register resource usage of the design, while still keeping the same throughput in most cases. Compared to standard software compilers, HLS tools do not normally require a lot of register allocation, however, this can still help in a lot of cases when registers are used unnecessarily.
Vericert is a formally verified high-level synthesis (HLS) tool written in Coq, which translates C code into Verilog hardware designs.
Memory Partitioning #
Memory partitioning is quite an advanced optimisation, which could be combined with the support for globals so as to make memory layouts on the FPGA more efficient and run various memory operations in parallel.
Loop pipelining #
Loop pipelining is an optimisation to schedule loops, instead of only scheduling the instructions inside of the loop. There are two versions of loop pipelining, software and hardware loop pipelining. The former is done purely on instructions, whereas the latter is performed in tandem with scheduling.