92
7 Designing Application-Specific Architectures
Table 7.1 Variables representing realizations of experiment φ 1
φ 1 :=
( f,
m,
d, )
φ 1 [1] = f
φ 1 [2] = m
φ 1 [3] = d
Variables
ex φ 1 [1] 1
ex φ 1 [2] 1
ex φ 1 [3] 1
ex φ 1 [1] 2
ex φ 1 [2] 2
ex φ 1 [3] 2
Assignments
ex φ 1 [1] 1 = 1
ex φ 1 [2] 1 = 0
ex φ 1 [3] 1 = 0
ex φ 1 [1] 2 = 0
ex φ 1 [2] 2 = 1
ex φ 1 [3] 2 = 1
Since the SMT-solver may arbitrarily assign the newly introduced ex φ[p] i -
variables, a constraint has to be added which enforces that each operation in an
experiment is realized by exactly one module. To this end, for each experiment
φ ∈ and each operation φ[p] of φ, all possible instances (represented by ex φ[p] i
with 1 ≤ i ≤ maxI(φ[p])) are considered. Then, it is enforced that only one of them
indeed is realizing the operation, i.e. only one of the corresponding ex φ[p] i -variables
is set to 1. This is accomplished by the constraint
φ∈
|φ|
p=1
⎛
⎝
maxI(φ[p])
i=1
ex φ[p] i
⎞
⎠ = 1.
Next, it has to be ensured that the, respectively, chosen chain of instances
realizing the experiment φ (represented by ex φ[p] i -variables) is indeed also realized
in the graph G. To this end, the e (u,v) -variables have to be restricted depending on
the respective values of the ex φ[p] i -variables. This is enforced by the constraint
φ∈
|φ|−1
p=1
maxI(φ[p])
i=1
maxI(φ[p+1])
j =1
ex φ[p] i ∧ ex φ[p+1] j ⇒ e (φ[p] i ,φ[p+1] j ) ,
which checks for each experiment φ ∈ and each consecutive pair of operations φ[p] and φ[p + 1] whether the instances φ[p] i and φ[p + 1] j are used to
realize them, respectively, (i.e., whether the variables ex φ[p] i and ex φ[p+1] j are set
to 1). If this is true, then it is enforced that G contains a connection between these
modules (i.e., that e (φ[p] i ,φ[p+1] j ) is set to 1). Finally, the edges connecting the MPU
with the first module as well as the last module with the MPU have to be enforced by
φ∈
maxI(φ[1])
i=1
ex φ[1] i ⇒ e (MP U,φ[1] i ) and
φ∈
maxI(φ[|φ|])
i=1
ex φ[|φ|] i ⇒ e (φ[|φ|] i ,MP U ) ,
respectively.
7 Designing Application-Specific Architectures
Table 7.1 Variables representing realizations of experiment φ 1
φ 1 :=
( f,
m,
d, )
φ 1 [1] = f
φ 1 [2] = m
φ 1 [3] = d
Variables
ex φ 1 [1] 1
ex φ 1 [2] 1
ex φ 1 [3] 1
ex φ 1 [1] 2
ex φ 1 [2] 2
ex φ 1 [3] 2
Assignments
ex φ 1 [1] 1 = 1
ex φ 1 [2] 1 = 0
ex φ 1 [3] 1 = 0
ex φ 1 [1] 2 = 0
ex φ 1 [2] 2 = 1
ex φ 1 [3] 2 = 1
Since the SMT-solver may arbitrarily assign the newly introduced ex φ[p] i -
variables, a constraint has to be added which enforces that each operation in an
experiment is realized by exactly one module. To this end, for each experiment
φ ∈ and each operation φ[p] of φ, all possible instances (represented by ex φ[p] i
with 1 ≤ i ≤ maxI(φ[p])) are considered. Then, it is enforced that only one of them
indeed is realizing the operation, i.e. only one of the corresponding ex φ[p] i -variables
is set to 1. This is accomplished by the constraint
φ∈
|φ|
p=1
⎛
⎝
maxI(φ[p])
i=1
ex φ[p] i
⎞
⎠ = 1.
Next, it has to be ensured that the, respectively, chosen chain of instances
realizing the experiment φ (represented by ex φ[p] i -variables) is indeed also realized
in the graph G. To this end, the e (u,v) -variables have to be restricted depending on
the respective values of the ex φ[p] i -variables. This is enforced by the constraint
φ∈
|φ|−1
p=1
maxI(φ[p])
i=1
maxI(φ[p+1])
j =1
ex φ[p] i ∧ ex φ[p+1] j ⇒ e (φ[p] i ,φ[p+1] j ) ,
which checks for each experiment φ ∈ and each consecutive pair of operations φ[p] and φ[p + 1] whether the instances φ[p] i and φ[p + 1] j are used to
realize them, respectively, (i.e., whether the variables ex φ[p] i and ex φ[p+1] j are set
to 1). If this is true, then it is enforced that G contains a connection between these
modules (i.e., that e (φ[p] i ,φ[p+1] j ) is set to 1). Finally, the edges connecting the MPU
with the first module as well as the last module with the MPU have to be enforced by
φ∈
maxI(φ[1])
i=1
ex φ[1] i ⇒ e (MP U,φ[1] i ) and
φ∈
maxI(φ[|φ|])
i=1
ex φ[|φ|] i ⇒ e (φ[|φ|] i ,MP U ) ,
respectively.