Reconfigurable processor fabric implementation using satisfiability analysis
Disclosed techniques utilize a satisfiability solver for allocation and/or configuration of resources in a reconfigurable fabric of processing elements. A dataflow graph is an input provided to a toolchain that includes a satisfiability solver. The satisfiability solver operates on subsets of interconnected nodes within a dataflow graph to derive a solution. The solution is trimmed by removing artifacts and unnecessary parts. The solutions of subsets are then used as an input to additional subsets of nodes within the dataflow graph in an iterative process to derive a complete solution. The satisfiability solver technique uses adaptive windowing in both the time dimension and the spatial dimensions of the dataflow graph. Processing elements and routing elements within the reconfigurable fabric are configured based on the complete solution. Data computation is performed based on the dataflow graph using the processing elements and the routing resources.
1. A computer-implemented method for resource allocation comprising:
configuring a first plurality of processing elements from a reconfigurable fabric for computational calculations, based on a dataflow graph, wherein the configuring is performed using a satisfiability solver technique comprising constructing a set of mapping constraints and building a satisfiability model of the mapping constraints, and wherein the satisfiability solver technique includes adaptive windowing;
configuring routing resources within the reconfigurable fabric based on the satisfiability solver technique; and
performing data computation based on the dataflow graph using the first plurality of processing elements and the routing resources.
2. The method of claim 1 wherein the satisfiability solver technique includes scaling with iterative packing.
3. The method of claim 2 wherein the scaling includes partitioning execution time into overlapping time windows.
4. The method of claim 2 wherein the satisfiability solver technique includes bounding time in an adaptive window to solve an optimization sub-problem.
5. The method of claim 1 wherein the satisfiability solver technique comprises a Boolean satisfiability problem solving technique.
6. The method of claim 5 further comprising solving the satisfiability model.
7. The method of claim 6 further comprising storing a solution of the satisfiability model.
8. The method of claim 7 further comprising trimming the solution, wherein the trimming includes removing unnecessary parts from the solution.
9. The method of claim 1 wherein the satisfiability solver technique further comprises grouping instructions from the dataflow graph.
10. The method of claim 9 wherein the satisfiability solver technique includes solving the instructions which were grouped.
11. The method of claim 10 wherein the solving the instructions which were grouped comprises solving a sub-problem.
12. The method of claim 11 wherein the solving the instructions is across a set of sub-tics within the reconfigurable fabric.
13. The method of claim 1 further comprising scheduling the first plurality of processing elements based on the dataflow graph and the satisfiability solver technique.
14. The method of claim 1 wherein the mapping constraints comprise instructions for implementing a function on a processing element from the first plurality of processing elements.
15. The method of claim 14 wherein the instructions for implementing a function on the processing element are loaded into a circular buffer associated with the processing element that controls the processing element.
16. The method of claim 1 wherein the mapping constraints prevent data collisions within the reconfigurable fabric.
17. The method of claim 1 wherein the mapping constraints comprise a three-dimensional (3D) solution space comprising an x and y physical location of processing elements along with a z dimension time.
18. The method of claim 1 wherein the satisfiability solver technique comprises learning across variables and clauses.
19. The method of claim 1 wherein the satisfiability model includes variables, clauses, and conjunction of clauses.
20. The method of claim 1 wherein the configuring routing resources is based on propagations indicated by routing instructions.
21. The method of claim 1 further comprising partitioning the dataflow graph into time partitions and solving the satisfiability model for a time partition.
22. The method of claim 21 further comprising moving the time partition forward in time and backward in time to optimize the solving the satisfiability model across the backward in time partition, the time partition, and the forward in time partition.
23. The method of claim 21 further comprising applying a template, wherein the template describes local constraints for a node in the time partition of the dataflow graph.
24. The method of claim 1 wherein input data to the dataflow graph is obtained directly from a processing element within the plurality of processing elements.
25. The method of claim 1 wherein input data to the dataflow graph is obtained from outside the reconfigurable fabric.
26. The method of claim 1 wherein output data from the dataflow graph is propagated directly to a processing element within the plurality of processing elements.
27. The method of claim 1 wherein output data from the dataflow graph is propagated outside the reconfigurable fabric.
28. A computer program product embodied in a non-transitory computer readable medium for resource allocation, the computer program product comprising code which causes one or more processors to perform operations of:
configuring a first plurality of processing elements from a reconfigurable fabric for computational calculations, based on a dataflow graph, wherein the configuring is performed using a satisfiability solver technique comprising constructing a set of mapping constraints and building a satisfiability model of the mapping constraints, and wherein the satisfiability solver technique includes adaptive windowing;
configuring routing resources within the reconfigurable fabric based on the satisfiability solver technique; and
performing data computation based on the dataflow graph using the first plurality of processing elements and the routing resources.
29. A computer system for resource allocation comprising:
a memory which stores instructions;
one or more processors attached to the memory wherein the one or more processors, when executing the instructions which are stored, are configured to:
configure a first plurality of processing elements from a reconfigurable fabric for computational calculations, based on a dataflow graph, wherein the configuring is performed using a satisfiability solver technique comprising constructing a set of mapping constraints and building a satisfiability model of the mapping constraints, and wherein the satisfiability solver technique includes adaptive windowing;
configure routing resources within the reconfigurable fabric based on the satisfiability solver technique; and
perform data computation based on the dataflow graph using the first plurality of processing elements and the routing resources.