summaryrefslogtreecommitdiffstats
path: root/chapters/pipelining.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-05-05 17:08:12 +0100
committerYann Herklotz <git@yannherklotz.com>2022-05-05 17:08:12 +0100
commitc9648f2dc56a0c970a90e1539925ae78b0610fbc (patch)
tree41a7934ad8d327684e33038b0e7f63d7bfe407dc /chapters/pipelining.tex
parentb90e207d5a9d1871d5ecde168d39ce91c7691fe1 (diff)
downloadlsr22_fvhls-c9648f2dc56a0c970a90e1539925ae78b0610fbc.tar.gz
lsr22_fvhls-c9648f2dc56a0c970a90e1539925ae78b0610fbc.zip
First realistic draft
Diffstat (limited to 'chapters/pipelining.tex')
-rw-r--r--chapters/pipelining.tex7
1 files changed, 4 insertions, 3 deletions
diff --git a/chapters/pipelining.tex b/chapters/pipelining.tex
index 09fae11..b0bdb20 100644
--- a/chapters/pipelining.tex
+++ b/chapters/pipelining.tex
@@ -168,9 +168,10 @@ all, the proof from the paper was actually never fully completed:
location=middle,
width=\dimexpr \textwidth - 1cm \relax,
]
- {\noindent\it [Semantic preservation going from unrolled loops in a basic-block representation to
- the actual loops in a CFG] is intuitively obvious but surprisingly tedious to formalize in full
- details: indeed, this is the only result in this paper that we have not yet mechanized in Coq.}
+ {\noindent\it [Semantic preservation going from unrolled loops in a basic block representation to
+ the actual loops in a CFG] is intuitively obvious but surprisingly tedious to formalize in
+ full details: indeed, this is the only result in this paper that we have not yet mechanized in
+ Coq.}
\startalignment[flushright]
--- \cite[alternative=authoryears,right={, Section