Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Finding heap-bounds for hardware synthesis

Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiří Šimša, Satnam Singh, and Viktor Vafeiadis


Dynamically allocated and manipulated data structures cannot be translated into hardware unless there is an upper bound on the amount of memory the program uses during all executions. This bound can depend on the generic parameters to the program, i.e., program inputs that are instantiated at synthesis time. We propose a constraint based method for the discovery of memory usage bounds, which leads to the first known C-to-gates hardware synthesis supporting programs with non-trivial use of dynamically allocated memory, e.g., linked lists maintained with malloc and free. We illustrate the practicality of our tool on a range of examples.


Publication typeInproceedings
Published inFormal Methods in Computer Aided Design (FMCAD)
> Publications > Finding heap-bounds for hardware synthesis