Finding heap-bounds for hardware synthesis

Abstract—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 firstknown 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.

• Type: Conference
• Year: 2009
• Where: FMCAD
• Authors: Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis
• Keywords: C-to-gates Hardware Synthesis, FMCAD 2009, Formal Methods, Memory Usage Bounds, Upper Bound