diff --git a/report/Makefile b/report/Makefile index 935279d..1db03ae 100644 --- a/report/Makefile +++ b/report/Makefile @@ -5,3 +5,6 @@ all: upload: scp report.pdf www.tobast:~/tobast.fr/public_html/m1/internship.pdf + +upload-alt: + scp report.pdf www.tobast:~/tobast.fr/public_html/m1/internship.tmp.pdf diff --git a/report/img/mux_of_tri.png b/report/img/mux_of_tri.png new file mode 100644 index 0000000..91b352b Binary files /dev/null and b/report/img/mux_of_tri.png differ diff --git a/report/img/mux_of_tri/mux_of_tri.dot b/report/img/mux_of_tri/mux_of_tri.dot new file mode 100644 index 0000000..0b1f954 --- /dev/null +++ b/report/img/mux_of_tri/mux_of_tri.dot @@ -0,0 +1,33 @@ +digraph mux { + rankdir = LR; + + if0 [shape=triangle, orientation=270]; + if1 [shape=triangle, orientation=270]; + prenot [shape=point, width=0]; + not [shape=triangle, orientation=180]; + + in0 [shape=point]; + sel [shape=point]; + in1 [shape=point]; + + preout [shape=point, width=0]; + out [shape=point, label=out]; + + edge [weight=1]; + + sel -> prenot [label=select, arrowhead=none]; + prenot -> if1 [arrowhead=normal, tailport=s, headport=n]; + prenot -> not [headport=n]; + in0 -> if0 [label=in0, headport=w]; + in1 -> if1 [label=in1, headport=w]; + + if0 -> preout [tailport=e, arrowhead=none]; + if1 -> preout [tailport=e, arrowhead=none]; + + preout -> out [label=out]; + + not -> if0 [weight=42, headport=n, tailport=s, arrowtail=invodot]; + + {rank=same; sel ; in0 ; in1; } + {rank=same; if0 ; if1; prenot; not;} +} diff --git a/report/report.tex b/report/report.tex index 2c6a3db..ff7e2a4 100644 --- a/report/report.tex +++ b/report/report.tex @@ -761,7 +761,19 @@ the memoized results (essentially the signatures) are kept for the second one, considerably speeding it up: the same program proving only one way takes about \textbf{475\,ms}. \todo{explain why} +\paragraph{Match.} The subcircuit match feature was tested by trying to find +every occurrence of a pattern that can be easily found using tools like +\lstbash{grep}. For this purpose, the ad-hoc implementation of a MUX gate was +used: two tristate gates and a NOT gate, as in Figure~\ref{fig:mux_of_tri}. +\begin{figure}[h] + \centering + \includegraphics[height=6cm]{img/mux_of_tri.png} + \caption{MUX gate made out of tristate and not gates}\label{fig:mux_of_tri} +\end{figure} + +This group appears 73 times in the processor. To match them all (none are +overlapping), it takes \textbf{\qtodo{todo}\,ms}. \subsection{Corner cases}\label{ssec:corner_cases}