Compute a PU allocation by modulo operation on node indices; the function returns a pair (numPU,allocMap) where numPU is the number of PUs used and allocMap is a map to assign each DPN node a PU

Compute a random PU allocation for numPU processing units; the function returns a pair (numPU,allocMap) where numPU is the number of PUs used and allocMap is a map to assign each DPN node a PU

Compute a PU allocation by a minimal vertex disjoint node cover; the function returns a pair (numPU,allocMap) where numPU is the number of PUs used and allocMap is a map to assign each DPN node a PU

 SCAD code generation with a given node ordering and PU assignment: The
 function performs a symbolic simulation to determine a buffer ordering
 for the given node order and returns (success,mvProg) with a move code
 program mvProg. The value success is false if no buffer ordering has
 been found or if the buffer size was not sufficient, and in this case,
 mvProg is the prefix of a program until a deadlock was reached.
 You may have to increase the buffer size (variable bufSize in module
 MoveCode) to make the code generator work in the latter case. Parameter
 beQuiet is used to suppress the printing of the processor state during
 code generation. Usually, inputs are read from LSU.out and outputs are
 written to LSU.val; using constMode=true, input values are provided
 instead via the parameter varMap as constants.
  Since DPN buffers are associated with move instructions, the code 
 generator assumes that input and output buffers have different names. If
 that is not the case, then either the input or output buffers must be
 renamed.

This function starts with the given buffer size and calls CodeGenSCAD; if it fails with buffer-size-too-small exception, the buffer size is increased until either the code is generated successfully or fails for another reason.

buffer mapping: map a buffer bf of the DPN dpn to the input buffer of a PU in a BED processor architecture with two input and two output buffers

Given a model of the constraints generated by MkConstraintsSAT, this extracts the node/buffer orders, the PU allocation, and the set of Dup nodes that were switched by the model. It also requires the set of variables, and the sets of nodes and buffers (possibly split into levels). The function returns a tuple (nodOrder,bufOrder,nodeAsg,switchDupNodes) where nodOrder contains the sorted list of nodes per level, bufOrder contains the sorted list of buffers per level, nodeAsg is the PU assignment that maps nodes to PUs, and switchDupNodes is the set of Dup nodes that have to be switched.

buffer mapping: map a buffer bf of the DPN dpn to the output buffer of a PU in a BED processor architecture with two input and two output buffers

This function generates constraints for code generation from dataflow graphs that may or may not be leveled for a SCAD machine with 2x2 PUs. If the given dpn is leveled, optLevelInfo should be a triple of the form (nodLevel,bufLevel,maxNodLevel) where nodLevel maps the DPN nodes to a level number, bufLevel maps the buffers of the DPN to a level number, and maxNodLevel is the number of levels. The parameter puNum is the number of 2x2 PUs of the SCAD machine. The result (nodLevels,bufLevels,variables,constraints) consists of arrays nodLevels and bufLevels where nodLevels[i] and bufLevels[i] are the set of nodes and buffers of level i, respectively; variables is the set of variables, and constraints is the set of generated constraints. The constraints use the following variables: nodOrd{i,j} holds if node i fires before node j in the schedule, bufOrd{bf1,bf2} holds if the move instruction corresponding to bf1 is done before that one of bf2, asgVar{i,p} holds, if node i is mapped to PU p, and swD{i} holds iff Dup node i shall switch its outputs.

This function generates constraints for code generation from dataflow graphs that may or may not be leveled for a SCAD machine with 2x2 PUs. If the given dpn is leveled, optLevelInfo should be a triple of the form (nodLevel,bufLevel,maxNodLevel) where nodLevel maps the DPN nodes to a level number, bufLevel maps the buffers of the DPN to a level number, and maxNodLevel is the number of levels. The parameter puNum is the number of 2x2 PUs of the SCAD machine. The result (nodLevels,bufLevels,variablesBool,variablesNat,constraints) consists of arrays nodLevels and bufLevels where nodLevels[i] and bufLevels[i] are the set of nodes and buffers of level i, respectively; variablesBool and variablesNat are the variables of types bool and nat, respectively, and constraints is the set of generated constraints. The constraints use the following variables: nodAt{i} is the point of time when node i fires in the schedule, bufAt{bf} is the point of time when the move instruction of buffer bf is done, nod2PU{i} is the PU assigned to node i, and swD{i} holds iff the Dup node i shall switch its outputs.

MkTwoSatConstraintsWithAlloc generates with a given PU allocation alpha (where alpha[i] is the PU of dpn.nodes[i]) a 2SAT problem, i.e., a set of constraints of type TwoSAT. The constraints do neither take care of transitivity nor of switching the output of DUP nodes.

SolveConstraintsSAT generates the SAT constraints by MkConstraintsSAT, solves them by either Averest's internal SAT solver of Microsoft's Z3 (depending on useZ3), and extracts the orders and PU allocation with GetOrderAndAllocation.

SolveConstraintsSATminPU applies SolveConstraintsSAT for numPU=1,2,... until it finally succeeds.

clusters which are closed under transitivity and which merged in case that these are overlapping, i.e., in case their node/buffer ordering constraints do overlap. Each cluster consists of a pair (nodOrd,bufOrd) which are the node and buffer ordering constraints that are equivalent to each other. The first cluster equCluster[0] has a speical role since its entries are the facts that must hold for the node and buffer ordering. After partitioning the equivalences into non-overlapping classes, the function randomly picks an equivalence cluster (other than the first one) and merges it with the first one. This process is carried out repeatedly until a model is found (i.e., no further equivalence cluster exists that could be merged) or if the first cluster got a cycle. In the latter case, backtracking is applied in that the latest decision, i.e., the latest cluster merged is taken back and it is reversed and then merged again.

verify that a computed solution (nodOrd,bufOrd) indeed satisfies given 2SAT constraints (nodOrdInit,bufOrdInit,equClusterInit); it is expected that the given orders have enough transitive constraints, so that the function does not compute the transitive hull in advance

Generate move code from a DPN that is based on a vertex-disjoint path cover. The function first levelizes the DPN, then computes a minimal vertex-disjoint path cover using MinimumNumberOfVertexDisjointPathsDPN. It then derives the assignment to processing units from the vertex-disjoint path cover and orders the obtained threads randomly (by converting the set to a list). Note that by the levelization, the thread ordering also determines a node ordering in that nodes are primarily ordered by their levels, and nodes of the same level are ordered by their thread number. Using this node ordering, and PU assignment, function CodeGenSCAD is used to generate the move code with a certificate (a symbolic execution). The result is a tuple (puNum,nodeOrd,nodeAsg,dpnLeveled,edges,threadL,mvProg) where puNum is the number of PUs used, nodeOrd is the node ordering, nodeAsg is the PU assignment, dpnLeveled is the leveled DPN, edges is the set of edges used by the vertex-disjoint path cover, and threadL is the set of vertex-disjoint paths (ordered randomly). Finally, mvProg is the generated move code program.

write the preliminary node/buffer orders and remaining equivalences to a graph in graphviz format (additional edges on nodes or buffers which may close a cycle are drawn in red)