8.3 Verification
121
Passing this symbolic formulation to an SMT-solver would yield an arbitrary
assignment of the bit vectors and, hence, it is not guaranteed that the droplets
correctly flow through the microfluidic network, that an experiment is executed, or
that no droplets coalesce. Therefore, the assignments of the symbolic formulation
have to be restricted.
Enforcing the Droplet Flow
The hydrodynamic force produced by the pumps causes a flow of the payload and
header droplets through the microfluidic network. To realize this flow, the time a
droplet is already contained in an entity has to be increased in each time step. The
used one-hot encoding allows to do this with a single right shift. Note that this also
handles a droplet leaving an entity because the execution of the right shift operation
drops a 1 contained in the last position (i.e., the execution of the shift operation drops
hd e,t [hSteps(e)] and pd e,t [pSteps(e)]). In the following, the flow of the header
droplets is formally discussed. Likewise, it is applied to the bit vectors representing
payload droplets.
The flow of header droplets is formally enforced as
e∈C∪M
T up +T maxP ath
t=1
hd e,t = (hd e,t−1 1) ∨ .
(8.1)
Equation 8.1 executes a single right shift on the bit vector hd e,t−1 of time t−1 and
assigns this value to bit vector hd e,t . However, it does not consider the droplet flow
between entities (e.g., a droplet leaving an entity and entering the successor entity).
Depending on the entity e, three cases have to be differentiated for the droplet flow
between entities (replacing the placeholder
of Eq. 8.1):
• In case e is the input channel, new droplets are injected into this channel within
the first T up time steps. The injection sequence of headers is represented by the
vector inj H . A 1 (i.e., inj H [t] = 1) represents the injection of a new header in
time t. This motivates the following replacement:
= inj H [t].
(8.2)
• In case e is a successor channel of a bifurcation, a droplet only flows into
channel e, if it has fewer time steps than the other successor channel of the
bifurcation and it does not already contain droplets. Therefore, let f be the
channel before the bifurcation (i.e., the predecessor of e). Three requirements
have to be fulfilled so that a droplet flows into the channel e in time step t:
(1) there has to be a header droplet, which leaves the predecessor f in the next
time step t (i.e., part 1 of Eq. 8.3), (2) the channel e itself does not already contain
droplets (which would have increased the hydraulic resistance) (i.e., part 2 of
121
Passing this symbolic formulation to an SMT-solver would yield an arbitrary
assignment of the bit vectors and, hence, it is not guaranteed that the droplets
correctly flow through the microfluidic network, that an experiment is executed, or
that no droplets coalesce. Therefore, the assignments of the symbolic formulation
have to be restricted.
Enforcing the Droplet Flow
The hydrodynamic force produced by the pumps causes a flow of the payload and
header droplets through the microfluidic network. To realize this flow, the time a
droplet is already contained in an entity has to be increased in each time step. The
used one-hot encoding allows to do this with a single right shift. Note that this also
handles a droplet leaving an entity because the execution of the right shift operation
drops a 1 contained in the last position (i.e., the execution of the shift operation drops
hd e,t [hSteps(e)] and pd e,t [pSteps(e)]). In the following, the flow of the header
droplets is formally discussed. Likewise, it is applied to the bit vectors representing
payload droplets.
The flow of header droplets is formally enforced as
e∈C∪M
T up +T maxP ath
t=1
hd e,t = (hd e,t−1 1) ∨ .
(8.1)
Equation 8.1 executes a single right shift on the bit vector hd e,t−1 of time t−1 and
assigns this value to bit vector hd e,t . However, it does not consider the droplet flow
between entities (e.g., a droplet leaving an entity and entering the successor entity).
Depending on the entity e, three cases have to be differentiated for the droplet flow
between entities (replacing the placeholder
of Eq. 8.1):
• In case e is the input channel, new droplets are injected into this channel within
the first T up time steps. The injection sequence of headers is represented by the
vector inj H . A 1 (i.e., inj H [t] = 1) represents the injection of a new header in
time t. This motivates the following replacement:
= inj H [t].
(8.2)
• In case e is a successor channel of a bifurcation, a droplet only flows into
channel e, if it has fewer time steps than the other successor channel of the
bifurcation and it does not already contain droplets. Therefore, let f be the
channel before the bifurcation (i.e., the predecessor of e). Three requirements
have to be fulfilled so that a droplet flows into the channel e in time step t:
(1) there has to be a header droplet, which leaves the predecessor f in the next
time step t (i.e., part 1 of Eq. 8.3), (2) the channel e itself does not already contain
droplets (which would have increased the hydraulic resistance) (i.e., part 2 of