diff options
Diffstat (limited to 'part1.tex')
-rw-r--r-- | part1.tex | 60 |
1 files changed, 50 insertions, 10 deletions
@@ -105,13 +105,15 @@ components, we also allow these values to be swapped: &\land \cdots \nonumber \end{align} -To avoid an overlap between any pair of components $i$ and $j$ (with $i \neq -j$), we add the restriction that each other component $j$ must be located either -below, to the left, above or to the right of a component $i$. +To avoid an overlap between any pair of components $i$ and $j$ (with $i < j$), +we add the restriction that each other component $j$ must be located either +below, to the left, above or to the right of a component $i$. (Note the use of +$i < j$ is sufficient, $i \neq j$ would also have been correct, but due to +symmetry of the overlap check it would contain redundant parts.) \begin{align} \label{eq:chip3} \bigwedge_{0 \leq i < n} -\bigwedge_{0 \leq j < n, i \neq j} +\bigwedge_{i < j < n} y'_j \leq y_i \lor x'_j \leq x_i \lor y_j \geq y'_i \lor @@ -225,26 +227,64 @@ hasOverlap_y(i, j) &= Finally we must add a clause that ensures a difference of at least $powerDistance$ between the centers of any pair of power components $i$, $j$ -(with $i \neq j$). (Note that this is a horizontal or vertical difference, not +(with $i < j$). (Note that this is a horizontal or vertical difference, not the Euclidean one.) Let the center for a power component $i$ be defined by: \begin{align*} cx_i &= x_i + \frac{1}{2}w_i & cy_i &= y_i + \frac{1}{2}h_i \end{align*} -then: +then we have to check pairs that we have not seen yet: \begin{align} \label{eq:chip5} \bigwedge_{0 \leq i < m} -\bigwedge_{0 \leq j < m, i \neq j} +\bigwedge_{i < j < m} cx_i \geq& cx_j + powerDistance \lor cx_j \geq cx_i + powerDistance \lor \\ cy_i \geq& cy_j + powerDistance \lor cy_j \geq cy_i + powerDistance \end{align} -Taking the conjunction of the above parts (\ref{eq:chip1}, \ref{eq:chip2}, -\ref{eq:chip3}, \ref{eq:chip4}, \ref{eq:chip5}), -we obtain a result which is visualized in Figure~\ref{fig:chipDesign}. +We wrote a generator program that takes the conjunction of the above parts +(formulae \ref{eq:chip1}, \ref{eq:chip2}, \ref{eq:chip3}, \ref{eq:chip4}, +\ref{eq:chip5}). Its annotated (partial) output is shown in +Listing~\ref{lst:chipDesign}. Evaluation of this output using +\texttt{python generate-chipdesign.py | z3 -smt -in} finished in 12 seconds. +The result is visualized in Figure~\ref{fig:chipDesign}. +Indeed, the requirements are satisfied. + +\begin{lstlisting}[caption={Generated SMT output for +ChipDesign},label={lst:chipDesign},language=lisp,basicstyle=\scriptsize] +(benchmark test.smt +:logic QF_UFLIA +:extrafuns ((x0 Int) (y0 Int) (w0 Int) (h0 Int) ... +(x11 Int) (y11 Int) (w11 Int) (h11 Int)) +:formula (and +; check requirement 1 (chip width and height) +(>= x0 0) (>= y0 0) (<= (+ x0 w0) 30) (<= (+ y0 h0) 30) +; check requirement 2 or 3 (component width) +(or (and (= w0 4) (= h0 3)) (and (= w0 3) (= h0 4))) +... +(>= x11 0) (>= y11 0) (<= (+ x11 w11) 30) (<= (+ y11 h11) 30) +(or (and (= w11 10) (= h11 20)) (and (= w11 20) (= h11 10))) +; check requirement 4 (no overlap, may be turned) +(or (<= (+ y1 h1) y0) (<= (+ x1 w1) x0) + (>= y1 (+ y0 h0)) (>= x1 (+ x0 w0))) +... +(or (<= (+ y11 h11) y10) (<= (+ x11 w11) x10) + (>= y11 (+ y10 h10)) (>= x11 (+ x10 w10))) +; check requirement 6 (minimum distance between power components) +(or (>= (+ x0 (/ w0 2)) (+ (+ x1 (/ w1 2)) 17)) + ... +) +; check requirement 5 (power for regular components) +(or (and + (or (= (+ y0 h0) y2) (= y0 (+ y2 h2))) + (or (and (<= x2 x0) (<= x0 (+ x2 w2))) + (and (<= x2 (+ x0 w0)) (<= (+ x0 w0) (+ x2 w2))) + )) + ... +)...)) +\end{lstlisting} \begin{figure} \centering |