Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiří Šimša, Satnam Singh, and Viktor Vafeiadis
15 November 2009
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.
In Formal Methods in Computer Aided Design (FMCAD)