94
7 Designing Application-Specific Architectures
By this, all paths possible in the graph G are recursively defined and become
accessible due to the pth (u,v) -variables. Now, it only has to be ensured that no cyclic
paths occur, i.e. if there is a path between the nodes u ∈ ˆ
V and v ∈ ˆ
V , there must
not be an edge from the nodes v to node u. Hence, enforcing
u∈ ˆ
V \{MP U}
v∈ ˆ
V \{MP U}
pth (u,v) ⇒ e (v,u) = 0
prohibits the generation of graphs G with cycles.
Passing the resulting formulation to an SMT-solver now only yields assignments
representing architectures realizing the desired experiments and satisfying the
physical constraints. If the SMT-solver determines that no assignment is possible
satisfying all constraints, it has been proven that the desired experiments cannot
be realized given the number of possible instantiations for each module. Then, the
designer has to increase the respective values for maxI. If a satisfying assignment
is determined, the corresponding graph can easily be derived from the values of the
e (u,v) -variables (as illustrated in Fig. 7.2).
7.4.4 Employing the Quality Criteria
Usually, the formulation presented above yields a significant number of possible
assignments. This is because the considered experiments can usually be realized
by a large number of possible architectures (in particular, if the respective values
for maxI are large and, hence, a high degree of freedom exists). However, all
these architectures differ in their quality. Hence, designers might be interested in
a solution, which is optimized or even optimal with respect to one or more of the
quality criteria.
In order to employ that, an SMT-solver is utilized, which does not only allow
for determining a satisfying assignment, but an assignment which is additionally
optimized with respect to an objective function. 2 More precisely, in order to
determine a graph G optimized with respect to
• the number of connections, the number of edges in G is minimized by using the
e (u,v) -variables set to 1, i.e.
min :
(u,v)∈ ˆ
E
e (u,v) , or
2 Alternatively to objective functions, it is also possible to define constraints restricting the different
quality criteria.
7 Designing Application-Specific Architectures
By this, all paths possible in the graph G are recursively defined and become
accessible due to the pth (u,v) -variables. Now, it only has to be ensured that no cyclic
paths occur, i.e. if there is a path between the nodes u ∈ ˆ
V and v ∈ ˆ
V , there must
not be an edge from the nodes v to node u. Hence, enforcing
u∈ ˆ
V \{MP U}
v∈ ˆ
V \{MP U}
pth (u,v) ⇒ e (v,u) = 0
prohibits the generation of graphs G with cycles.
Passing the resulting formulation to an SMT-solver now only yields assignments
representing architectures realizing the desired experiments and satisfying the
physical constraints. If the SMT-solver determines that no assignment is possible
satisfying all constraints, it has been proven that the desired experiments cannot
be realized given the number of possible instantiations for each module. Then, the
designer has to increase the respective values for maxI. If a satisfying assignment
is determined, the corresponding graph can easily be derived from the values of the
e (u,v) -variables (as illustrated in Fig. 7.2).
7.4.4 Employing the Quality Criteria
Usually, the formulation presented above yields a significant number of possible
assignments. This is because the considered experiments can usually be realized
by a large number of possible architectures (in particular, if the respective values
for maxI are large and, hence, a high degree of freedom exists). However, all
these architectures differ in their quality. Hence, designers might be interested in
a solution, which is optimized or even optimal with respect to one or more of the
quality criteria.
In order to employ that, an SMT-solver is utilized, which does not only allow
for determining a satisfying assignment, but an assignment which is additionally
optimized with respect to an objective function. 2 More precisely, in order to
determine a graph G optimized with respect to
• the number of connections, the number of edges in G is minimized by using the
e (u,v) -variables set to 1, i.e.
min :
(u,v)∈ ˆ
E
e (u,v) , or
2 Alternatively to objective functions, it is also possible to define constraints restricting the different
quality criteria.