Commit 25594172 authored by Jules Saget's avatar Jules Saget
Browse files

Continue working on report (the end is near!)

parent 1da5cec8
......@@ -9,8 +9,8 @@
.DEFAULT_GOAL := main.pdf
%.pdf %.aux %.idx: %.tex figs %.bbl
pdflatex $<
%.pdf %.aux %.idx: %.tex figs tables %.bbl
pdflatex -shell-escape $<
if grep 'Rerun to get ' $*.log ; then make $@ ; fi
if grep 'There were undefined references' $*.log ; then exit 1 ; fi
if grep 'Please (re)run Biber' $*.log ; then make $*.bbl ; make $@ ; fi
......@@ -19,11 +19,14 @@
biber $*
%.bcf: %.tex
pdflatex $<
pdflatex -shell-escape $<
figs:
make -C figures
tables:
make -C tables
clean:
make -C figures clean
rm -f *.bbl
......
figs: comparator.pdf simple_graph_reductions.pdf ski_combinators.pdf 4ph.pdf
figs: comparator.pdf simple_graph_reductions.pdf ski_combinators.pdf 4ph.pdf andor.png add-sub.pdf mul.pdf clean.pdf
%.pdf: %.gv
dot -o$@ -Tpdf $<
......
digraph addsub_FSM {
subgraph cluster_AB {
style = filled;
color = white;
AB_ALLOC -> AB_WRITE -> AB_READ_A -> AB_READ_B -> AB_ADDSUB -> AB_ALLOC;
label = "A unfinished, B unfinished";
}
subgraph cluster_A {
style = filled;
color = white;
A_CHECK [style = filled, color = lightgrey];
A_CHECK -> A_ALLOC -> A_WRITE -> A_READ -> A_ADDSUB -> A_CHECK;
A_CHECK -> A_LINK;
label = "A unfinished, B finished";
}
subgraph cluster_FINAL {
style = filled;
color = white;
FINAL_CHECK [style = filled, color = lightgrey];
FINAL_CHECK -> FINAL_LINK;
FINAL_CHECK -> FINAL_ALLOC -> FINAL_WRITE -> FINAL_WAIT -> FINAL_LAST_WRITE;
label = "A finished, B finished"
}
subgraph cluster_B {
style = filled;
color = white;
B_CHECK [style = filled, color = lightgrey];
B_CHECK -> B_LINK;
B_CHECK -> B_ALLOC -> B_WRITE -> B_READ -> B_ADDSUB -> B_CHECK;
label = "A finished, B unfinished";
}
IDLE -> AB_READ_A;
AB_ADDSUB -> A_CHECK;
AB_ADDSUB -> B_CHECK;
AB_ADDSUB -> FINAL_CHECK;
A_LINK -> DONE;
B_LINK -> DONE;
FINAL_LINK -> DONE;
FINAL_LAST_WRITE -> DONE;
A_CHECK -> FINAL_CHECK;
B_CHECK -> FINAL_CHECK;
}
digraph clean_FSM {
rankdir="LR";
IDLE;
PRE_READ [style = filled, color = lightgrey];
WAIT_READ;
READ;
UPDATE;
CHECK [style = filled, color = lightgrey];
FINAL_CHECK [style = filled, color = lightgrey];
WRITE;
DONE;
{ rank = same; PRE_READ, READ, UPDATE }
IDLE -> PRE_READ;
PRE_READ -> WAIT_READ;
WAIT_READ -> PRE_READ;
PRE_READ -> READ;
READ -> UPDATE;
UPDATE -> CHECK;
CHECK -> PRE_READ;
CHECK -> FINAL_CHECK;
FINAL_CHECK -> WRITE;
FINAL_CHECK -> DONE;
WRITE -> DONE;
}
digraph addsub_FSM {
rankdir="LR";
subgraph cluster_A {
style = filled;
......
digraph mul_FSM {
node [style = filled, color=black, fillcolor = white];
IDLE;
DONE;
{ rank = same; IDLE, DONE }
subgraph cluster_A {
label = "Read A loop (outer loop)";
style = filled;
color = azure1;
READ_A;
A_LOOP_CHECK [color = invis, fillcolor = lightgrey];
{ rank = same; READ_A, A_LOOP_CHECK }
subgraph cluster_B {
label = "Read B loop (inner loop)";
style = filled;
color = azure2;
READ_B;
MUL;
B_LOOP_CHECK [color = invis, fillcolor = lightgrey];
{ rank = same; B_LOOP_CHECK, READ_B, MUL }
subgraph cluster_ADD {
style = filled;
color = azure3;
label = "Add loop";
READY_RES [color=invis, fillcolor = lightgrey];
READ_RES;
ADD;
READY_ADDRESS [color=invis, fillcolor = lightgrey];
ALLOC;
WRITE;
ADD_LOOP_CHECK [color=invis, fillcolor = lightgrey];
{ rank = same; READY_RES, ADD, READY_ADDRESS, WRITE, ADD_LOOP_CHECK }
READY_RES -> ADD -> READY_ADDRESS -> WRITE ->
ADD_LOOP_CHECK -> READY_RES;
READY_RES -> READ_RES -> ADD;
READY_ADDRESS -> ALLOC -> WRITE;
}
ADD_LOOP_CHECK -> B_LOOP_CHECK -> READ_B -> MUL -> READY_RES;
}
B_LOOP_CHECK -> A_LOOP_CHECK -> READ_A -> READ_B;
}
A_LOOP_CHECK -> DONE;
DONE -> IDLE [color = invis];
IDLE -> READ_A;
}
This diff is collapsed.
......@@ -20,7 +20,7 @@
publisher = {Prentice-Hall},
}
@MANUAL{VossManual,
@MANUAL{VossII-manual,
author = {Seger, Carl-Johan H.},
title = {fl --- A Functional Language for Formal Verification: User's
Guide},
......@@ -39,6 +39,16 @@
note = {Submitted}
}
@MISC{stately-git,
author = {Jeremy Pope},
title = {Stately},
year = {2020},
publisher = {GitHub},
journal = {GitHub repository},
howpublished = {\url{https://github.com/popje-chalmers/stately}}
}
@UNPUBLISHED{CEPHALOPODE,
author = {Jeremy Pope and Jules Saget and Carl-Johan H. Seger},
title = {{CEPHALOPODE}: A custom processor aimed at functional
......@@ -70,8 +80,6 @@
doi = {10.1145/74818.74828}
}
@ARTICLE{VTech,
author = {Daniel Victor},
date = {2015-11-30},
......
tables: arith_2cpl.tex arith_ex_clean.tex arith_ex_gonewrong.tex arith_ex_simple.tex mul_2by2.tex
......@@ -5,6 +5,7 @@
\setlength{\tabcolsep}{4pt}
\begin{table}[h]
\centering
\begin{tabular}{rl|rcc|rcc|r}
\multicolumn{2}{c|}{\multirow{2}{*}{State}} & \multicolumn{3}{c|}{A} & \multicolumn{3}{c|}{B} & \multicolumn{1}{c}{\multirow{2}{*}{Res}} \\
\multicolumn{2}{c|}{} & \multicolumn{1}{c}{Mem} & End & $\pm$ & \multicolumn{1}{c}{Mem} & End & $\pm$ & \multicolumn{1}{c}{} \\ \hline
......
......@@ -4,6 +4,7 @@
\def\oldtabcolsep{\tabcolsep}
\setlength{\tabcolsep}{4pt}
\begin{table}[h]
\centering
\begin{tabular}{rl|rcc|rcc|r}
\multicolumn{2}{c|}{\multirow{2}{*}{State}} & \multicolumn{3}{c|}{A}
& \multicolumn{3}{c|}{B} &
......
% Please add the following required packages to your document preamble:
% \usepackage{multirow}
\begin{table}[h]
\centering
\begin{tabular}{rl|rcc|rcc|l}
\multicolumn{2}{c|}{\multirow{2}{*}{State}} & \multicolumn{3}{c|}{A} & \multicolumn{3}{c|}{B} & \multicolumn{1}{c}{\multirow{2}{*}{Res}} \\
\multicolumn{2}{c|}{} & \multicolumn{1}{c}{Mem} & End & $\pm$ & \multicolumn{1}{c}{Mem} & End & $\pm$ & \multicolumn{1}{c}{} \\ \hline
......
% Please add the following required packages to your document preamble:
% \usepackage{multirow}
% \usepackage[table,xcdraw]{xcolor}
% If you use beamer only pass "xcolor=table" option, i.e. \documentclass[xcolor=table]{beamer}
\begin{table}[ht]
\footnotesize
\centering
\begin{tabular}{c|cc|cc|cc|ccccc|cccc}
& \multicolumn{2}{c|}{} & \multicolumn{2}{c|}{} & \multicolumn{2}{c|}{} & \multicolumn{5}{c|}{ADD} & \multicolumn{4}{c|}{} \\
& \multicolumn{2}{c|}{} & \multicolumn{2}{c|}{} & \multicolumn{2}{c|}{} & \multicolumn{3}{c|}{inputs} & \multicolumn{2}{c|}{outputs} & \multicolumn{4}{c|}{} \\
\multirow{-3}{*}{State} & \multicolumn{2}{c|}{\multirow{-3}{*}{A}} & \multicolumn{2}{c|}{\multirow{-3}{*}{B}} & \multicolumn{2}{c|}{\multirow{-3}{*}{MUL}} & in1 & in2 & c & res & c & \multicolumn{4}{c|}{\multirow{-3}{*}{Result}} \\ \hline
IDLE & 010 & ·111 & 011 & 111 & & & & & & & & \textit{} & & & \\
\rowcolor[HTML]{EFEFEF}
READ\_A & 010 & \textbf{·111} & 011 & 111 & & & & & & & & \textit{} & & & \\
READ\_B & 010 & \textbf{·111} & 011 & \textbf{111} & & & & & & & & \textit{} & & & \\
\rowcolor[HTML]{EFEFEF}
MUL & 010 & \textbf{·111} & 011 & \textbf{111} & 110 & 001 & & & & & & \textit{} & & & \\
ADD & 010 & \textbf{·111} & 011 & \textbf{111} & & & 001 & 000 & 0 & 001 & 0 & & & & \\
\rowcolor[HTML]{EFEFEF}
ALLOC & 010 & \textbf{·111} & 011 & \textbf{111} & & & & & & & & & & & \\
WRITE & 010 & \textbf{·111} & 011 & \textbf{111} & & & & & & & & & & & \textit{·001} \\
\rowcolor[HTML]{EFEFEF}
ADD & 010 & \textbf{·111} & 011 & \textbf{111} & & & 110 & 000 & 0 & 110 & 0 & & & & \textit{·001} \\
ALLOC & 010 & \textbf{·111} & 011 & \textbf{111} & & & & & & & & & & & \textit{·001} \\
\rowcolor[HTML]{EFEFEF}
WRITE & 010 & \textbf{·111} & 011 & \textbf{111} & & & & & & & & & & \textit{·110} & ·001 \\
READ\_B & 010 & \textbf{·111} & \textbf{011} & 111 & & & & & & & & & & \textit{·110} & ·001 \\
\rowcolor[HTML]{EFEFEF}
MUL & 010 & \textbf{·111} & \textbf{011} & 111 & 010 & 101 & & & & & & & & \textit{·110} & ·001 \\
READ\_RES & 010 & \textbf{·111} & \textbf{011} & 111 & & & & & & & & \textbf{} & & \textit{\textbf{·110}} & ·001 \\
\rowcolor[HTML]{EFEFEF}
ADD & 010 & \textbf{·111} & \textbf{011} & 111 & & & 101 & 110 & 0 & 011 & 1 & \textbf{} & & \textit{\textbf{·110}} & ·001 \\
WRITE & 010 & \textbf{·111} & \textbf{011} & 111 & & & & & & & & & & \textit{·011} & ·001 \\
\rowcolor[HTML]{EFEFEF}
ADD & 010 & \textbf{·111} & \textbf{011} & 111 & & & 010 & 000 & 1 & 011 & 0 & & & \textit{·011} & ·001 \\
ALLOC & 010 & \textbf{·111} & \textbf{011} & 111 & & & & & & & & & & \textit{·011} & ·001 \\
\rowcolor[HTML]{EFEFEF}
WRITE & 010 & \textbf{·111} & \textbf{011} & 111 & & & & & & & & & \textit{·011} & ·011 & ·001 \\
READ\_A & \textbf{010} & ·111 & \textbf{011} & 111 & & & & & & & & & \textit{·011} & ·011 & ·001 \\
\rowcolor[HTML]{EFEFEF}
READ\_B & \textbf{010} & ·111 & 011 & \textbf{111} & & & & & & & & & \textit{·011} & ·011 & ·001 \\
MUL & \textbf{010} & ·111 & 011 & \textbf{111} & 001 & 110 & & & & & & & \textit{·011} & ·011 & ·001 \\
\rowcolor[HTML]{EFEFEF}
READ\_RES & \textbf{010} & ·111 & 011 & \textbf{111} & & & & & & & & \textbf{} & \textit{·011} & \textbf{·011} & ·001 \\
ADD & \textbf{010} & ·111 & 011 & \textbf{111} & & & 110 & 011 & 0 & 001 & 1 & \textbf{} & \textit{·011} & \textbf{·011} & ·001 \\
\rowcolor[HTML]{EFEFEF}
WRITE & \textbf{010} & ·111 & 011 & \textbf{111} & & & & & & & & & ·011 & \textit{·001} & ·001 \\
READ\_RES & \textbf{010} & ·111 & 011 & \textbf{111} & & & & & & & & \textbf{} & \textbf{·011} & \textit{·001} & ·001 \\
\rowcolor[HTML]{EFEFEF}
ADD & \textbf{010} & ·111 & 011 & \textbf{111} & & & 001 & 011 & 1 & 101 & 0 & \textbf{} & \textbf{·011} & \textit{·001} & ·001 \\
WRITE & \textbf{010} & ·111 & 011 & \textbf{111} & & & & & & & & & \textit{·101} & ·001 & ·001 \\
\rowcolor[HTML]{EFEFEF}
READ\_B & \textbf{010} & ·111 & \textbf{011} & 111 & & & & & & & & & \textit{·101} & ·001 & ·001 \\
MUL & \textbf{010} & ·111 & \textbf{011} & 111 & 000 & 110 & & & & & & & \textit{·101} & ·001 & ·001 \\
\rowcolor[HTML]{EFEFEF}
READ\_RES & \textbf{010} & ·111 & \textbf{011} & 111 & & & & & & & & \textbf{} & \textit{\textbf{·101}} & ·001 & ·001 \\
ADD & \textbf{010} & ·111 & \textbf{011} & 111 & & & 110 & 101 & 0 & 011 & 1 & & \textit{\textbf{·101}} & ·001 & ·001 \\
\rowcolor[HTML]{EFEFEF}
WRITE & \textbf{010} & ·111 & \textbf{011} & 111 & & & & & & & & \textbf{} & \textit{·011} & ·001 & ·001 \\
ADD & \textbf{010} & ·111 & \textbf{011} & 111 & & & 000 & 000 & 1 & 001 & 0 & & \textit{·011} & ·001 & ·001 \\
\rowcolor[HTML]{EFEFEF}
WRITE & \textbf{010} & ·111 & \textbf{011} & 111 & & & & & & & & \textit{001} & \cellcolor[HTML]{EFEFEF}·011 & ·001 & ·001 \\
DONE & \textbf{010} & ·111 & \textbf{011} & 111 & & & & & & & & \textit{001} & ·011 & ·001 & ·001
\end{tabular}
\caption{Example of multiplication}
\label{tab:mul_2by2}
\end{table}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment