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 procedure returns (success,mvProg) with the SCAD program mvProg and a boolean flag success that holds iff the program was completed (since a buffer ordering exists for the node ordering). Otherwise, success is false and mvProg is the prefix of a program until a deadlock was reached.

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

Compute the set of buffers used by load/store token chains of a DPN

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

get the index of the output buffer of the SCAD PU of a DPN buffer for the standard SCAD PU with two input and two output buffers In addition to GetOutBufOfPU, this version takes care of a potential exchange of the outputs of a Dup node. It therefore does not only Return the index, but a list of pairs (optSwt,idx) where idx is the index if the optional guard optSwt holds. This guard is a pair (neg,dupIdx) where the boolean neg denotes that the outputs are not switched and dupIdx is the index of the dup node (to generate a variable).

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.

Solves a propositional logic formula phi by means of the BDD package. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values.

Solves a propositional logic formula phi by means of the SAT solver. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values.

Given the results of function MkConstraintsSAT, this function solves the computed constraints by Averest's SAT solver. It returns an optional 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.

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)