next up previous contents
Next: Bounded Model Checking Up: Translating an expression to Previous: Translating an expression to   Contents

Interconnect synthesis in reconfigurable computing

Figure: Example of a Reconfigurable Computer
Figure: A Programmable Interconnection Network
Figure: A typical routing block
\begin{figure}\centerline{\epsfig{figure=Fig/reconfig_board.eps,width=3in,height...
...ce*{10mm}
\centerline{\epsfig{figure=Fig/Network.eps,width=3.5in}}\end{figure}

Many reconfigurable computers consist of multiple field-programmable processors (FPGAs) connected through a Programmable Interconnect Network (PIN) as shown in Figure [*]. Interconnect synthesis is the process of configuring the PIN to match the communication requirements of the designs implemented on the processors. The general architecture of a PIN is depicted in Figure [*]. A PIN routes signals between various input and output pins of the FPGAs: the specific routing is determined by the control signals on each of the routing blocks. One of many available routing blocks is shown in Figure [*], this one on the well-known Wildforce board.

Typically, but not necessarily, the control signals define a permutation of the inputs of the block and the permuted signals are routed to the corresponding output pins of the block. Each control signal can take a value from $\{T,F\}$ or be unassigned. An assignment of values to control signals is said to be a program of the interconnection network. Thus, a program defines a routing of the signals through the interconnection network. A required routing may be realizable through one or more programs or not realizable at all depending upon the routing capabilities of the interconnection blocks and how they are connected. A configuration of an interconnection network refers to a set of routes realized by a program. Whereas a program defines a configuration, it is not necessary that each configuration is realizable by a unique program.

The problem of interconnect synthesis can be formulated as a problem of determining the satisfiability of a class of QBFs. For a PIN, let $PI$ be the set of primary inputs (those connecting to FPGA outputs), $PO$ be the set of primary outputs (those connecting to FPGA inputs), and $IO$ be the set of intermediate outputs (those not directly accessible through pins). Let $M$ be a desired routing from $PI$ to $PO$ and $Constraints_{M,IO}(PI,PO)$ be a set of contraints which evaluates to T if and only if values on $PO$ match values on a given $PI$ according to $M$ without any inconsistencies among $IO$. The QBFs have the following form:

\begin{displaymath}
\forall ~PI~
\exists ~PO~\&~IO~
s.t.~Constraints_{M,IO}(PI,PO)
\end{displaymath}

For this class, there is an efficient method for eliminating the Quantifiers resulting in a system of quantifier-free formulas that can be determined using ordinary satisfiability solvers. The key idea, called impulse response, is to establish constraints that force exactly one route from a single input to its destination at a time, and to repeat this process for all inputs.

Given an $n$ dimensional Boolean vector $V=\{x_1, x_2, \cdots x_n\}$, define impulse($i$) to be an assignment of F to variable $x_i$ and T to all the other variables in $V$. Clearly, there are $n$ impulses for an $n$ dimensional vector. For each impulse, it is straightforward to build constraints that force the target primary output to take value F and all other primary outputs to take value T while enforcing consistency among intermediate values (an example follows). Call such a constraint, for impulse($i$), $ImpConstraint_{M,IO}(i)$. Then the QBF above can be replaced with the following Boolean expression:

\begin{displaymath}
\wedge_{i=1}^n ImpConstraint_{M,IO}(i) \wedge x_i\equiv F
\wedge_{j\not=i} x_j\equiv T
\end{displaymath}

which, it can be shown, evaluates to T if and only if the QBF above does.

Consider, for example, just the routing block of Figure [*]. The primary inputs are $\{x_1, x_2,
x_3, x_4, s_1, s_2, s_3\}$, the primary outputs are $\{o_1, o_2, o_3,
o_4\}$, and the two intermediate outputs are $\{o_5, o_6\}$. Suppose each subblock $S$ (there are three of them) either routes its two inputs directly to its two outputs (for example, $x_1$ is routed to $o_1$ and $x_2$ is routed to $o_5$ through the upper left subblock if $s_1=F$) or crosses its routes (for example, $x_1$ is routed to $o_5$ and $x_2$ is routed to $o_1$ if $s_1=T$). Then one can write the four equations shown in the Figure that relate primary outputs to primary inputs. Those equations are the basis for the consistency constraints needed.

The precise constraints depend on the routing desired. Suppose we wish to determine whether there is a program (assignment to $\{s_1,
s_2, s_3\}$) that realizes the configuration $x_1$ to $o_1$, $x_2$ to $o_3$, $x_3$ to $o_2$, and $x_4$ to $o_4$. For impulse($1$) the consistency constraints are

$
o_{11}\equiv ite(s_{1}, x_{12}, x_{11})
\wedge o_{12}\equiv ite(s_{3}, o_{16},...
...quiv ite(s_{3}, o_{15}, o_{16})
\wedge o_{14}\equiv ite(s_{2}, x_{13}, x_{14})
$
$
\wedge o_{15}\equiv ite(s_{1}, x_{11}, x_{12})
\wedge o_{16}\equiv ite(s_{2}, x_{14}, x_{13})
$
$
\wedge x_{11}\equiv o_{11}
$
These are conjoined with the constraints forcing impulse($1$) which are
$x_{11}\equiv F\wedge x_{12}\equiv T\wedge x_{13}\equiv T\wedge x_{14}\equiv T$
Similar constraints may be constructed for impulse($2$) through impulse($4$). The conjunction of all four sets of constraints is the Boolean expression of interest: if some assignment to $\{s_1,
s_2, s_3\}$ satisfies that expression, that assignment routes primary inputs to primary outputs as desired. The next step is to write the constraints in canonical form. This is straightforward and the result is shown in Figure [*].

Figure: Interconnect synthesis example in canonical form.
\begin{figure}\begin{verbatim}p bdd 43 32
; Consistency constraints for impu...
...nstraint forcing impulse(4)
and(x41, x42, x43, -x44)\end{verbatim}
\end{figure}


next up previous contents
Next: Bounded Model Checking Up: Translating an expression to Previous: Translating an expression to   Contents
John Franco 2011-09-15