Static memory allocation using sat solver

Abstract

A method of statically allocating memory for a computer program includes splitting a computational graph associated with a plurality of static memory allocation constraints into a plurality of subgraphs; determining a memory allocation for each combination of subgraphs of the plurality of subgraphs using an SAT solver and a plurality of Boolean conditions that formalize the plurality of static memory allocation constraints; subdividing a subgraph of the plurality of subgraphs into a plurality of tiles, when the memory allocation for that subgraph cannot satisfy a hardware memory size constraint of the plurality of static memory allocation constraints; performing a performance analysis on all possible subgraphs and plurality of tiles; selecting a combination of subgraphs whose plurality of tiles has a best overall performance; and determining a memory allocation for the plurality of tiles for the selected combination of subgraphs using the SAT solver.