summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-05-03 08:00:29 +0100
committerYann Herklotz <git@yannherklotz.com>2022-05-03 08:00:29 +0100
commit7458e17b2bf5b3c6f342731510f1be589851c3a0 (patch)
tree96076f7ba48c7a76e5a6320fa13a738a7ac92194
parent1e411adb9dcb79858ce26a11513ce9114916bc42 (diff)
downloadlsr22_fvhls-7458e17b2bf5b3c6f342731510f1be589851c3a0.tar.gz
lsr22_fvhls-7458e17b2bf5b3c6f342731510f1be589851c3a0.zip
Add pipelining notes
Diffstat
-rw-r--r--Makefile4
-rw-r--r--chapters/background.tex6
-rw-r--r--chapters/hls.tex13
-rw-r--r--chapters/introduction.tex5
-rw-r--r--chapters/pipelining.tex49
-rw-r--r--chapters/pipelining_notes.org57
-rw-r--r--chapters/scheduling.tex243
-rw-r--r--fonts_env.tex10
-rw-r--r--lsr_env.tex50
-rw-r--r--lsr_refs.bib1584
-rw-r--r--title.tex4
11 files changed, 1023 insertions, 1002 deletions
diff --git a/Makefile b/Makefile
index 55c4e4f..98d14cc 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,5 @@
+MODE ?= main
+
.PHONY: all clean
all: main.pdf
@@ -10,5 +12,5 @@ figures/%.pdf: figures/%.tex
# silent structure,structures,pages,resolvers,open source,close source,loading,modules
%.pdf: %.tex
- context --nonstopmode --silent='*' $<
+ context --mode=$(MODE) --nonstopmode --silent='*' $<
cp $(notdir $@) $@ || true
diff --git a/chapters/background.tex b/chapters/background.tex
index 305f72a..51a6632 100644
--- a/chapters/background.tex
+++ b/chapters/background.tex
@@ -387,7 +387,9 @@ correct manner. In addition to that, the assumption is made that the semantics
same in Handel-C as well as in the netlist format that is generated, which could be proven if the
constructs are shown to behave in the exact same way as the handel-C constructs.
-% \section{Bibliography}
-% \placelistofpublications
+\startmode[section]
+ \section{Bibliography}
+ \placelistofpublications
+\stopmode
\stopcomponent
diff --git a/chapters/hls.tex b/chapters/hls.tex
index 5e7237a..90dc238 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -104,8 +104,8 @@ formal semantics.
\hbox{\starttikzpicture [language/.style={fill=white,rounded corners=3pt,minimum height=7mm},
continuation/.style={},
linecount/.style={rounded corners=3pt,dashed}]
- \fill[compcert,rounded corners=3pt] (-1,-0.5) rectangle (9.9,2);
- \fill[formalhls,rounded corners=3pt] (-1,-1) rectangle (9.9,-2.4);
+ \fill[compcert,rounded corners=3pt] (-1.2,-0.5) rectangle (10.2,2);
+ \fill[formalhls,rounded corners=3pt] (-1.2,-1) rectangle (10.2,-2.4);
%\draw[linecount] (-0.95,-0.45) rectangle (3.6,1);
%\draw[linecount] (4,-0.45) rectangle (7.5,1);
\node[language] at (-0.3,0) (clight) {Clight};
@@ -124,7 +124,7 @@ formal semantics.
%%\node[anchor=west] at (-0.9,0.7) {\small $\sim$ 27 kloc};
%%\node[anchor=west] at (4.1,0.7) {\small $\sim$ 46 kloc};
%%\node[anchor=west] at (2,-1.5) {\small $\sim$ 17 kloc};
- \node[align=center] at (3.2,-2) {RAM\blank insertion};
+ \node[align=center] at (3.2,-2) {RAM\\[-0.5ex]insertion};
\draw[->,thick] (clight) -- (conta);
\draw[->,thick] (conta) -- (cminor);
\draw[->,thick] (cminor) -- (rtl);
@@ -186,8 +186,9 @@ Vericert, this event is either a positive (rising) or a negative (falling) clock
always-blocks triggering on the same event are executed in parallel. Always-blocks can also express
control-flow using if-statements and case-statements.
-\startplacemarginfigure[reference={fig:tutorial:state_machine},title={Hello}]
- \startfloatcombination [nx=2, ny=1]
+\startplacemarginfigure[reference={fig:tutorial:state_machine},title={Example of a state machine
+ implementation in Verilog and it's corresponding state diagram.}]
+ \startfloatcombination[nx=2, ny=1]
\startplacesubfigure
\startframedtext[width={0.9\textwidth},frame=off,offset=none,loffset=3cm,bodyfont=11pt]
\starthlverilog
@@ -213,7 +214,7 @@ control-flow using if-statements and case-statements.
\stopplacesubfigure
\startplacesubfigure
\hbox{\starttikzpicture
- \node[draw,circle,inner sep=6pt,fill=red] (s0) at (0,0) {$S_{\mathit{start}} / \mono{x}$};
+ \node[draw,circle,inner sep=6pt] (s0) at (0,0) {$S_{\mathit{start}} / \mono{x}$};
\node[draw,circle,inner sep=8pt] (s1) at (1.5,-3) {$S_{1} / \mono{1}$};
\node[draw,circle,inner sep=8pt] (s2) at (3,0) {$S_{0} / \mono{1}$};
\node (s2s) at ($(s2.west) + (-0.3,1)$) {\mono{00}};
diff --git a/chapters/introduction.tex b/chapters/introduction.tex
index 7ab9d47..55ed41b 100644
--- a/chapters/introduction.tex
+++ b/chapters/introduction.tex
@@ -109,4 +109,9 @@ a fork of CompCert which implements \SSA\ as an intermediate language.
\desc{\in{Chapter}[sec:schedule]} describes the current implementation timeline.
+\startmode[section]
+ \section{Bibliography}
+ \placelistofpublications
+\stopmode
+
\stopcomponent
diff --git a/chapters/pipelining.tex b/chapters/pipelining.tex
index 9bdacc1..6c351c8 100644
--- a/chapters/pipelining.tex
+++ b/chapters/pipelining.tex
@@ -15,9 +15,52 @@ Standard instruction scheduling only addresses parallelisation inside hyperblock
sections of code. However, loops are often the most critical sections in code, and scheduling only
addresses parallelisation within one iteration.
-\section{Introduction to loop pipelining}
+\section{Loop pipelining example}
-\section{Bibliography}
-\placelistofpublications
+\startplacemarginfigure[location=here,reference={fig:pipelined-loop},title={Example of pipelining a
+ loop.}]
+ \startfloatcombination[nx=2]
+
+ \startplacesubfigure[title={Simple loop containing an accumulation of values with an
+ inter-iteration dependency.}]
+ \startframedtext[frame=off,offset=none,width={0.6\textwidth}]
+ \starthlC
+ for (int i = 1; i < N; i++) {
+ c1 = acc[i-1] * c;
+ c2 = x[i] * y[i];
+ acc[i] = c1 + c2;
+ }
+ \stophlC
+ \stopframedtext
+ \stopplacesubfigure
+
+ \startplacesubfigure[title={Pipelined loop reducing the number of dependencies inside of the
+ loop.}]
+ \startframedtext[frame=off,offset=none,width={0.6\textwidth}]
+ \starthlC
+ c1 = acc[0] * c;
+ c2 = x[1] * y[1];
+ for (int i = 1; i < N-1; i++) {
+ acc[i] = c1 + c2;
+ c2 = x[i+1] * y[i+1];
+ c1 = acc[i+1] * c;
+ }
+ acc[N-1] = c1 + c2;
+ \stophlC
+ \stopframedtext
+ \stopplacesubfigure
+
+ \stopfloatcombination
+\stopplacemarginfigure
+
+\in{Figure}[fig:pipelined-loop] shows an example of pipelining a loop which accumulates values and
+modifies an array. In \in{Figure}{a}[fig:pipelined-loop], the body of the loop cannot be scheduled
+in less than three cycles, assuming that a load takes two clock cycles. However, after transforming
+the code into the pipelined version on the right
+
+\startmode[section]
+ \section{Bibliography}
+ \placelistofpublications
+\stopmode
\stopcomponent
diff --git a/chapters/pipelining_notes.org b/chapters/pipelining_notes.org
new file mode 100644
index 0000000..0680800
--- /dev/null
+++ b/chapters/pipelining_notes.org
@@ -0,0 +1,57 @@
+A1 x18 = x6 + -1 (int)
+R1 x16 = int32[x4 + x18 * 4 + 0]
+M1 x8 = x16 * x1
+R2 x12 = int32[x3 + x6 * 4 + 0]
+R3 x13 = int32[x2 + x6 * 4 + 0]
+M2 x7 = x12 * x13
+A2 x11 = x8 + x7 + 0 (int)
+W1 int32[x4 + x6 * 4 + 0] = x11
+A3 x6 = x6 + 1 (int)
+
+| N%3 | N%2 | N | Add1 | Add2 | Add3 | Mult1 | Mult2 | Mem1 | Mem2 | Mem3 |
+|-----+-----+---+------+------+------+-------+-------+------+------+------|
+| 0 | 0 | 0 | A1 | | | | | | R2 | R3 |
+| 1 | 1 | 1 | | | | | | R1 | | |
+| 2 | 0 | 2 | | | | | M2 | | | |
+| 0 | 1 | 3 | | | | M1 | | | | |
+| 1 | 0 | 4 | | A2 | | | | | | |
+| 2 | 1 | 5 | | | A3 | | | W1 | | |
+
+| N | Add1 | Add2 | Add3 | Mult1 | Mult2 | Mem1 | Mem2 | Mem3 |
+|---+------+--------+--------+--------+-------+--------+------+------|
+| 0 | n:A1 | | | n-1:M1 | | | n:R2 | n:R3 |
+| 1 | | n-1:A2 | | | | n:R1 | | |
+| 2 | | | n-1:A3 | | n:M2 | n-1:W1 | | |
+
+| Instr | Stage | Code |
+|-------+-------+----------------------------------------------------------------|
+| 0 | 0 | ~x18 = x6 - 1~, ~x12 = int32[x3+x6*4]~, ~x13 = int32[x3+x6*4]~ |
+| | 1 | ~x8 = x16 * x1~ |
+| 1 | 0 | ~x16 = int32[x4+x18*4]~ |
+| | 1 | ~x11 = x8 + x7~ |
+| 2 | 0 | ~x7 = x12 * x13~ |
+| | 1 | ~x6 = x6 + 1~, ~int32[x4+x6*4] = x11~ |
+
+| N%3 | N%2 | N | Add1 | Add2 | Add3 | Mult1 | Mult2 | Mem1 | Mem2 | Mem3 |
+|-----+-----+---+------+------+------+-------+-------+------+------+------|
+| 0 | 0 | 0 | A1 | | | | | | R2 | R3 |
+| 1 | 1 | 1 | | | | | | R1 | | |
+| 2 | 0 | 2 | | | | | M2 | | | |
+| 0 | 1 | 3 | | | | M1 | | | | |
+| 1 | 0 | 4 | | A2 | | | | | | |
+| 2 | 1 | 5 | | | | | | | | |
+| 0 | 0 | 6 | | | A3 | | | W1 | | |
+
+| N | Add1 | Add2 | Add3 | Mult1 | Mult2 | Mem1 | Mem2 | Mem3 |
+|---+------+--------+--------+--------+--------+--------+------+------|
+| 0 | n:A1 | n-2:A2 | n-3:A3 | | n-1:M2 | n-3:W1 | n:R2 | n:R3 |
+| 1 | | | | n-1:M1 | | n:R1 | | |
+
+| Instr | Stage | Code |
+|-------+-------+-------------------------------------------------------------------|
+| 0 | 0 | ~x18 = x6 - 1~, ~x16 = int32[x4+x18*4+0]~, ~x12 = int32[x3+x6*4]~ |
+| | 1 | ~x7 = x12 * x13~ |
+| | 2 | ~x11 = x8 + x7~ |
+| | 3 | ~x6 = x6 + 1~, ~int32[x4+x6*4] = x11~ |
+| 1 | 0 | ~x16 = int32[x4+x18*4]~ |
+| | 1 | ~x8 = x16 * x1~ |
diff --git a/chapters/scheduling.tex b/chapters/scheduling.tex
index 2463099..75ae1fd 100644
--- a/chapters/scheduling.tex
+++ b/chapters/scheduling.tex
@@ -32,18 +32,18 @@ the performance. Trace scheduling~ is an alternative that addresses this issue,
that might cross branching instructions, and scheduling the instructions in that path. However, the
main problem with trace scheduling is that it is often infeasible on large programs, and because of
the large design space, it's sometimes hard to find an optimal
-schedule. \index{superblock}Superblock~ and \index{hyperblock}hyperblock~ scheduling are two subsets
-of trace scheduling, which compromise on the flexibility of trace scheduling to instead build more
-tractable algorithms. Superblock scheduling produces more efficient code for processors with a low
-issue rate, whereas hyperblock scheduling produces more performant code for processors with a high
-issue rate~.
-
-CompCert~ is a compiler that is formally verified in Coq. In addition to that, have also added a
-formally verified hardware back end to CompCert, allowing it to also generate provably correct
-hardware designs. A hardware back end is an ideal target for hyperblock scheduling, as the issue
-rate is practically infinite. This paper describes the implementation of a hyperblock instruction
-scheduler in CompCert so that it can benefit existing CompCert back ends, as well as support more
-general targets such as scheduling instructions for custom hardware.
+schedule. \index{superblock}Superblock~\cite[hwu93_super] and
+\index{hyperblock}hyperblock~\cite[mahlke92_effec_compil_suppor_predic_execut_using_hyper]
+scheduling are two subsets of trace scheduling, which compromise on the flexibility of trace
+scheduling to instead build more tractable algorithms. Superblock scheduling produces more
+efficient code for processors with a low issue rate, whereas hyperblock scheduling produces more
+performant code for processors with a high issue
+rate~\cite[mahlke92_effec_compil_suppor_predic_execut_using_hyper,aiken16_trace_sched].
+
+A hardware back end is an ideal target for hyperblock scheduling, as the issue rate is practically
+infinite. This paper describes the implementation of a hyperblock instruction scheduler in CompCert
+so that it can benefit existing CompCert back ends, as well as support more general targets such as
+scheduling instructions for custom hardware.
\subsection[key-points]{Key Points}
@@ -61,9 +61,36 @@ the key points of this paper are the following:
\section[sec:scheduling]{Implementation of Hyperblocks in CompCert}
\index{hyperblock}This section describes the structure of hyperblocks in
-Section~\goto{2.1}[scheduling:hyperblocks]. Then, the structure of two extra intermediate languages
-that were added to CompCert to implement hyperblocks are also shown in
-Section~\goto{2.2}[sec:rtlblockdef].
+\in{Section}[scheduling:hyperblocks]. Then, the structure of two extra intermediate languages that
+were added to CompCert to implement hyperblocks are also shown in \in{Section}[sec:rtlblockdef].
+
+\startplacemarginfigure[reference={fig:compcert_interm},title={New intermediate languages introduced into
+ CompCert.}]
+ \hbox{\starttikzpicture[shorten >=1pt,>=stealth]
+ \node at (-3, 0) (dotsin) {$\cdots$};
+ \node at (10, 0) (dotsout) {$\cdots$};
+ \node[draw] at (-1, 0) (rtl) {\tt RTL};
+ \node[draw] at (2, 0) (rtlblock) {\tt RTLBlock};
+ \node[draw] at (2, -2) (abstrblock) {\tt Abstr};
+ \node[draw] at (6, 0) (rtlpar) {\tt RTLPar};
+ \node[draw] at (6, -2) (abstrpar) {\tt Abstr};
+ \node[draw] at (8, 0) (htl) {\tt HTL};
+
+ \draw[->] (rtl) -- node[above,midway,align=center,font=\small]
+ {basic-block \\[-0.3em] creation} (rtlblock);
+ \draw[->] (rtlblock) -- node[above,midway,font=\small] {scheduling} (rtlpar);
+ \draw[->] (rtlpar) -- (htl);
+ \draw[->,dashed] (rtlblock) -- (abstrblock);
+ \draw[->,dashed] (rtlpar) -- (abstrpar);
+ \draw[dashed,shorten >=0pt] (abstrblock) -- node[above,midway] {$\sim$} (abstrpar);
+ \draw[->] (rtlblock) to [out=130,in=50,loop,looseness=10]
+ node[above,midway,font=\small] {if-conversion} (rtlblock);
+ \draw[->] (rtlpar) to [out=130,in=50,loop,looseness=10]
+ node[above,midway,align=center,font=\small] { operation \\[-0.3em] pipelining} (rtlpar);
+ \draw[->] (dotsin) -- (rtl);
+ \draw[->] (htl) -- (dotsout);
+ \stoptikzpicture}
+\stopplacemarginfigure
\subsection[scheduling:hyperblocks]{Hyperblocks as a Generalisation of Basic Blocks}
@@ -75,48 +102,48 @@ instructions to eliminate of any delay slots caused by the CPU pipeline.
However, due to control-flow not being allowed in basic blocks, the number of instructions that can
be scheduled at any one time is limited. The boundaries to other basic blocks act as hard boundary
-to the scheduling algorithm. hyperblocks~ allow instructions to be predicated, thereby introducing
-some control-flow information into the blocks, which can also be taken into account by the
-scheduler. For example, any data dependency between instructions that have mutually exclusive
-predicates can be removed, as these instructions will never be activate at the same time.
+to the scheduling
+algorithm. Hyperblocks~\cite[mahlke92_effec_compil_suppor_predic_execut_using_hyper] allow
+instructions to be predicated, thereby introducing some control-flow information into the blocks,
+which can also be taken into account by the scheduler. For example, any data dependency between
+instructions that have mutually exclusive predicates can be removed, as these instructions will
+never be activate at the same time.
\subsection[sec:rtlblockdef]{RTLBlock and RTLPar Intermediate Language Definition}
-\lindex{RTLBlock}\lindex{RTLPar}Figure~\goto{{[}fig:compcert_interm{]}}[fig:compcert_interm] shows
-the intermediate languages introduced to implement hyperblocks in CompCert. This consists of new
-RTLBlock and RTLPar intermediate languages, which implement the sequential and parallel semantics of
-basic blocks respectively. The semantics of RTLBlock and RTLPar are based on the CompCert RTL
-intermediate language. However, instead of mapping from states to instructions, RTLBlock maps from
-states to hyperblocks, and RTLPar maps from states to parallel hyperblocks, which will be described
-in the next sections.
+\lindex{RTLBlock}\lindex{RTLPar}\in{Figure}[fig:compcert_interm] shows the intermediate languages
+introduced to implement hyperblocks in CompCert. This consists of new RTLBlock and RTLPar
+intermediate languages, which implement the sequential and parallel semantics of basic blocks
+respectively. The semantics of RTLBlock and RTLPar are based on the CompCert RTL intermediate
+language. However, instead of mapping from states to instructions, RTLBlock maps from states to
+hyperblocks, and RTLPar maps from states to parallel hyperblocks, which will be described in the
+next sections.
\placeformula \startformula \startmathalignment
-\NC i\ \ \colon\colon= \NC \ \ \mono{RBnop} \NR
-\NC \NC |\ \ \mono{RBop}\ p?\ \mathit{op}\ \vec{r}\ d \NR
-\NC \NC |\ \ \mono{RBload}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ d \NR
-\NC \NC |\ \ \mono{RBstore}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ s \NR
-\NC \NC |\ \ \mono{RBsetpred}\ p?\ c\ \vec{r}\ d \NR
+\NC i\ \ \colon\colon= \NC \ \ \text{\tt RBnop} \NR
+\NC \NC |\ \ \text{\tt RBop}\ p?\ \mathit{op}\ \vec{r}\ d \NR
+\NC \NC |\ \ \text{\tt RBload}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ d \NR
+\NC \NC |\ \ \text{\tt RBstore}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ s \NR
+\NC \NC |\ \ \text{\tt RBsetpred}\ p?\ c\ \vec{r}\ d \NR
\stopmathalignment \stopformula
\placeformula \startformula \startmathalignment
-\NC i_{\mathit{cf}}\ \ \colon\colon= \NC \ \ \mono{RBcall}\ \mathit{sig}\ f\ \vec{r}\ d\ n \NR
-\NC \NC |\ \ \mono{RBtailcall}\ \mathit{sig}\ f\ \vec{r} \NR
-\NC \NC |\ \ \mono{RBbuiltin}\ f_{\mathit{ext}}\ \vec{r}\ r\ n \NR
-\NC \NC |\ \ \mono{RBcond}\ c\ \vec{r}\ n_{1}\ n_{2} \NR
-\NC \NC |\ \ \mono{RBjumptable}\ r\ \vec{n} \NR
-\NC \NC |\ \ \mono{RBreturn}\ r? \NR
-\NC \NC |\ \ \mono{RBgoto}\ n \NR
-\NC \NC |\ \ \mono{RBpred\_{cf}}\ P\ i_{\mathit{cf}_{1}}\ i_{\mathit{cf}_{2}} \NR
+\NC i_{\mathit{cf}}\ \ \colon\colon= \NC \ \ \text{\tt RBcall}\ \mathit{sig}\ f\ \vec{r}\ d\ n \NR
+\NC \NC |\ \ \text{\tt RBtailcall}\ \mathit{sig}\ f\ \vec{r} \NR
+\NC \NC |\ \ \text{\tt RBbuiltin}\ f_{\mathit{ext}}\ \vec{r}\ r\ n \NR
+\NC \NC |\ \ \text{\tt RBcond}\ c\ \vec{r}\ n_{1}\ n_{2} \NR
+\NC \NC |\ \ \text{\tt RBjumptable}\ r\ \vec{n} \NR
+\NC \NC |\ \ \text{\tt RBreturn}\ r? \NR
+\NC \NC |\ \ \text{\tt RBgoto}\ n \NR
+\NC \NC |\ \ \text{\tt RBpred\_{cf}}\ P\ i_{\mathit{cf}_{1}}\ i_{\mathit{cf}_{2}} \NR
\stopmathalignment \stopformula
RTLBlock instructions are split into two types of instructions, standard instructions and
control-flow instructions. The standard instructions are the instructions that can be placed into
hyperblocks, whereas control-flow instructions are the instructions that can end hyperblocks. The
-standard instructions are shown in
-Figure~\goto{{[}fig:standard_instruction{]}}[fig:standard_instruction], whereas the control-flow
-instructions are shown in
-Figure~\goto{{[}fig:control_flow_instruction{]}}[fig:control_flow_instruction]. Most instructions
-are quite similar to their RTL counterparts, however, there are some instructions that have been
+standard instructions are shown in \in{Figure}[fig:standard_instruction], whereas the control-flow
+instructions are shown in \in{Figure}[fig:control_flow_instruction]. Most instructions are quite
+similar to their RTL counterparts, however, there are some instructions that have been
added. \type{RBsetpred} is a standard instruction which sets a predicate equal to an evaluated
condition. This instruction is used during if-conversion to set the predicate to the value of the
condition in the conditional statement instruction. To support proper predicated instructions, each
@@ -124,16 +151,19 @@ instruction therefore also contains an optional predicate which has been set bef
produces the hyperblock. In additon to that, there is also an extra control-flow instruction called
\type{RBpred_cf}, which can branch on a predicate an nests more control-flow instructions inside of
it. This is also necessary for if-conversion, when converting an already converted conditional
-statement, as depending on the predicate, a different control-flow instruction may be
-necessary.
+statement, as depending on the predicate, a different control-flow instruction may be necessary.
+
+\placeformula[fig:hb_def]\startformula\startalign[align={1:left}]
+\NC \blockbb \qquad \eqdef \qquad (\text{\tt list}\ i) \times i_{\mathit{cf}} \NR
+\NC \parbb \qquad \eqdef \qquad (\text{\tt list}\ \text{\tt list}\ \text{\tt list}\ i) \times i_{\mathit{cf}}\NR
+\stopalign\stopformula
These instructions are use in RTLBlock as well as in RTLPar. The main difference between these two
languages is how these instructions are arranged within the hyperblock and the execution semantics
-of the hyperblock in the languages. Let $\mathit{hb}_{b}$ be the definition of a hyperblock for
-RTLBlock, and let $\mathit{hb}_{p}$ be the definition of a hyperblock for RTLPar, then
-$\mathit{hb}_{b}$ and $\mathit{hb}_{p}$ be defined as in
-Figure~\goto{{[}fig:hb_def{]}}[fig:hb_def]. The Figure shows the different nesting levels of the
-basic blocks in RTLBlock as well as RTLPar, and where the parallel semantics of RTLPar come into
+of the hyperblock in the languages. Let $\blockbb$ be the definition of a hyperblock for RTLBlock,
+and let $\parbb$ be the definition of a hyperblock for RTLPar, then $\blockbb$ and $\parbb$ be
+defined as in \in{Equation}[fig:hb_def]. The Figure shows the different nesting levels of the basic
+blocks in RTLBlock as well as RTLPar, and where the parallel semantics of RTLPar come into
play. RTLBlock is made of a list of instructions and a control-flow instruction that ends the
hyperblock. Each instruction in RTLBlock is executed sequentially. RTLPar is made of three separate
lists. The outer list behaves like the list in RTLBlock, and executes each list inside of it
@@ -157,27 +187,25 @@ hyperblocks and rearranges their instructions to maximise parallelism based on t
dependencies. It then arranges the instructions in RTLPar by putting independent instructions into
the same parallel block. Scheduling is an optimisation that is well suited to translation
validation, as the algorithm itself can be quite complex, whereas the output is normally relatively
-easy to check for equivalence with the input.
-Figure~\goto{{[}fig:compcert_interm{]}}[fig:compcert_interm] shows that the scheduling step comes
-right after the if-conversion step which originally creates the hyperblocks.
-
-Figure~\goto{{[}fig:op_chain{]}}[fig:op_chain] shows how the scheduling step transforms RTLBlock
-into RTLPar. The RTLBlock hyperblock being scheduled is shown in
-Figure~\goto{{[}fig:op_chain_a{]}}[fig:op_chain_a], which contains five predicated operations,
-comprising two additions and three multiplications. The data dependencies of the instructions in the
-hyperblock are shown in Figure~\goto{{[}fig:op_chain_b{]}}[fig:op_chain_b]. Curiously, even though
+easy to check for equivalence with the input. \in{Figure}[fig:compcert_interm] shows that the
+scheduling step comes right after the if-conversion step which originally creates the hyperblocks.
+
+\in{Figure}[fig:op_chain] shows how the scheduling step transforms RTLBlock into RTLPar. The
+RTLBlock hyperblock being scheduled is shown in \in{Figure}[fig:op_chain_a], which contains five
+predicated operations, comprising two additions and three multiplications. The data dependencies of
+the instructions in the hyperblock are shown in \in{Figure}[fig:op_chain_b]. Curiously, even though
operations and are normally dependent on each other due to a write-after-write conflict, but because
the predicates are independent the write-after-write conflict can effectively be removed by the
scheduler.
The scheduler transforms the RTLBlock hyperblock into the RTLPar hyperblock shown in
-Figure~\goto{{[}fig:op_chain_c{]}}[fig:op_chain_c]. Even though the addition in is dependent on ,
-they can still be put into the same cycle as the additions do not take as long to complete as the
-multiplications. This optimisation is called operation chaining. Then, the multiplication in can
-also be placed in the same clock cycle as it does not have any data dependencies. Then, in the next
-clock cycle, either the multiplication in can take place, or the multiplication in will take place,
-meaning these two multiplications can also be placed in the same clock cycle. This gives the final
-schedule that is shown in Figure~\goto{{[}fig:op_chain_d{]}}[fig:op_chain_d].
+\in{Figure}[fig:op_chain_c]. Even though the addition in is dependent on , they can still be put
+into the same cycle as the additions do not take as long to complete as the multiplications. This
+optimisation is called operation chaining. Then, the multiplication in can also be placed in the
+same clock cycle as it does not have any data dependencies. Then, in the next clock cycle, either
+the multiplication in can take place, or the multiplication in will take place, meaning these two
+multiplications can also be placed in the same clock cycle. This gives the final schedule that is
+shown in \in{Figure}[fig:op_chain_d].
\section[abstr_interp]{Abstract Interpretation of Hyperblocks}
@@ -225,24 +253,25 @@ primitive is multiplication of two predicated types, which is implemented as per
multiplication between the predicated types in the two lists, anding the two predicates and joining
the two types of each list using a function.
-%\startformula \label{eq:1}
-% P_{1} \otimes_{f} P_{2} \equiv \mono{map } (\lambda ((p_{1}, e_{1}), (p_{2}, e_{2})) . (p_{1} \land p_{2}, f\ e_{1}\ e_{2})) P_{1} \times P_{2} \stopformula
+\placeformula[eq:1]\startformula
+ P_{1} \otimes_{f} P_{2} \equiv \text{\tt map } (\lambda ((p_{1}, e_{1}), (p_{2}, e_{2})) . (p_{1}
+ \land p_{2}, f\ e_{1}\ e_{2})) P_{1} \times P_{2} \stopformula
In addition to that, another primitive that is needed is the following append operation, which will
negate the combination of all predicates in the second predicated type, and it to the first
predicated type and append the first predicated type to the second:
-%\startformula \label{eq:2}
-% \mu(p, P) \equiv \mono{map } (\lambda (p', e') . (p \land p', e'))\ P \stopformula
+\placeformula[eq:2]\startformula
+ \mu(p, P) \equiv \text{\tt map } (\lambda (p', e') . (p \land p', e'))\ P \stopformula
-%\startformula \label{eq:3}
-% P_{1} \oplus_{p} P_{2} \equiv \mu(\neg p, P_{1}) \mathbin{++} \mu(p, P_{2}) \stopformula
+\placeformula[eq:3]\startformula
+ P_{1} \oplus_{p} P_{2} \equiv \mu(\neg p, P_{1}) + \mu(p, P_{2}) \stopformula
\subsection[example-of-translation]{Example of translation}
%\startformula \begin{aligned}
% \label{eq:4}
-% &\mono{r1} =
+% &\text{\tt r1} =
% \begin{cases}
% \mono{r1}^{0} + \mono{r4}^{0} + \mono{r4}^{0}, \quad &\mono{p1} \\
% \mono{r1}^{0}, \quad &\mono{!p1} \\
@@ -257,20 +286,18 @@ predicated type and append the first predicated type to the second:
% \end{cases}
% \end{aligned} \stopformula
-Using the example shown in Figure~\goto{{[}fig:op_chain{]}}[fig:op_chain], the RTLBlock hyperblock
-shown in Figure~\goto{{[}fig:op_chain_a{]}}[fig:op_chain_a] is scheduled into the hyperblock RTLPar
-shown in Figure~\goto{{[}fig:op_chain_c{]}}[fig:op_chain_c]. The first step is to translate the
-input and output of the scheduler into the Abstr intermediate language by calculating the symbolic
-values that will be stored in each of the registers. Symbolically evaluating the RTLBlock hyperblock
-results in the expressions shown in
-Figure~\goto{{[}fig:symbolic_expressions{]}}[fig:symbolic_expressions] for registers \type{r1},
-\type{r2} and \type{r3}, where the state of the register \type{r1} at the start of the hyperblock is
-denoted as $\mono{r1}^{0}$.
+Using the example shown in \in{Figure}[fig:op_chain], the RTLBlock hyperblock shown in
+\in{Figure}[fig:op_chain_a] is scheduled into the hyperblock RTLPar shown in
+\in{Figure}[fig:op_chain_c]. The first step is to translate the input and output of the scheduler
+into the Abstr intermediate language by calculating the symbolic values that will be stored in each
+of the registers. Symbolically evaluating the RTLBlock hyperblock results in the expressions shown
+in \in{Figure}[fig:symbolic_expressions] for registers \type{r1}, \type{r2} and \type{r3}, where the
+state of the register \type{r1} at the start of the hyperblock is denoted as $\text{\tt r1}^{0}$.
This symbolic expression can be generated by sequentially going through the list of predicated
-expressions and applying the update function defined in Section~\goto{3.1}[abstr_language]. The
-resulting predicated expressions is guaranteed to have predicates which are mutually exclusive,
-meaning if the predicate evaluates to true, all other predicates must evaluate to false.
+expressions and applying the update function defined in \in{Section}[abstr_language]. The resulting
+predicated expressions is guaranteed to have predicates which are mutually exclusive, meaning if the
+predicate evaluates to true, all other predicates must evaluate to false.
\subsection[linear-flat-predicated-expressions]{Linear (Flat) Predicated Expressions}
@@ -311,7 +338,7 @@ is because predicated instructions can be executed in many different orders, and
used to calculate dependence information and therefore also determine the order of operations.
Instead, comparing predicates can be done by checking logical equivalence of the predicates using a
-formally verified \SAT solver. This ensures that the predicates will always evaluate to the same
+formally verified \SAT\ solver. This ensures that the predicates will always evaluate to the same
value, thereby making it a fair comparison.
\subsection[verified_sat]{Verified Decidable DPLL SAT Solver}
@@ -377,28 +404,27 @@ of the scheduling transformation. The SAT query can therefore be broken down int
direct comparison that is more useful for the proof itself. The steps to perform the more fine
grained comparison are the following:
-%\startenumerate[n]
-%\item
-% Hash all of the expressions into a unique literal.
-%\item
-% Create a map from expression literals to their corresponding
-% predicate, thereby having a unique predicate for each expressions. If
-% there are duplicates in the list that forms the map, the predicates
-% are combined using the or operation.
-%\item
-% Iterate through the expressions in both maps and compare the
-% predicates using the SAT solver. If an expression is not present in
-% one of the maps, then it's predicate should be equivalent to $\perp$.
-%\stopenumerate
+\startitemize[n]
+\item
+ Hash all of the expressions into a unique literal.
+\item
+ Create a map from expression literals to their corresponding predicate, thereby having a unique
+ predicate for each expressions. If there are duplicates in the list that forms the map, the
+ predicates are combined using the or operation.
+\item
+ Iterate through the expressions in both maps and compare the predicates using the SAT solver. If
+ an expression is not present in one of the maps, then it's predicate should be equivalent to
+ $\perp$.
+\stopitemize
This comparison is logically equivalent to performing the large SAT query, however, it maps better
to the proof because it is comparing the predicates of the same expressions with each other.
\subsection[proof-of-equivalence-between-passes]{Proof of equivalence between passes}
-Figure~\goto{{[}fig:compcert_interm{]}}[fig:compcert_interm] shows the four different passes that
-were added to CompCert to form hyperblocks. This section will cover the proofs for each of the
-translations, focusing mainly on the proof of translation of the scheduling pass.
+\in{Figure}[fig:compcert_interm] shows the four different passes that were added to CompCert to form
+hyperblocks. This section will cover the proofs for each of the translations, focusing mainly on
+the proof of translation of the scheduling pass.
\subsubsection[proof-of-correctness-of-the-if-conversion-pass]{Proof of Correctness of the
If-Conversion Pass}
@@ -410,9 +436,9 @@ in the same language.
The scheduling pass is formally verified using translation validation, using the Abstr language as a
point of comparison between RTLBlock and RTLPar. Using the algorithm defined in
-Section~\goto{3}[abstr_interp], the formally verified SAT solver described in
-Section~\goto{4.2}[verified_sat] can be used prove that if the two predicated expression lists are
-equivalent, that they will always evaluate to the same value.
+\in{Section}[abstr_interp], the formally verified SAT solver described in \in{Section}[verified_sat]
+can be used prove that if the two predicated expression lists are equivalent, that they will always
+evaluate to the same value.
\section[implementation-details-of-static-sdc-scheduling]{\SDC\ Scheduling Implementation Details}
@@ -452,4 +478,9 @@ This material is based upon work supported by the under Grant No.~ and Grant No.
findings, and conclusions or recommendations expressed in this material are those of the author and
do not necessarily reflect the views of the National Science Foundation.
+\startmode[section]
+ \section{Bibliography}
+ \placelistofpublications
+\stopmode
+
\stopcomponent
diff --git a/fonts_env.tex b/fonts_env.tex
index 1ac7b24..d5cb7cd 100644
--- a/fonts_env.tex
+++ b/fonts_env.tex
@@ -15,11 +15,11 @@
\definefontsynonym[MonoBoldItalic] [Iosevka-BoldItalic] [features=default]
\stoptypescript
-\starttypescript [ebgaramondlato]
- \definetypeface [ebgaramondlato] [rm] [serif] [palatino] [default]
- \definetypeface [ebgaramondlato] [ss] [sans] [lato] [default]
- \definetypeface [ebgaramondlato] [tt] [mono] [modern] [default]
- \definetypeface [ebgaramondlato] [mm] [math] [palatino] [default]
+\starttypescript [lsrfont]
+ \definetypeface [lsrfont] [rm] [serif] [palatino] [default]
+ \definetypeface [lsrfont] [ss] [sans] [heros] [default]
+ \definetypeface [lsrfont] [tt] [mono] [modern] [default]
+ \definetypeface [lsrfont] [mm] [math] [palatino] [default]
\stoptypescript
\stopenvironment
diff --git a/lsr_env.tex b/lsr_env.tex
index c20063e..cbedab1 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -29,7 +29,7 @@
\setuppapersize[A4][A4]
\definefontfeature[default][default][protrusion=quality,expansion=quality]
\setupalign[hz,hanging,lesshyphenation,verytolerant]
-\setupbodyfont[ebgaramondlato,11pt]
+\setupbodyfont[lsrfont,11pt]
%\setupalign[hz,hanging,nothyphenated]
\setupinterlinespace[big]
@@ -54,7 +54,7 @@
]
\setuphead[chapter][
- style={\bfd},
+ style={\bfd\ss},
header=empty,
align=flushright,
numbercommand=\marginhead,
@@ -67,7 +67,6 @@
\setupheads[chapter][
after={\blank[2*big]},
before={\blank[big,force]},
- style={\bfd},
header=empty,
align=flushleft,
]
@@ -81,7 +80,6 @@
\setupheads[chapter][
after={\blank[2*big]},
before={\blank[big,force]},
- style={\bfd},
header=empty,
align=flushleft,
]
@@ -139,9 +137,9 @@
\define[1]\marginhead{\margintitle[location=right]{\switchtobodyfont[30pt] #1}}
-\setuphead[section][style={\bfb}]
-\setuphead[subsection][style={\bfa}]
-\setuphead[subsubsection][style={\bf},after={\blank[0.2cm]}]
+\setuphead[section][style={\bfb\ss}]
+\setuphead[subsection][style={\bfa\ss}]
+\setuphead[subsubsection][style={\bf\ss},after={\blank[0.2cm]}]
\setuplabeltext[chapter=]
% \setupheader[text][style=smallcaps,after=\hrule]
@@ -175,21 +173,6 @@
% @see http://wiki.contextgarden.net/Indentation
% Indent all paragraph after all section headers.
\setupindenting[yes,medium]
-%\setupheads[section, subsection][
-% indentnext=yes,
-% numberwidth=1.27cm,
-% style=bold,
-% before={\blank[3*line]},
-% after={\blank[1*line]},
-%]
-%
-%\setupheads[subsubsection][
-% indentnext=yes,
-% numberwidth=1.27cm,
-% style=bold,
-% before={\blank[1*line]},
-% after={\blank[1*line]},
-%]
% ==========================================================================
% Table of Contents
@@ -235,7 +218,8 @@
numbercommand=\groupedcommand{(}{)},
numberconversion=a,
prefix=no,
- way=bytext
+ way=bytext,
+ style=\rmx,
]
\setuplabeltext[subfigure=]
@@ -358,7 +342,17 @@
% ==========================================================================
\usemodule[tikz]
-\usetikzlibrary{shapes,calc,arrows.meta}
+\usetikzlibrary{
+ arrows,
+ arrows.meta,
+ automata,
+ calc,
+ decorations.pathreplacing,
+ patterns,
+ patterns.meta,
+ petri,
+ shapes,
+}
\definecolor[compcert][x=BEBADA]
\definecolor[formalhls][x=8DD3C7]
@@ -476,4 +470,12 @@
\define[1]\oindex{\index{optimisation+#1}}
\define[1]\pindex{\index{proof+#1}}
+% ==========================================================================
+% Macros
+% ==========================================================================
+
+\define\eqdef{{\strut\hbox to 0pt{\raisebox{0.5\baselineskip}\hbox{\rmx def}\hss}}=}
+\define\blockbb{\mathcal{B}_{\rm b}}
+\define\parbb{\mathcal{B}_{\rm p}}
+
\stopenvironment
diff --git a/lsr_refs.bib b/lsr_refs.bib
index 1833535..f9cf0d3 100644
--- a/lsr_refs.bib
+++ b/lsr_refs.bib
@@ -1,1296 +1,1194 @@
@article{05_ieee_stand_veril_regis_trans_level_synth,
- title = {{IEEE} Standard for {Verilog} Register Transfer Level Synthesis},
- journal = {IEC 62142-2005 First edition 2005-06 IEEE Std 1364.1},
- volume = {},
- number = {},
- pages = {1-116},
- year = {2005},
- doi = {10.1109/IEEESTD.2005.339572},
url = {https://doi.org/10.1109/IEEESTD.2005.339572},
- ISSN = {},
- key = {IEEE Std 1364.1},
- month = {},
- type = {Standard}
+ doi = {10.1109/IEEESTD.2005.339572},
+ journaltitle = {IEC 62142-2005 First edition 2005-06 IEEE Std 1364.1},
+ pages = {1--116},
+ title = {{IEEE} Standard for {Verilog} Register Transfer Level Synthesis},
+ type = {Standard},
+ year = {2005}
}
@article{06_ieee_stand_veril_hardw_descr_languag,
- author = {},
- title = {{IEEE} Standard for Verilog Hardware Description Language},
- journal = {IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)},
- volume = {},
- number = {},
- pages = {1-590},
- year = {2006},
- doi = {10.1109/IEEESTD.2006.99495},
url = {https://doi.org/10.1109/IEEESTD.2006.99495},
- ISSN = {},
- key = {IEEE Std 1364},
- month = {April},
- type = {Standard}
-}
-
-@InProceedings{armand11_modul_integ_sat_smt_solver,
- keywords = {SAT, verification, coq},
+ doi = {10.1109/IEEESTD.2006.99495},
+ journaltitle = {IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)},
+ month = 4,
+ pages = {1--590},
+ title = {{IEEE} Standard for Verilog Hardware Description Language},
+ type = {Standard},
+ year = {2006}
+}
+
+@inbook{aiken16_trace_sched,
+ abstract = {Since its introduction by Joseph A. Fisher in 1979, trace scheduling has influenced much of the work on compile-time ILP. Initially developed for use in microcode compaction, trace scheduling quickly became the main technique for machine-level compile-time parallelism exploitation. Trace scheduling has been used since the 1980s in many state-of-the-art compilers (e.g., Intel, Fujitsu, HP).},
+ author = {Aiken, Alex and Banerjee, Utpal and Kejariwal, Arun and Nicolau, Alexandru},
+ location = {Boston, MA},
+ publisher = {Springer US},
+ url = {https://doi.org/10.1007/978-1-4899-7797-7_4},
+ booktitle = {Instruction Level Parallelism},
+ doi = {10.1007/978-1-4899-7797-7_4},
+ isbn = {978-1-4899-7797-7},
+ keywords = {trace scheduling,static scheduling},
+ pages = {79--116},
+ title = {Trace Scheduling},
+ year = {2016}
+}
+
+@inproceedings{armand11_modul_integ_sat_smt_solver,
+ abstract = {We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.},
author = {Armand, Michael and Faure, Germain and Grégoire, Benjamin and Keller, Chantal and Théry, Laurent and Werner, Benjamin},
- editor = "Jouannaud, Jean-Pierre
-and Shao, Zhong",
- title = "A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses",
- booktitle = "Certified Programs and Proofs",
- year = "2011",
- publisher = "Springer Berlin Heidelberg",
- address = "Berlin, Heidelberg",
- pages = "135--150",
- abstract = "We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.",
- isbn = "978-3-642-25379-9"
+ editor = {Jouannaud, Jean-Pierre and Shao, Zhong},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer Berlin Heidelberg},
+ booktitle = {Certified Programs and Proofs},
+ isbn = {978-3-642-25379-9},
+ keywords = {SAT,verification,coq},
+ pages = {135--150},
+ title = {A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses},
+ year = {2011}
}
@article{aubury96_handel_c_languag_refer_guide,
author = {Aubury, Matthew and Page, Ian and Randall, Geoff and Saul, Jonathan and Watts, Robin},
+ journaltitle = {Computing Laboratory. Oxford University, UK},
title = {Handel-C Language Reference Guide},
- tags = {hls},
- journal = {Computing Laboratory. Oxford University, UK},
- year = 1996
+ year = {1996}
}
@inproceedings{bachrach12_chisel,
- title = {{Chisel: Constructing hardware in a Scala embedded language}},
- author = {Bachrach, Jonathan and Vo, Huy and Richards, Brian and Lee, Yunsup and Waterman, Andrew and Avi{\v{z}}ienis, Rimas and Wawrzynek, John and Asanovi{\'c}, Krste},
+ author = {Bachrach, Jonathan and Vo, Huy and Richards, Brian and Lee, Yunsup and Waterman, Andrew and Avižienis, Rimas and Wawrzynek, John and Asanović, Krste},
+ organization = {IEEE},
booktitle = {DAC Design Automation Conference 2012},
+ doi = {https://doi.org/10.1145/2228360.2228584},
pages = {1212--1221},
- year = {2012},
- organization = {IEEE},
- doi = {https://doi.org/10.1145/2228360.2228584}
+ title = {{Chisel: Constructing hardware in a Scala embedded language}},
+ year = {2012}
}
@article{banerjee14_verif_code_motion_techn_using_value_propag,
author = {{Banerjee}, K. and {Karfa}, C. and {Sarkar}, D. and {Mandal}, C.},
- title = {Verification of Code Motion Techniques Using Value
- Propagation},
- journal = {IEEE Transactions on Computer-Aided Design of Integrated
- Circuits and Systems},
- volume = 33,
- number = 8,
- pages = {1180-1193},
- year = 2014,
doi = {10.1109/TCAD.2014.2314392},
- ISSN = {1937-4151},
- month = {Aug}
+ issn = {1937-4151},
+ journaltitle = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+ month = 8,
+ number = {8},
+ pages = {1180--1193},
+ title = {Verification of Code Motion Techniques Using Value Propagation},
+ volume = {33},
+ year = {2014}
}
@article{barthe14_formal_verif_ssa_based_middl_end_compc,
- year = {2014},
abstract = {CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it has remained an open problem to verify formally an SSA-based compiler. We report on a formally verified, SSA-based middle-end for CompCert. In addition to providing a formally verified SSA-based middle-end, we address two problems raised by Leroy in [2009]: giving an intuitive formal semantics to SSA, and leveraging its global properties to reason locally about program optimizations.},
author = {Barthe, Gilles and Demange, Delphine and Pichardie, David},
location = {New York, NY, USA},
publisher = {Association for Computing Machinery},
url = {https://doi.org/10.1145/2579080},
- date = {2014-03},
doi = {10.1145/2579080},
issn = {0164-0925},
journaltitle = {ACM Trans. Program. Lang. Syst.},
keywords = {CompCertSSA,CompCert,SSA,coq,verification,compiler optimisation},
+ month = 3,
number = {1},
title = {Formal Verification of an SSA-Based Middle-End for CompCert},
- volume = {36}
+ volume = {36},
+ year = {2014}
}
@book{bertot04_inter_theor_provin_progr_devel,
- author = {Bertot, Yves and Cast{\'{e}}ran, Pierre},
- title = {Interactive Theorem Proving and Program Development},
- year = 2004,
+ author = {Bertot, Yves and Castéran, Pierre},
publisher = {Springer Berlin Heidelberg},
url = {https://doi.org/10.1007/978-3-662-07964-5},
- doi = {10.1007/978-3-662-07964-5}
+ doi = {10.1007/978-3-662-07964-5},
+ title = {Interactive Theorem Proving and Program Development},
+ year = {2004}
}
@inproceedings{bertot06_struc_approac_provin_compil_optim,
- author = "Bertot, Yves and Gr{\'e}goire, Benjamin and Leroy, Xavier",
- title = "A Structured Approach to Proving Compiler Optimizations
- Based on Dataflow Analysis",
- booktitle = "Types for Proofs and Programs",
- year = 2006,
- pages = "66--81",
- address = "Berlin, Heidelberg",
- editor = "Filli{\^a}tre, Jean-Christophe and Paulin-Mohring,
- Christine and Werner, Benjamin",
- isbn = "978-3-540-31429-5",
- publisher = "Springer"
+ author = {Bertot, Yves and Grégoire, Benjamin and Leroy, Xavier},
+ editor = {Filliâtre, Jean-Christophe and Paulin-Mohring, Christine and Werner, Benjamin},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer},
+ booktitle = {Types for Proofs and Programs},
+ isbn = {978-3-540-31429-5},
+ pages = {66--81},
+ title = {A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis},
+ year = {2006}
}
@article{besson18_compc,
- doi = {10.1007/s10817-018-9496-y},
- url = {https://doi.org/10.1007/s10817-018-9496-y},
- year = {2018},
- month = nov,
+ author = {Besson, Frédéric and Blazy, Sandrine and Wilke, Pierre},
publisher = {Springer Science and Business Media {LLC}},
- volume = {63},
+ url = {https://doi.org/10.1007/s10817-018-9496-y},
+ doi = {10.1007/s10817-018-9496-y},
+ journaltitle = {Journal of Automated Reasoning},
+ month = 11,
number = {2},
pages = {369--392},
- author = {Fr{\'{e}}d{\'{e}}ric Besson and Sandrine Blazy and Pierre Wilke},
title = {{CompCertS}: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics},
- journal = {Journal of Automated Reasoning}
+ volume = {63},
+ year = {2018}
}
@inproceedings{blazy05_formal_verif_memor_model_c,
- author = "Blazy, Sandrine and Leroy, Xavier",
- title = "Formal Verification of a Memory Model for {C}-Like Imperative
- Languages",
- tags = {verification},
- booktitle = "Formal Methods and Software Engineering",
- year = 2005,
- pages = "280--299",
- address = "Berlin, Heidelberg",
- editor = "Lau, Kung-Kiu and Banach, Richard",
- isbn = "978-3-540-32250-4",
- publisher = "Springer Berlin Heidelberg",
- doi = {0.1007/11576280_20}
+ author = {Blazy, Sandrine and Leroy, Xavier},
+ editor = {Lau, Kung-Kiu and Banach, Richard},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer Berlin Heidelberg},
+ booktitle = {Formal Methods and Software Engineering},
+ doi = {0.1007/11576280_20},
+ isbn = {978-3-540-32250-4},
+ pages = {280--299},
+ title = {Formal Verification of a Memory Model for {C}-Like Imperative Languages},
+ year = {2005}
}
@inproceedings{bourgeat20_essen_blues,
- author = {Bourgeat, Thomas and Pit-Claudel, Cl\'{e}ment and Chlipala, Adam and Arvind},
- title = {The Essence of {Bluespec}: A Core Language for Rule-Based Hardware Design},
- booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
- and Implementation},
- year = 2020,
- pages = {243-257},
- doi = {10.1145/3385412.3385965},
- url = {https://doi.org/10.1145/3385412.3385965},
- address = {New York, NY, USA},
- isbn = 9781450376136,
- keywords = {Hardware Description Language, Compiler Correctness, Semantics},
+ author = {Bourgeat, Thomas and Pit-Claudel, Clément and Chlipala, Adam and Arvind},
location = {London, UK},
- numpages = 15,
publisher = {ACM},
- series = {PLDI 2020}
+ url = {https://doi.org/10.1145/3385412.3385965},
+ booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ doi = {10.1145/3385412.3385965},
+ isbn = {9781450376136},
+ keywords = {Hardware Description Language,Compiler Correctness,Semantics},
+ pages = {243--257},
+ series = {PLDI 2020},
+ title = {The Essence of {Bluespec}: A Core Language for Rule-Based Hardware Design},
+ year = {2020}
}
-@InProceedings{bouton09,
+@inproceedings{bouton09,
+ abstract = {This article describes the first public version of the satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.},
author = {Bouton, Thomas and Caminha B. de Oliveira, Diego and Déharbe, David and Fontaine, Pascal},
- editor = "Schmidt, Renate A.",
- title = "veriT: An Open, Trustable and Efficient SMT-Solver",
- booktitle = "Automated Deduction -- CADE-22",
- year = "2009",
- publisher = "Springer Berlin Heidelberg",
- address = "Berlin, Heidelberg",
- pages = "151--156",
- abstract = "This article describes the first public version of the satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.",
- isbn = "978-3-642-02959-2"
+ editor = {Schmidt, Renate A.},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer Berlin Heidelberg},
+ booktitle = {Automated Deduction -- CADE-22},
+ isbn = {978-3-642-02959-2},
+ pages = {151--156},
+ title = {veriT: An Open, Trustable and Efficient SMT-Solver},
+ year = {2009}
}
@article{bowen98_handel_c_languag_refer_manual,
author = {Bowen, Matthew},
+ journaltitle = {Embedded Solutions Ltd},
title = {Handel-C Language Reference Manual},
- journal = {Embedded Solutions Ltd},
volume = {2},
year = {1998}
}
@inproceedings{canis11_legup,
- author = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and
- Kammoona, Ahmed and Anderson, Jason Helge and Brown, Stephen Dean and Czajkowski, Tomasz S.},
- title = {{LegUp}: high-level synthesis for {FPGA}-based processor/accelerator systems},
+ author = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and Kammoona, Ahmed and Anderson, Jason Helge and Brown, Stephen Dean and Czajkowski, Tomasz S.},
+ publisher = {ACM},
booktitle = {{FPGA}},
- year = 2011,
+ doi = {10.1145/1950413.1950423},
pages = {33--36},
- publisher = {{ACM}},
- doi = {10.1145/1950413.1950423}
+ title = {{LegUp}: high-level synthesis for {FPGA}-based processor/accelerator systems},
+ year = {2011}
}
@article{canis13_legup,
- author = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and
- Kammoona, Ahmed and Czajkowski, Tomasz and Brown, Stephen D. and Anderson, Jason
- H.},
- title = {Legup: an Open-Source High-Level Synthesis Tool for Fpga-Based
- Processor/accelerator Systems},
- journal = {ACM Trans. Embed. Comput. Syst.},
- volume = {13},
- number = {2},
- year = {2013},
+ author = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and Kammoona, Ahmed and Czajkowski, Tomasz and Brown, Stephen D. and Anderson, Jason H.},
+ location = {New York, NY, USA},
+ publisher = {Association for Computing Machinery},
doi = {10.1145/2514740},
- address = {New York, NY, USA},
- articleno = {24},
issn = {1539-9087},
- issue_date = {September 2013},
- keywords = {High-level synthesis, FPGAs, hardware/software codesign, synthesis,
- performance, power, field-programmable gate arrays},
- month = sep,
- numpages = {27},
- publisher = {Association for Computing Machinery}
+ journaltitle = {ACM Trans. Embed. Comput. Syst.},
+ keywords = {High-level synthesis,FPGAs,hardware/software codesign,synthesis,performance,power,field-programmable gate arrays},
+ month = 9,
+ number = {2},
+ title = {Legup: an Open-Source High-Level Synthesis Tool for Fpga-Based Processor/accelerator Systems},
+ volume = {13},
+ year = {2013}
}
@inproceedings{chapman92_verif_bedroc,
author = {{Chapman}, R. and {Brown}, G. and {Leeser}, M.},
- title = {Verified high-level synthesis in BEDROC},
+ publisher = {IEEE Computer Society},
booktitle = {[1992] Proceedings The European Conference on Design Automation},
- year = 1992,
- pages = {59--63},
doi = {10.1109/EDAC.1992.205894},
- month = {March},
- publisher = {IEEE Computer Society}
+ month = 3,
+ pages = {59--63},
+ title = {Verified high-level synthesis in BEDROC},
+ year = {1992}
}
@misc{chauhan20_formal_ensur_equiv_c_rtl,
author = {Chauhan, Pankaj},
- title = {Formally Ensuring Equivalence between C++ and RTL designs},
url = {https://bit.ly/2KbT0ki},
+ title = {Formally Ensuring Equivalence between C++ and RTL designs},
year = {2020}
}
@inproceedings{cheng20_combin_dynam_static_sched_high_level_synth,
- author = {Cheng, Jianyi and Josipovic, Lana and Constantinides, George A. and Ienne,
- Paolo and Wickerson, John},
- title = {Combining Dynamic \& Static Scheduling in High-Level Synthesis},
- booktitle = {The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
- year = 2020,
- pages = {288-298},
- doi = {10.1145/3373087.3375297},
- address = {New York, NY, USA},
- isbn = 9781450370998,
- keywords = {high-level synthesis, dynamic scheduling, static analysis},
+ author = {Cheng, Jianyi and Josipovic, Lana and Constantinides, George A. and Ienne, Paolo and Wickerson, John},
location = {Seaside, CA, USA},
- numpages = 11,
publisher = {Association for Computing Machinery},
- series = {FPGA '20}
+ booktitle = {The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
+ doi = {10.1145/3373087.3375297},
+ isbn = {9781450370998},
+ keywords = {high-level synthesis,dynamic scheduling,static analysis},
+ pages = {288--298},
+ series = {FPGA '20},
+ title = {Combining Dynamic \& Static Scheduling in High-Level Synthesis},
+ year = {2020}
}
-@INPROCEEDINGS{choi18_hls_based_optim_desig_space,
+@inproceedings{choi18_hls_based_optim_desig_space,
author = {{Choi}, Y. and {Cong}, J.},
booktitle = {2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
+ doi = {10.1145/3240765.3240815},
+ pages = {1--8},
title = {HLS-Based Optimization and Design Space Exploration for Applications with Variable Loop Bounds},
- year = {2018},
- volume = {},
- number = {},
- pages = {1-8},
- doi = {10.1145/3240765.3240815}
+ year = {2018}
}
@article{chouksey19_trans_valid_code_motion_trans_invol_loops,
author = {{Chouksey}, R. and {Karfa}, C. and {Bhaduri}, P.},
- title = {Translation Validation of Code Motion Transformations
- Involving Loops},
- journal = {IEEE Transactions on Computer-Aided Design of Integrated
- Circuits and Systems},
- volume = 38,
- number = 7,
- pages = {1378-1382},
- year = 2019,
doi = {10.1109/TCAD.2018.2846654},
- ISSN = {1937-4151},
- month = {July}
+ issn = {1937-4151},
+ journaltitle = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+ month = jul,
+ number = {7},
+ pages = {1378--1382},
+ title = {Translation Validation of Code Motion Transformations Involving Loops},
+ volume = {38},
+ year = {2019}
}
@article{chouksey20_verif_sched_condit_behav_high_level_synth,
author = {Chouksey, R. and Karfa, C.},
- title = {Verification of Scheduling of Conditional Behaviors in
- High-Level Synthesis},
- journal = {IEEE Transactions on Very Large Scale Integration (VLSI)
- Systems},
- volume = {},
- number = {},
- pages = {1-14},
- year = {2020},
- doi = {10.1109/TVLSI.2020.2978242},
url = {https://doi.org/10.1109/TVLSI.2020.2978242},
- ISSN = {1557-9999},
- month = {}
+ doi = {10.1109/TVLSI.2020.2978242},
+ issn = {1557-9999},
+ journaltitle = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
+ pages = {1--14},
+ title = {Verification of Scheduling of Conditional Behaviors in High-Level Synthesis},
+ year = {2020}
}
@inproceedings{clarke03_behav_c_veril,
- author = {E. {Clarke} and D. {Kroening} and K. {Yorav}},
- title = {Behavioral consistency of {C} and {Verilog} programs using bounded model checking},
+ author = {{Clarke}, E. and {Kroening}, D. and {Yorav}, K.},
+ url = {https://doi.org/10.1145/775832.775928},
booktitle = {Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451)},
- year = 2003,
- pages = {368-371},
doi = {10.1145/775832.775928},
- url = {https://doi.org/10.1145/775832.775928}
+ pages = {368--371},
+ title = {Behavioral consistency of {C} and {Verilog} programs using bounded model checking},
+ year = {2003}
}
@inproceedings{cong06_sdc,
- year = {2006},
abstract = {Scheduling plays a central role in the behavioral synthesis process, which automatically compiles high-level specifications into optimized hardware implementations. However, most of the existing behavior-level scheduling heuristics either have a limited efficiency in a specific class of applications or lack general support of various design constraints. In this paper we describe a new scheduler that converts a rich set of scheduling constraints into a system of difference constraints (SDC) and performs a variety of powerful optimizations under a unified mathematical programming framework. In particular, we show that our SDC-based scheduling algorithm can efficiently support resource constraints, frequency constraints, latency constraints, and relative timing constraints, and effectively optimize longest path latency, expected overall latency, and the slack distribution. Experiments demonstrate that our proposed technique provides efficient solutions for a broader range of applications with higher quality of results (in terms of system performance) when compared to the state-of-the-art scheduling heuristics},
- author = {Cong, J. and Zhiru Zhang},
+ author = {Cong, J. and Zhang, Zhiru},
url = {https://doi.org/10.1145/1146909.1147025},
booktitle = {2006 43rd ACM/IEEE Design Automation Conference},
- date = {2006-07},
doi = {10.1145/1146909.1147025},
issn = {0738-100X},
keywords = {high-level synthesis,static scheduling},
+ month = jul,
pages = {433--438},
- title = {An efficient and versatile scheduling algorithm based on SDC formulation}
+ title = {An efficient and versatile scheduling algorithm based on SDC formulation},
+ year = {2006}
}
@article{cong11_high_level_synth_fpgas,
- author = {Jason Cong and
- Bin Liu and
- Stephen Neuendorffer and
- Juanjo Noguera and
- Kees A. Vissers and
- Zhiru Zhang},
- title = {High-Level Synthesis for FPGAs: From Prototyping to Deployment},
- journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
- volume = {30},
+ author = {Cong, Jason and Liu, Bin and Neuendorffer, Stephen and Noguera, Juanjo and Vissers, Kees A. and Zhang, Zhiru},
+ doi = {10.1109/TCAD.2011.2110592},
+ journaltitle = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
number = {4},
pages = {473--491},
- year = {2011},
- doi = {10.1109/TCAD.2011.2110592}
+ title = {High-Level Synthesis for FPGAs: From Prototyping to Deployment},
+ volume = {30},
+ year = {2011}
}
@inbook{coussy08_gaut,
- author = "Coussy, Philippe
-and Chavet, Cyrille
-and Bomel, Pierre
-and Heller, Dominique
-and Senn, Eric
-and Martin, Eric",
- editor = "Coussy, Philippe
-and Morawiec, Adam",
- title = "GAUT: A High-Level Synthesis Tool for DSP Applications",
- bookTitle = "High-Level Synthesis: From Algorithm to Digital Circuit",
- year = "2008",
- publisher = "Springer Netherlands",
- address = "Dordrecht",
- pages = "147--169",
- abstract = "This chapter presents GAUT, an academic and open-source high-level synthesis tool dedicated to digital signal processing applications. Starting from an algorithmic bit-accurate specification written in C/C++, GAUT extracts the potential parallelism before processing the allocation, the scheduling and the binding tasks. Mandatory synthesis constraints are the throughput and the clock period while the memory mapping and the I/O timing diagram are optional. GAUT next generates a potentially pipelined architecture composed of a processing unit, a memory unit and a communication with a GALS/LIS interface.",
- isbn = "978-1-4020-8588-8",
- doi = "10.1007/978-1-4020-8588-8_9",
- url = "https://doi.org/10.1007/978-1-4020-8588-8_9"
+ abstract = {This chapter presents GAUT, an academic and open-source high-level synthesis tool dedicated to digital signal processing applications. Starting from an algorithmic bit-accurate specification written in C/C++, GAUT extracts the potential parallelism before processing the allocation, the scheduling and the binding tasks. Mandatory synthesis constraints are the throughput and the clock period while the memory mapping and the I/O timing diagram are optional. GAUT next generates a potentially pipelined architecture composed of a processing unit, a memory unit and a communication with a GALS/LIS interface.},
+ author = {Coussy, Philippe and Chavet, Cyrille and Bomel, Pierre and Heller, Dominique and Senn, Eric and Martin, Eric},
+ editor = {Coussy, Philippe and Morawiec, Adam},
+ location = {Dordrecht},
+ publisher = {Springer Netherlands},
+ url = {https://doi.org/10.1007/978-1-4020-8588-8_9},
+ booktitle = {High-Level Synthesis: From Algorithm to Digital Circuit},
+ doi = {10.1007/978-1-4020-8588-8_9},
+ isbn = {978-1-4020-8588-8},
+ pages = {147--169},
+ title = {GAUT: A High-Level Synthesis Tool for DSP Applications},
+ year = {2008}
}
@article{coussy09_introd_to_high_level_synth,
- author = {P. {Coussy} and D. D. {Gajski} and M. {Meredith} and
- A. {Takach}},
- title = {An Introduction To High-Level Synthesis},
- tags = {hls},
- journal = {IEEE Design Test of Computers},
- volume = 26,
- number = 4,
- pages = {8-17},
- year = 2009,
+ author = {{Coussy}, P. and {Gajski}, D. D. and {Meredith}, M. and {Takach}, A.},
doi = {10.1109/MDT.2009.69},
- keywords = {high level synthesis;high-level synthesis;optimized RTL
- hardware;abstraction level design;HLS techniques;High level
- synthesis;Assembly;Application software;Circuit
- simulation;Design methodology;Space exploration;Computer
- architecture;Design optimization;Hardware design
- languages;Circuit synthesis;high-level synthesis;RTL
- abstraction;custom processors;hardware synthesis and
- verification;architectures;design and test},
- month = {July}
+ journaltitle = {IEEE Design Test of Computers},
+ keywords = {high level synthesis;high-level synthesis;optimized RTL hardware;abstraction level design;HLS techniques;High level synthesis;Assembly;Application software;Circuit simulation;Design methodology;Space exploration;Computer architecture;Design optimization;Hardware design languages;Circuit synthesis;high-level synthesis;RTL abstraction;custom processors;hardware synthesis and verification;architectures;design and test},
+ month = jul,
+ number = {4},
+ pages = {8--17},
+ title = {An Introduction To High-Level Synthesis},
+ volume = {26},
+ year = {2009}
}
@inproceedings{davidthomas_asap16,
author = {Thomas, David B.},
- title = {Synthesisable recursion for {C++} {HLS} tools},
+ publisher = {{IEEE} Computer Society},
booktitle = {{ASAP}},
+ doi = {10.1109/ASAP.2016.7760777},
pages = {91--98},
- publisher = {{IEEE} Computer Society},
- year = {2016},
- doi = {10.1109/ASAP.2016.7760777}
+ title = {Synthesisable recursion for {C++} {HLS} tools},
+ year = {2016}
}
-@phdthesis{ellis08_correc,
+@thesis{ellis08_correc,
author = {Ellis, Martin},
- title = {Correct synthesis and integration of compiler-generated function units},
- school = {Newcastle University},
+ institution = {Newcastle University},
url = {https://theses.ncl.ac.uk/jspui/handle/10443/828},
+ title = {Correct synthesis and integration of compiler-generated function units},
+ type = {phdthesis},
year = {2008}
}
-@INPROCEEDINGS{gajski10_what_hls,
- author = {Dan Gajski and Todd Austin and Steve Svoboda},
+@inproceedings{gajski10_what_hls,
+ author = {Gajski, Dan and Austin, Todd and Svoboda, Steve},
booktitle = {Design Automation Conference},
+ doi = {10.1145/1837274.1837489},
+ pages = {857--858},
title = {What input-language is the best choice for high level synthesis (HLS)?},
- year = {2010},
- volume = {},
- number = {},
- pages = {857-858},
- doi = {10.1145/1837274.1837489}
+ year = {2010}
}
@misc{gauthier20_high_level_synth,
author = {Gauthier, Stephane and Wadood, Zubair},
- title = {High-Level Synthesis: Can it outperform hand-coded {HDL}?},
- note = {White paper},
url = {https://info.silexica.com/high-level-synthesis/1},
+ note = {White paper},
+ title = {High-Level Synthesis: Can it outperform hand-coded {HDL}?},
year = {2020}
}
@inproceedings{grass94_high,
author = {{Grass}, W. and {Mutz}, M. and {Tiedemann}, W. -.},
- title = {High level synthesis based on formal methods},
- booktitle = {Proceedings of Twentieth Euromicro Conference. System
- Architecture and Integration},
- year = 1994,
- pages = {83-91},
+ booktitle = {Proceedings of Twentieth Euromicro Conference. System Architecture and Integration},
doi = {10.1109/EURMIC.1994.390403},
- month = {Sep.}
+ month = sep,
+ pages = {83--91},
+ title = {High level synthesis based on formal methods},
+ year = {1994}
}
@inproceedings{greaves08_kiwi,
- author = {David J. Greaves and
- Satnam Singh},
- title = {Kiwi: Synthesis of {FPGA} Circuits from Parallel Programs},
+ author = {Greaves, David J. and Singh, Satnam},
+ publisher = {{IEEE} Computer Society},
booktitle = {{FCCM}},
+ doi = {10.1109/FCCM.2008.46},
pages = {3--12},
- publisher = {{IEEE} Computer Society},
- year = {2008},
- doi = {10.1109/FCCM.2008.46}
+ title = {Kiwi: Synthesis of {FPGA} Circuits from Parallel Programs},
+ year = {2008}
}
@misc{greaves19_resear_note,
- title = {Research Note: An Open Source Bluespec Compiler},
- author = {David J. Greaves},
- year = {2019},
+ author = {Greaves, David J.},
eprint = {1905.03746},
- archivePrefix = {arXiv},
- primaryClass = {cs.PL}
+ eprintclass = {cs.PL},
+ eprinttype = {arXiv},
+ title = {Research Note: An Open Source Bluespec Compiler},
+ year = {2019}
}
@inproceedings{gupta03_spark,
author = {{Gupta}, S. and {Dutt}, N. and {Gupta}, R. and {Nicolau}, A.},
- title = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler
- transformations},
+ url = {https://doi.org/10.1109/ICVD.2003.1183177},
booktitle = {16th International Conference on VLSI Design, 2003. Proceedings.},
- year = 2003,
- pages = {461-466},
doi = {10.1109/ICVD.2003.1183177},
- url = {https://doi.org/10.1109/ICVD.2003.1183177},
- ISSN = {1063-9667},
- month = {Jan}
+ issn = {1063-9667},
+ month = jan,
+ pages = {461--466},
+ title = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler transformations},
+ year = {2003}
}
@inproceedings{herklotz20_findin_under_bugs_fpga_synth_tools,
- author = {Yann Herklotz and John Wickerson},
- title = {Finding and Understanding Bugs in {FPGA} Synthesis Tools},
+ author = {Herklotz, Yann and Wickerson, John},
+ location = {Seaside, CA, USA},
booktitle = {ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays},
- year = 2020,
doi = {10.1145/3373087.3375310},
isbn = {978-1-4503-7099-8/20/02},
- keywords = {automated testing, compiler defect, compiler testing, random program
- generation, random testing},
- location = {Seaside, CA, USA},
- numpages = 11
+ keywords = {automated testing,compiler defect,compiler testing,random program generation,random testing},
+ title = {Finding and Understanding Bugs in {FPGA} Synthesis Tools},
+ year = {2020}
}
-@INPROCEEDINGS{herklotz21_empir_study_reliab_high_level_synth_tools,
+@inproceedings{herklotz21_empir_study_reliab_high_level_synth_tools,
author = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John},
booktitle = {2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)},
+ doi = {10.1109/FCCM51124.2021.00034},
+ pages = {219--223},
title = {An Empirical Study of the Reliability of High-Level Synthesis Tools},
- year = {2021},
- volume = {},
- number = {},
- pages = {219-223},
- doi = {10.1109/FCCM51124.2021.00034}
+ year = {2021}
}
@article{herklotz21_formal_verif_high_level_synth,
- year = {2021},
abstract = {High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity. In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language such as Verilog, while maintaining the convenience and the rich ecosystem of software development. However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level. Furthermore, there is mounting evidence that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs. To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software. Our tool, called Vericert, extends the CompCert verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. Vericert supports most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general control-flow statements. An evaluation on the PolyBench/C benchmark suite indicates that Vericert generates hardware that is around an order of magnitude slower (only around 2\texttimes{} slower in the absence of division) and about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.},
author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
location = {New York, NY, USA},
publisher = {Association for Computing Machinery},
url = {https://doi.org/10.1145/3485494},
- date = {2021-10},
doi = {10.1145/3485494},
- journal = {Proceedings of the ACM on Programming Languages},
+ journaltitle = {Proceedings of the ACM on Programming Languages},
keywords = {high-level synthesis,Coq,Verilog,CompCert,C},
+ month = oct,
number = {OOPSLA},
title = {Formal Verification of High-Level Synthesis},
- volume = {5}
+ volume = {5},
+ year = {2021}
}
@misc{herklotz21_veric,
- author = {Yann Herklotz and James D. Pollard and Nadesh Ramanathan and John Wickerson},
- title = {Vericert v1.2.1},
- month = jul,
- year = 2021,
+ author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
publisher = {Zenodo},
- version = {v1.2.1},
+ url = {https://doi.org/10.5281/zenodo.5093839},
doi = {10.5281/zenodo.5093839},
- url = {https://doi.org/10.5281/zenodo.5093839}
+ month = jul,
+ title = {Vericert v1.2.1},
+ version = {v1.2.1},
+ year = {2021}
}
@inproceedings{homsirikamol14_can,
author = {Homsirikamol, Ekawat and Gaj, Kris},
- title = {Can high-level synthesis compete against a hand-written code in the
- cryptographic domain? {A} case study},
+ publisher = {IEEE},
booktitle = {ReConFig},
+ doi = {10.1109/ReConFig.2014.7032504},
pages = {1--8},
- publisher = {{IEEE}},
- year = {2014},
- doi = {10.1109/ReConFig.2014.7032504}
+ title = {Can high-level synthesis compete against a hand-written code in the cryptographic domain? {A} case study},
+ year = {2014}
}
@article{hwang91_formal_approac_to_sched_probl,
author = {{Hwang}, C. -. and {Lee}, J. -. and {Hsu}, Y. -.},
- title = {A Formal Approach To the Scheduling Problem in High Level
- Synthesis},
- journal = {IEEE Transactions on Computer-Aided Design of Integrated
- Circuits and Systems},
- volume = 10,
- number = 4,
- pages = {464-475},
- year = 1991,
- doi = {10.1109/43.75629},
url = {https://doi.org/10.1109/43.75629},
- month = {April}
+ doi = {10.1109/43.75629},
+ journaltitle = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+ month = apr,
+ number = {4},
+ pages = {464--475},
+ title = {A Formal Approach To the Scheduling Problem in High Level Synthesis},
+ volume = {10},
+ year = {1991}
}
@inproceedings{hwang99_fsmd,
author = {Hwang, Enoch and Vahid, Frank and Hsu, Yu-Chin},
- title = {FSMD functional partitioning for low power},
booktitle = {Proceedings of the conference on Design, automation and test in Europe},
- year = 1999,
+ doi = {10.1109/DATE.1999.761092},
pages = {7--es},
- doi = {10.1109/DATE.1999.761092}
+ title = {FSMD functional partitioning for low power},
+ year = {1999}
+}
+
+@inbook{hwu93_super,
+ abstract = {A compiler for VLIW and superscalar processors must expose sufficient instruction-level parallelism (ILP) to effectively utilize the parallel hardware. However, ILP within basic blocks is extremely limited for control-intensive programs. We have developed a set of techniques for exploiting ILP across basic block boundaries. These techniques are based on a novel structure called the superblock. The superblock enables the optimizer and scheduler to extract more ILP along the important execution paths by systematically removing constraints due to the unimportant paths. Superblock optimization and scheduling have been implemented in the IMPACT-I compiler. This implementation gives us a unique opportunity to fully understand the issues involved in incorporating these techniques into a real compiler. Superblock optimizations and scheduling are shown to be useful while taking into account a variety of architectural features.},
+ author = {Hwu, Wen-Mei W. and Mahlke, Scott A. and Chen, William Y. and Chang, Pohua P. and Warter, Nancy J. and Bringmann, Roger A. and Ouellette, Roland G. and Hank, Richard E. and Kiyohara, Tokuzo and Haab, Grant E. and Holm, John G. and Lavery, Daniel M.},
+ editor = {Rau, B. R. and Fisher, J. A.},
+ location = {Boston, MA},
+ publisher = {Springer US},
+ url = {https://doi.org/10.1007/978-1-4615-3200-2_7},
+ booktitle = {Instruction-Level Parallelism: A Special Issue of The Journal of Supercomputing},
+ doi = {10.1007/978-1-4615-3200-2_7},
+ isbn = {978-1-4615-3200-2},
+ keywords = {superblock scheduling,trace scheduling,static scheduling},
+ pages = {229--248},
+ title = {The Superblock: An Effective Technique for VLIW and Superscalar Compilation},
+ year = {1993}
}
@misc{intel19_intel_quart,
author = {Intel},
- title = {{Intel Quartus}},
url = {https://intel.ly/2m7wbCs},
+ title = {{Intel Quartus}},
urldate = {2019-01-14},
- year = 2019
+ year = {2019}
}
@misc{intel20_high_synth_compil,
author = {Intel},
- title = {High-level Synthesis Compiler},
url = {https://intel.ly/2UDiWr5},
+ title = {High-level Synthesis Compiler},
urldate = {2020-11-18},
year = {2020}
}
@misc{intel20_sdk_openc_applic,
author = {Intel},
- title = {{SDK} for {OpenCL} Applications},
url = {https://intel.ly/30sYHz0},
+ title = {{SDK} for {OpenCL} Applications},
urldate = {2020-07-20},
- year = 2020
+ year = {2020}
}
@inproceedings{jifeng93_towar,
- author = "Jifeng, He and Page, Ian and Bowen, Jonathan",
- title = "Towards a provably correct hardware implementation of Occam",
- booktitle = "Correct Hardware Design and Verification Methods",
- year = 1993,
- pages = "214--225",
- address = "Berlin, Heidelberg",
- editor = "Milne, George J. and Pierre, Laurence",
- isbn = "978-3-540-70655-7",
- publisher = "Springer"
+ author = {Jifeng, He and Page, Ian and Bowen, Jonathan},
+ editor = {Milne, George J. and Pierre, Laurence},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer},
+ booktitle = {Correct Hardware Design and Verification Methods},
+ isbn = {978-3-540-70655-7},
+ pages = {214--225},
+ title = {Towards a provably correct hardware implementation of Occam},
+ year = {1993}
}
@article{josipovic17_out_of_order_load_store,
author = {Josipovic, Lana and Brisk, Philip and Ienne, Paolo},
- title = {An Out-Of-Order Load-Store Queue for Spatial Computing},
- journal = {ACM Trans. Embed. Comput. Syst.},
- volume = {16},
- number = {5s},
- year = {2017},
+ location = {New York, NY, USA},
+ publisher = {Association for Computing Machinery},
doi = {10.1145/3126525},
- address = {New York, NY, USA},
- articleno = {125},
issn = {1539-9087},
- issue_date = {October 2017},
- keywords = {Load-store queue, dynamic scheduling, allocation, spatial computing},
+ journaltitle = {ACM Trans. Embed. Comput. Syst.},
+ keywords = {Load-store queue,dynamic scheduling,allocation,spatial computing},
month = sep,
- numpages = {19},
- publisher = {Association for Computing Machinery}
+ number = {5s},
+ title = {An Out-Of-Order Load-Store Queue for Spatial Computing},
+ volume = {16},
+ year = {2017}
}
@inproceedings{josipovic18_dynam_sched_high_level_synth,
- author = {Josipovi\'{c}, Lana and Ghosal, Radhika and Ienne, Paolo},
- title = {Dynamically Scheduled High-Level Synthesis},
- booktitle = {Proceedings of the 2018 ACM/SIGDA International Symposium on Field-Programmable
- Gate Arrays},
- year = 2018,
- pages = {127-136},
- doi = {10.1145/3174243.3174264},
- address = {New York, NY, USA},
- isbn = 9781450356145,
- keywords = {dynamically scheduled circuits, compiler, pipelining, high-level synthesis},
+ author = {Josipović, Lana and Ghosal, Radhika and Ienne, Paolo},
location = {Monterey, CALIFORNIA, USA},
- numpages = 10,
publisher = {Association for Computing Machinery},
- series = {FPGA '18}
+ booktitle = {Proceedings of the 2018 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
+ doi = {10.1145/3174243.3174264},
+ isbn = {9781450356145},
+ keywords = {dynamically scheduled circuits,compiler,pipelining,high-level synthesis},
+ pages = {127--136},
+ series = {FPGA '18},
+ title = {Dynamically Scheduled High-Level Synthesis},
+ year = {2018}
}
@inproceedings{josipovic20_buffer_placem_sizin_high_perfor_dataf_circuit,
- author = {Josipovi\'{c}, Lana and Sheikhha, Shabnam and Guerrieri, Andrea and Ienne,
- Paolo and Cortadella, Jordi},
- title = {Buffer Placement and Sizing for High-Performance Dataflow Circuits},
- booktitle = {The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
- year = 2020,
- pages = {186-196},
- doi = {10.1145/3373087.3375314},
- address = {New York, NY, USA},
- isbn = 9781450370998,
- keywords = {buffers, high-level synthesis, dataflow circuits, timing optimization},
+ author = {Josipović, Lana and Sheikhha, Shabnam and Guerrieri, Andrea and Ienne, Paolo and Cortadella, Jordi},
location = {Seaside, CA, USA},
- numpages = 11,
publisher = {Association for Computing Machinery},
- series = {FPGA '20}
+ booktitle = {The 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
+ doi = {10.1145/3373087.3375314},
+ isbn = {9781450370998},
+ keywords = {buffers,high-level synthesis,dataflow circuits,timing optimization},
+ pages = {186--196},
+ series = {FPGA '20},
+ title = {Buffer Placement and Sizing for High-Performance Dataflow Circuits},
+ year = {2020}
}
@inproceedings{jourdan12_valid_lr_parser,
- author = "Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and
- Leroy, Xavier",
- title = "Validating LR(1) Parsers",
- booktitle = "Programming Languages and Systems",
- year = 2012,
- pages = "397--416",
- address = "Berlin, Heidelberg",
- editor = "Seidl, Helmut",
- isbn = "978-3-642-28869-2",
- publisher = "Springer Berlin Heidelberg",
- doi = "10.1007/978-3-642-28869-2_20"
+ author = {Jourdan, Jacques-Henri and Pottier, François and Leroy, Xavier},
+ editor = {Seidl, Helmut},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer Berlin Heidelberg},
+ booktitle = {Programming Languages and Systems},
+ doi = {10.1007/978-3-642-28869-2_20},
+ isbn = {978-3-642-28869-2},
+ pages = {397--416},
+ title = {Validating LR(1) Parsers},
+ year = {2012}
}
@inproceedings{karfa06_formal_verif_method_sched_high_synth,
- author = {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and
- Reade, Chris},
- title = {A Formal Verification Method of Scheduling in High-level
- Synthesis},
- booktitle = {Proceedings of the 7th International Symposium on Quality
- Electronic Design},
- year = 2006,
- pages = {71--78},
+ author = {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and Reade, Chris},
+ location = {Washington, DC, USA},
+ publisher = {IEEE Computer Society},
+ booktitle = {Proceedings of the 7th International Symposium on Quality Electronic Design},
doi = {10.1109/ISQED.2006.10},
- acmid = 1126731,
- address = {Washington, DC, USA},
isbn = {0-7695-2523-7},
- numpages = 8,
- publisher = {IEEE Computer Society},
- series = {ISQED '06}
+ pages = {71--78},
+ series = {ISQED '06},
+ title = {A Formal Verification Method of Scheduling in High-level Synthesis},
+ year = {2006}
}
@inproceedings{karfa07_hand_verif_high_synth,
- author = {Karfa, C. and Sarkar, D. and Mandal, C.
- and Reade, C.},
- title = {Hand-in-hand Verification of High-level Synthesis},
- tags = {hls},
+ author = {Karfa, C. and Sarkar, D. and Mandal, C. and Reade, C.},
+ location = {Stresa-Lago Maggiore, Italy},
+ publisher = {ACM},
booktitle = {Proceedings of the 17th ACM Great Lakes Symposium on VLSI},
- year = 2007,
- pages = {429--434},
doi = {10.1145/1228784.1228885},
- acmid = 1228885,
- address = {New York, NY, USA},
isbn = {978-1-59593-605-9},
- location = {Stresa-Lago Maggiore, Italy},
- numpages = 6,
- publisher = {ACM},
- series = {GLSVLSI '07}
+ pages = {429--434},
+ series = {GLSVLSI '07},
+ title = {Hand-in-hand Verification of High-level Synthesis},
+ year = {2007}
}
@article{karfa08_equiv_check_method_sched_verif,
- author = {C. {Karfa} and D. {Sarkar} and C. {Mandal} and P. {Kumar}},
- title = {An Equivalence-Checking Method for Scheduling Verification in
- High-Level Synthesis},
- tags = {hls, verification},
- journal = {IEEE Transactions on Computer-Aided Design of Integrated
- Circuits and Systems},
- volume = 27,
- number = 3,
- pages = {556-569},
- year = 2008,
+ author = {{Karfa}, C. and {Sarkar}, D. and {Mandal}, C. and {Kumar}, P.},
doi = {10.1109/TCAD.2007.913390},
- ISSN = {1937-4151},
- month = {March}
+ issn = {1937-4151},
+ journaltitle = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+ month = mar,
+ number = {3},
+ pages = {556--569},
+ title = {An Equivalence-Checking Method for Scheduling Verification in High-Level Synthesis},
+ volume = {27},
+ year = {2008}
}
@article{karfa10_verif_datap_contr_gener_phase,
- author = {C. {Karfa} and D. {Sarkar} and C. {Mandal}},
- title = {Verification of Datapath and Controller Generation Phase in
- High-Level Synthesis of Digital Circuits},
- tags = {hls, verification},
- journal = {IEEE Transactions on Computer-Aided Design of Integrated
- Circuits and Systems},
- volume = 29,
- number = 3,
- pages = {479-492},
- year = 2010,
+ author = {{Karfa}, C. and {Sarkar}, D. and {Mandal}, C.},
doi = {10.1109/TCAD.2009.2035542},
- ISSN = {1937-4151},
- month = {March}
+ issn = {1937-4151},
+ journaltitle = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+ month = mar,
+ number = {3},
+ pages = {479--492},
+ title = {Verification of Datapath and Controller Generation Phase in High-Level Synthesis of Digital Circuits},
+ volume = {29},
+ year = {2010}
}
@article{karfa12_formal_verif_code_motion_techn,
author = {Karfa, C. and Mandal, C. and Sarkar, D.},
- title = {Formal Verification of Code Motion Techniques Using
- Data-Flow-Driven Equivalence Checking},
- tags = {hls, verification},
- journal = {ACM Trans. Des. Autom. Electron. Syst.},
- volume = 17,
- number = 3,
- year = 2012,
+ location = {New York, NY, USA},
+ publisher = {Association for Computing Machinery},
doi = {10.1145/2209291.2209303},
- address = {New York, NY, USA},
- articleno = {Article 30},
issn = {1084-4309},
- issue_date = {June 2012},
+ journaltitle = {ACM Trans. Des. Autom. Electron. Syst.},
month = jul,
- numpages = 37,
- publisher = {Association for Computing Machinery}
+ number = {3},
+ title = {Formal Verification of Code Motion Techniques Using Data-Flow-Driven Equivalence Checking},
+ volume = {17},
+ year = {2012}
}
@inproceedings{kildall73_unified_approac_global_progr_optim,
author = {Kildall, Gary A.},
- title = {A Unified Approach to Global Program Optimization},
- booktitle = {Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of
- Programming Languages},
- year = 1973,
- pages = {194-206},
- doi = {10.1145/512927.512945},
- address = {New York, NY, USA},
- isbn = 9781450373494,
location = {Boston, Massachusetts},
- numpages = 13,
publisher = {Association for Computing Machinery},
- series = {POPL '73}
+ booktitle = {Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
+ doi = {10.1145/512927.512945},
+ isbn = {9781450373494},
+ pages = {194--206},
+ series = {POPL '73},
+ title = {A Unified Approach to Global Program Optimization},
+ year = {1973}
}
@inproceedings{kim04_autom_fsmd,
- author = { {Youngsik Kim} and {Kopuri}, S. and {Mansouri}, N.},
- title = {Automated formal verification of scheduling process using
- finite state machines with datapath (FSMD)},
- booktitle = {International Symposium on Signals, Circuits and
- Systems. Proceedings, SCS 2003. (Cat. No.03EX720)},
- year = 2004,
- pages = {110-115},
+ author = {{Youngsik Kim} and {Kopuri}, S. and {Mansouri}, N.},
+ booktitle = {International Symposium on Signals, Circuits and Systems. Proceedings, SCS 2003. (Cat. No.03EX720)},
doi = {10.1109/ISQED.2004.1283659},
- month = {March}
+ month = mar,
+ pages = {110--115},
+ title = {Automated formal verification of scheduling process using finite state machines with datapath (FSMD)},
+ year = {2004}
}
@inproceedings{kundu07_autom,
- author = { {Sudipta Kundu} and S. {Lerner} and {Rajesh Gupta}},
- title = {Automated refinement checking of concurrent systems},
+ author = {{Sudipta Kundu} and {Lerner}, S. and {Rajesh Gupta}},
booktitle = {2007 IEEE/ACM International Conference on Computer-Aided Design},
- year = 2007,
- pages = {318-325},
doi = {10.1109/ICCAD.2007.4397284},
- ISSN = {1558-2434},
- month = {Nov}
+ issn = {1558-2434},
+ month = nov,
+ pages = {318--325},
+ title = {Automated refinement checking of concurrent systems},
+ year = {2007}
}
@inproceedings{kundu08_valid_high_level_synth,
- author = "Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh",
- title = "Validating High-Level Synthesis",
- booktitle = "Computer Aided Verification",
- year = 2008,
- pages = "459--472",
- address = "Berlin, Heidelberg",
- editor = "Gupta, Aarti and Malik, Sharad",
- isbn = "978-3-540-70545-1",
- publisher = "Springer",
- doi = "10.1007/978-3-540-70545-1_44"
+ author = {Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh},
+ editor = {Gupta, Aarti and Malik, Sharad},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer},
+ booktitle = {Computer Aided Verification},
+ doi = {10.1007/978-3-540-70545-1_44},
+ isbn = {978-3-540-70545-1},
+ pages = {459--472},
+ title = {Validating High-Level Synthesis},
+ year = {2008}
}
@article{lahti19_are_we_there_yet,
- author = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and
- T. D. {H{\"a}m{\"a}l{\"a}inen}},
- title = {Are We There Yet? a Study on the State of High-Level
- Synthesis},
- journal = {IEEE Transactions on Computer-Aided Design of Integrated
- Circuits and Systems},
- volume = {38},
- number = {5},
- pages = {898-911},
- year = {2019},
+ author = {{Lahti}, S. and {Sjövall}, P. and {Vanne}, J. and {Hämäläinen}, T. D.},
doi = {10.1109/TCAD.2018.2834439},
- ISSN = {1937-4151},
- month = {May}
+ issn = {1937-4151},
+ journaltitle = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+ month = may,
+ number = {5},
+ pages = {898--911},
+ title = {Are We There Yet? a Study on the State of High-Level Synthesis},
+ volume = {38},
+ year = {2019}
}
@inproceedings{leroy06_formal_certif_compil_back_end,
author = {Leroy, Xavier},
- title = {Formal Certification of a Compiler Back-End or: Programming
- a Compiler with a Proof Assistant},
- booktitle = {Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium
- on Principles of Programming Languages},
- year = 2006,
- pages = {42-54},
- doi = {10.1145/1111037.1111042},
- url = {https://doi.org/10.1145/1111037.1111042},
- address = {New York, NY, USA},
- isbn = 1595930272,
location = {Charleston, South Carolina, USA},
- numpages = 13,
publisher = {ACM},
- series = {POPL '06}
+ url = {https://doi.org/10.1145/1111037.1111042},
+ booktitle = {Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ doi = {10.1145/1111037.1111042},
+ isbn = {1595930272},
+ pages = {42--54},
+ series = {POPL '06},
+ title = {Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant},
+ year = {2006}
}
@article{leroy09_formal_verif_compil_back_end,
author = {Leroy, Xavier},
- title = {A Formally Verified Compiler Back-End},
- journal = {Journal of Automated Reasoning},
- volume = {43},
+ doi = {10.1007/s10817-009-9155-4},
+ issn = {1573-0670},
+ journaltitle = {Journal of Automated Reasoning},
number = {4},
pages = {363},
- year = {2009},
- doi = {10.1007/s10817-009-9155-4},
- issn = {1573-0670}
+ title = {A Formally Verified Compiler Back-End},
+ volume = {43},
+ year = {2009}
}
@article{leroy09_formal_verif_realis_compil,
author = {Leroy, Xavier},
- title = {Formal Verification of a Realistic Compiler},
- journal = {Commun. ACM},
- volume = 52,
- number = 7,
- pages = {107-115},
- year = 2009,
+ location = {New York, NY, USA},
+ publisher = {ACM},
doi = {10.1145/1538788.1538814},
- address = {New York, NY, USA},
issn = {0001-0782},
- issue_date = {July 2009},
+ journaltitle = {Commun. ACM},
month = jul,
- numpages = 9,
- publisher = {ACM}
+ number = {7},
+ pages = {107--115},
+ title = {Formal Verification of a Realistic Compiler},
+ volume = {52},
+ year = {2009}
}
@inproceedings{lidbury15_many_core_compil_fuzzin,
- author = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson,
- Alastair F.},
- title = {Many-Core Compiler Fuzzing},
- booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design
- and Implementation},
- year = 2015,
- pages = {65-76},
- doi = {10.1145/2737924.2737986},
- address = {New York, NY, USA},
- isbn = 9781450334686,
+ author = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson, Alastair F.},
location = {Portland, OR, USA},
- numpages = 12,
publisher = {ACM},
- series = {PLDI '15}
+ booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ doi = {10.1145/2737924.2737986},
+ isbn = {9781450334686},
+ pages = {65--76},
+ series = {PLDI '15},
+ title = {Many-Core Compiler Fuzzing},
+ year = {2015}
}
@inproceedings{liu16_effic_high_level_synth_desig,
- author = { {Dong Liu} and B. C. {Schafer}},
- title = {Efficient and reliable High-Level Synthesis Design Space
- Explorer for FPGAs},
- booktitle = {2016 26th International Conference on Field Programmable
- Logic and Applications (FPL)},
- year = 2016,
- pages = {1-8},
+ author = {{Dong Liu} and {Schafer}, B. C.},
+ booktitle = {2016 26th International Conference on Field Programmable Logic and Applications (FPL)},
doi = {10.1109/FPL.2016.7577370},
- ISSN = {1946-1488},
- month = {Aug}
+ issn = {1946-1488},
+ month = aug,
+ pages = {1--8},
+ title = {Efficient and reliable High-Level Synthesis Design Space Explorer for FPGAs},
+ year = {2016}
}
@inproceedings{loow19_proof_trans_veril_devel_hol,
- author = {L\"{o}\"{o}w, Andreas and Myreen, Magnus O.},
- title = {A Proof-producing Translator for Verilog Development in HOL},
- tags = {hls, semantics},
- booktitle = {Proceedings of the 7th International Workshop on Formal
- Methods in Software Engineering},
- year = 2019,
- pages = {99--108},
- doi = {10.1109/FormaliSE.2019.00020},
- url = {https://doi.org/10.1109/FormaliSE.2019.00020},
- acmid = 3338828,
- address = {Piscataway, NJ, USA},
+ author = {Lööw, Andreas and Myreen, Magnus O.},
location = {Montreal, Quebec, Canada},
- numpages = 10,
publisher = {IEEE Press},
- series = {FormaliSE '19}
+ url = {https://doi.org/10.1109/FormaliSE.2019.00020},
+ booktitle = {Proceedings of the 7th International Workshop on Formal Methods in Software Engineering},
+ doi = {10.1109/FormaliSE.2019.00020},
+ pages = {99--108},
+ series = {FormaliSE '19},
+ title = {A Proof-producing Translator for Verilog Development in HOL},
+ year = {2019}
}
@inproceedings{loow19_verif_compil_verif_proces,
- author = {L\"{o}\"{o}w, Andreas and Kumar, Ramana and Tan, Yong Kiam and
- Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar
- and Fox, Anthony},
- title = {Verified Compilation on a Verified Processor},
- tags = {verification},
- booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming
- Language Design and Implementation},
- year = 2019,
- pages = {1041--1053},
- doi = {10.1145/3314221.3314622},
- acmid = 3314622,
- address = {New York, NY, USA},
- isbn = {978-1-4503-6712-7},
- keywords = {compiler verification, hardware verification, program
- verification, verified stack},
+ author = {Lööw, Andreas and Kumar, Ramana and Tan, Yong Kiam and Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar and Fox, Anthony},
location = {Phoenix, AZ, USA},
- numpages = 13,
publisher = {ACM},
- series = {PLDI 2019}
+ booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ doi = {10.1145/3314221.3314622},
+ isbn = {978-1-4503-6712-7},
+ keywords = {compiler verification,hardware verification,program verification,verified stack},
+ pages = {1041--1053},
+ series = {PLDI 2019},
+ title = {Verified Compilation on a Verified Processor},
+ year = {2019}
}
@inproceedings{loow21_lutsig,
- author = {L\"{o}\"{o}w, Andreas},
- title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
- year = {2021},
- isbn = {9781450382991},
+ abstract = {We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper we show how Lutsig, as a consequence of this connection, fits into a hardware development methodology for verified circuits in the HOL4 theorem prover. One important step in the methodology is transporting properties proved at the behavioral Verilog level down to technology mapped netlists, and Lutsig is the component in the methodology that enables such transportation.},
+ author = {Lööw, Andreas},
+ location = {Virtual, Denmark},
publisher = {ACM},
- address = {New York, NY, USA},
url = {https://doi.org/10.1145/3437992.3439916},
- doi = {10.1145/3437992.3439916},
- abstract = {We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper we show how Lutsig, as a consequence of this connection, fits into a hardware development methodology for verified circuits in the HOL4 theorem prover. One important step in the methodology is transporting properties proved at the behavioral Verilog level down to technology mapped netlists, and Lutsig is the component in the methodology that enables such transportation.},
booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
- pages = {46–60},
- numpages = {15},
- keywords = {hardware verification, hardware synthesis, compiler verification},
- location = {Virtual, Denmark},
- series = {CPP 2021}
+ doi = {10.1145/3437992.3439916},
+ isbn = {9781450382991},
+ keywords = {hardware verification,hardware synthesis,compiler verification},
+ pages = {46--60},
+ series = {CPP 2021},
+ title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
+ year = {2021}
+}
+
+@article{mahlke92_effec_compil_suppor_predic_execut_using_hyper,
+ author = {Mahlke, Scott A. and Lin, David C. and Chen, William Y. and Hank, Richard E. and Bringmann, Roger A.},
+ location = {New York, NY, USA},
+ publisher = {Association for Computing Machinery},
+ url = {https://doi.org/10.1145/144965.144998},
+ doi = {10.1145/144965.144998},
+ issn = {1050-916X},
+ journaltitle = {SIGMICRO Newsl.},
+ keywords = {speculative execution,static scheduling,hyperblocks},
+ month = dec,
+ number = {1-2},
+ pages = {45--54},
+ title = {Effective Compiler Support for Predicated Execution Using the Hyperblock},
+ volume = {23},
+ year = {1992}
+}
+
+@article{mahlke93_sentin_sched,
+ abstract = {Speculative execution is an important source of parallelism for VLIW and superscalar processors. A serious challenge with compiler-controlled speculative execution is to efficiently handle exceptions for speculative instructions. In this article, a set of architectural features and compile-time scheduling support collectively referred to as sentinel scheduling is introduced. Sentinel scheduling provides an effective framework for both compiler-controlled speculative execution and exception handling. All program exceptions are accurately detected and reported in a timely manner with sentinel scheduling. Recovery from exceptions is also ensured with the model. Experimental results show the effectiveness of sentinel scheduling for exploiting instruction-level parallelism and overhead associated with exception handling.},
+ author = {Mahlke, Scott A. and Chen, William Y. and Bringmann, Roger A. and Hank, Richard E. and Hwu, Wen-Mei W. and Rau, B. Ramakrishna and Schlansker, Michael S.},
+ location = {New York, NY, USA},
+ publisher = {Association for Computing Machinery},
+ url = {https://doi.org/10.1145/161541.159765},
+ doi = {10.1145/161541.159765},
+ issn = {0734-2071},
+ journaltitle = {ACM Trans. Comput. Syst.},
+ keywords = {speculative execution,static scheduling,hyperblocks},
+ month = nov,
+ number = {4},
+ pages = {376--408},
+ title = {Sentinel Scheduling: A Model for Compiler-Controlled Speculative Execution},
+ volume = {11},
+ year = {1993}
+}
+
+@inproceedings{mahlke94_charac_impac_predic_execut_branc_predic,
+ abstract = {Branch instructions are recognized as a major impediment to exploiting instruction level parallelism. Even with sophisticated branch prediction techniques, many frequently executed branches remain difficult to predict. An architecture supporting predicated execution may allow the compiler to remove many of these hard-to-predict branches, reducing the number of branch mispredictions and thereby improving performance. We present an in-depth analysis of the characteristics of those branches which are frequently mispredicted and examine the effectiveness of an advanced compiler to eliminate these branches. Over the benchmarks studied, an average of 27% of the dynamic branches and 56% of the dynamic branch mispredictions are eliminated with predicated execution support.},
+ author = {Mahlke, Scott A. and Hank, Richard E. and Bringmann, Roger A. and Gyllenhaal, John C. and Gallagher, David M. and Hwu, Wen-mei W.},
+ location = {San Jose, California, USA},
+ publisher = {Association for Computing Machinery},
+ url = {https://doi.org/10.1145/192724.192755},
+ booktitle = {Proceedings of the 27th Annual International Symposium on Microarchitecture},
+ doi = {10.1145/192724.192755},
+ isbn = {0897917073},
+ keywords = {speculative execution,static scheduling,hyperblocks},
+ pages = {217--227},
+ series = {MICRO 27},
+ title = {Characterizing the Impact of Predicated Execution on Branch Prediction},
+ year = {1994}
}
@misc{mentor20_catap_high_level_synth,
author = {Mentor},
- title = {Catapult High-Level Synthesis},
url = {https://www.mentor.com/hls-lp/catapult-high-level-synthesis/c-systemc-hls},
+ title = {Catapult High-Level Synthesis},
urldate = {2020-06-06},
- year = 2020
+ year = {2020}
}
@inproceedings{meredith10_veril,
- author = {{Meredith}, P. and {Katelman}, M. and {Meseguer}, J. and {Ro{\c{s}}u} G.},
- title = {A formal executable semantics of {Verilog}},
- tags = {semantics},
- booktitle = {Eighth ACM/IEEE International Conference on Formal Methods and
- Models for Codesign (MEMOCODE 2010)},
- year = 2010,
- pages = {179-188},
- doi = {10.1109/MEMCOD.2010.5558634},
+ author = {{Meredith}, P. and {Katelman}, M. and {Meseguer}, J. and G., {Roşu}},
url = {https://doi.org/10.1109/MEMCOD.2010.5558634},
- month = {July}
+ booktitle = {Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010)},
+ doi = {10.1109/MEMCOD.2010.5558634},
+ month = jul,
+ pages = {179--188},
+ title = {A formal executable semantics of {Verilog}},
+ year = {2010}
}
@book{micheli94_synth_optim_digit_circuit,
author = {De Micheli, Giovanni},
- title = {Synthesis and Optimization of Digital Circuits},
- year = 1994,
publisher = {McGraw-Hill Higher Education},
edition = {1st},
- isbn = 0070163332
+ isbn = {0070163332},
+ title = {Synthesis and Optimization of Digital Circuits},
+ year = {1994}
}
@inproceedings{nigam20_predic_accel_desig_time_sensit_affin_types,
- author = {Nigam, Rachit and Atapattu, Sachille and Thomas, Samuel and Li, Zhijing and
- Bauer, Theodore and Ye, Yuwei and Koti, Apurva and Sampson, Adrian and Zhang,
- Zhiru},
- title = {Predictable Accelerator Design with Time-Sensitive Affine Types},
- booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
- and Implementation},
- year = 2020,
- pages = {393-407},
- doi = {10.1145/3385412.3385974},
- url = {https://doi.org/10.1145/3385412.3385974},
- address = {New York, NY, USA},
- isbn = 9781450376136,
- keywords = {Affine Type Systems, High-Level Synthesis},
+ author = {Nigam, Rachit and Atapattu, Sachille and Thomas, Samuel and Li, Zhijing and Bauer, Theodore and Ye, Yuwei and Koti, Apurva and Sampson, Adrian and Zhang, Zhiru},
location = {London, UK},
- numpages = 15,
publisher = {ACM},
- series = {PLDI 2020}
+ url = {https://doi.org/10.1145/3385412.3385974},
+ booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ doi = {10.1145/3385412.3385974},
+ isbn = {9781450376136},
+ keywords = {Affine Type Systems,High-Level Synthesis},
+ pages = {393--407},
+ series = {PLDI 2020},
+ title = {Predictable Accelerator Design with Time-Sensitive Affine Types},
+ year = {2020}
}
@inproceedings{nikhil04_blues_system_veril,
author = {{Nikhil}, R.},
- title = {Bluespec System Verilog: efficient, correct RTL from high level specifications},
- booktitle = {Proceedings. Second ACM and IEEE International Conference on Formal Methods and
- Models for Co-Design, 2004. MEMOCODE '04.},
- year = 2004,
- pages = {69-70},
+ url = {https://doi.org/10.1109/MEMCOD.2004.1459818},
+ booktitle = {Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04.},
doi = {10.1109/MEMCOD.2004.1459818},
- url = {https://doi.org/10.1109/MEMCOD.2004.1459818}
+ pages = {69--70},
+ title = {Bluespec System Verilog: efficient, correct RTL from high level specifications},
+ year = {2004}
}
@inproceedings{noronha17_rapid_fpga,
- keywords = {high-level synthesis, FPGA, inlining, compiler optimisation},
author = {{Noronha}, D. H. and {Pinilla}, J. P. and {Wilton}, S. J. E.},
booktitle = {2017 International Conference on ReConFigurable Computing and FPGAs (ReConFig)},
+ doi = {10.1109/RECONFIG.2017.8279807},
+ keywords = {high-level synthesis,FPGA,inlining,compiler optimisation},
+ pages = {1--6},
title = {Rapid circuit-specific inlining tuning for FPGA high-level synthesis},
- year = {2017},
- volume = {},
- number = {},
- pages = {1-6},
- doi = {10.1109/RECONFIG.2017.8279807}
+ year = {2017}
}
@inproceedings{ottenstein90_progr_depen_web,
- year = {1990},
abstract = {The Program Dependence Web (PDW) is a program representation that can be directly interpreted using control-, data-, or demand-driven models of execution. A PDW combines a single-assignment version of the program with explicit operators that manage the flow of data values. The PDW can be viewed as an augmented Program Dependence Graph. Translation to the PDW representation provides the basis for projects to compile Fortran onto dynamic dataflow architectures and simulators. A second application of the PDW is the construction of various compositional semantics for program dependence graphs.},
author = {Ottenstein, Karl J. and Ballance, Robert A. and MacCabe, Arthur B.},
location = {White Plains, New York, USA},
publisher = {Association for Computing Machinery},
url = {https://doi.org/10.1145/93542.93578},
booktitle = {Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation},
- date = {1990},
doi = {10.1145/93542.93578},
isbn = {0897913647},
keywords = {gated-SSA,SSA,program dependence graph},
pages = {257--271},
series = {PLDI '90},
- title = {The Program Dependence Web: A Representation Supporting Control-, Data-, and Demand-Driven Interpretation of Imperative Languages}
+ title = {The Program Dependence Web: A Representation Supporting Control-, Data-, and Demand-Driven Interpretation of Imperative Languages},
+ year = {1990}
}
@inproceedings{page91_compil_occam,
author = {Page, Ian and Luk, Wayne},
+ booktitle = {FPGAs, Oxford Workshop on Field Programmable Logic and Applications},
+ pages = {271--283},
title = {Compiling Occam into field-programmable gate arrays},
- booktitle = {FPGAs, Oxford Workshop on Field Programmable Logic and
- Applications},
- year = 1991,
- volume = 15,
- pages = {271--283}
+ volume = {15},
+ year = {1991}
}
@inproceedings{paulin89_sched_bindin_algor_high_level_synth,
author = {Paulin, P. G. and Knight, J. P.},
- title = {Scheduling and Binding Algorithms for High-Level Synthesis},
- booktitle = {Proceedings of the 26th ACM/IEEE Design Automation Conference},
- year = 1989,
- pages = {1-6},
- doi = {10.1145/74382.74383},
- url = {https://doi.org/10.1145/74382.74383},
- address = {New York, NY, USA},
- isbn = 0897913108,
location = {Las Vegas, Nevada, USA},
- numpages = 6,
publisher = {ACM},
- series = {DAC '89}
+ url = {https://doi.org/10.1145/74382.74383},
+ booktitle = {Proceedings of the 26th ACM/IEEE Design Automation Conference},
+ doi = {10.1145/74382.74383},
+ isbn = {0897913108},
+ pages = {1--6},
+ series = {DAC '89},
+ title = {Scheduling and Binding Algorithms for High-Level Synthesis},
+ year = {1989}
}
@inproceedings{pelcat16_desig_hdl,
- author = {Maxime Pelcat and C\'edric Bourrasset and Luca Maggiani and François Berry},
+ author = {Pelcat, Maxime and Bourrasset, Cédric and Maggiani, Luca and Berry, François},
booktitle = {2016 International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation (SAMOS)},
+ doi = {10.1109/SAMOS.2016.7818341},
+ pages = {140--147},
title = {Design productivity of a high level synthesis compiler versus HDL},
- year = {2016},
- volume = {},
- number = {},
- pages = {140-147},
- doi = {10.1109/SAMOS.2016.7818341}
+ year = {2016}
}
@article{perna11_correc_hardw_synth,
- author = "Perna, Juan and Woodcock, Jim and Sampaio, Augusto and Iyoda,
- Juliano",
+ author = {Perna, Juan and Woodcock, Jim and Sampaio, Augusto and Iyoda, Juliano},
+ date = {2011-12-01},
+ doi = {10.1007/s00236-011-0142-y},
+ issn = {1432-0525},
+ journaltitle = {Acta Informatica},
+ number = {7},
+ pages = {363--396},
title = {Correct Hardware Synthesis},
- journal = "Acta Informatica",
- volume = 48,
- number = 7,
- pages = "363--396",
- year = 2011,
- doi = "10.1007/s00236-011-0142-y",
- day = 01,
- issn = "1432-0525",
- month = "Dec"
+ volume = {48}
}
@article{perna12_mechan_wire_wise_verif_handel_c_synth,
- author = "Perna, Juan and Woodcock, Jim",
+ author = {Perna, Juan and Woodcock, Jim},
+ doi = {10.1016/j.scico.2010.02.007},
+ issn = {0167-6423},
+ journaltitle = {Science of Computer Programming},
+ number = {4},
+ pages = {424--443},
title = {Mechanised Wire-Wise Verification of {Handel-C} Synthesis},
- journal = "Science of Computer Programming",
- volume = 77,
- number = 4,
- pages = "424 - 443",
- year = 2012,
- doi = "10.1016/j.scico.2010.02.007",
- issn = "0167-6423"
+ volume = {77},
+ year = {2012}
}
@inproceedings{pilato13_bambu,
- year = {2013},
author = {{Pilato}, C. and {Ferrandi}, F.},
booktitle = {2013 23rd International Conference on Field programmable Logic and Applications},
- date = {2013},
doi = {10.1109/FPL.2013.6645550},
pages = {1--4},
- title = {Bambu: A modular framework for the high level synthesis of memory-intensive applications}
+ title = {Bambu: A modular framework for the high level synthesis of memory-intensive applications},
+ year = {2013}
}
@inproceedings{pnueli98_trans,
- author = "Pnueli, A. and Siegel, M. and Singerman, E.",
- title = "Translation validation",
- booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
- year = 1998,
- pages = "151--166",
- address = "Berlin, Heidelberg",
- editor = "Steffen, Bernhard",
- isbn = "978-3-540-69753-4",
- publisher = "Springer",
- doi = "10.1007/BFb0054170"
-}
-
-@INPROCEEDINGS{poly_hls_zhao2017,
+ author = {Pnueli, A. and Siegel, M. and Singerman, E.},
+ editor = {Steffen, Bernhard},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer},
+ booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
+ doi = {10.1007/BFb0054170},
+ isbn = {978-3-540-69753-4},
+ pages = {151--166},
+ title = {Translation validation},
+ year = {1998}
+}
+
+@inproceedings{poly_hls_zhao2017,
author = {Zhao, Jieru and Feng, Liang and Sinha, Sharad and Zhang, Wei and Liang, Yun and He, Bingsheng},
booktitle = {2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
+ doi = {10.1109/ICCAD.2017.8203809},
+ pages = {430--437},
title = {COMBA: A comprehensive model-based analysis framework for high level synthesis of real applications},
- year = {2017},
- volume = {},
- number = {},
- pages = {430-437},
- doi = {10.1109/ICCAD.2017.8203809}
+ year = {2017}
}
@inproceedings{poly_hls_zuo2013,
- title = {Improving polyhedral code generation for high-level synthesis},
- author = {Zuo, Wei and Li, Peng and Chen, Deming and Pouchet, Louis-No{\"e}l and Zhong, Shunan and Cong, Jason},
+ author = {Zuo, Wei and Li, Peng and Chen, Deming and Pouchet, Louis-Noël and Zhong, Shunan and Cong, Jason},
+ organization = {IEEE},
booktitle = {2013 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ ISSS)},
+ doi = {https://doi.org/10.1109/CODES-ISSS.2013.6659002},
pages = {1--10},
- year = {2013},
- organization = {IEEE},
- doi = {https://doi.org/10.1109/CODES-ISSS.2013.6659002}
+ title = {Improving polyhedral code generation for high-level synthesis},
+ year = {2013}
}
@inproceedings{pouchet13_polyh,
- title = {Polyhedral-based data reuse optimization for configurable computing},
author = {Pouchet, Louis-Noel and Zhang, Peng and Sadayappan, Ponnuswamy and Cong, Jason},
booktitle = {Proceedings of the ACM/SIGDA international symposium on Field programmable gate arrays},
+ doi = {https://doi.org/10.1145/2435264.2435273},
pages = {29--38},
- year = {2013},
- doi = {https://doi.org/10.1145/2435264.2435273}
+ title = {Polyhedral-based data reuse optimization for configurable computing},
+ year = {2013}
}
@inproceedings{schuiki20_llhd,
author = {Schuiki, Fabian and Kurth, Andreas and Grosser, Tobias and Benini, Luca},
- title = {LLHD: A Multi-Level Intermediate Representation for Hardware Description
- Languages},
- booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
- and Implementation},
- year = 2020,
- pages = {258-271},
- doi = {10.1145/3385412.3386024},
- url = {https://doi.org/10.1145/3385412.3386024},
- address = {New York, NY, USA},
- isbn = 9781450376136,
location = {London, UK},
- numpages = 14,
publisher = {ACM},
- series = {PLDI 2020}
+ url = {https://doi.org/10.1145/3385412.3386024},
+ booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ doi = {10.1145/3385412.3386024},
+ isbn = {9781450376136},
+ pages = {258--271},
+ series = {PLDI 2020},
+ title = {LLHD: A Multi-Level Intermediate Representation for Hardware Description Languages},
+ year = {2020}
}
@article{sevcik13_compc,
- author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
- title = {CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency},
- year = {2013},
- issue_date = {June 2013},
+ abstract = {In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.},
+ author = {Ševčı́k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
+ location = {New York, NY, USA},
publisher = {ACM},
- address = {New York, NY, USA},
- volume = {60},
- number = {3},
- issn = {0004-5411},
url = {https://doi.org/10.1145/2487241.2487248},
doi = {10.1145/2487241.2487248},
- abstract = {In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.},
- journal = {J. ACM},
+ issn = {0004-5411},
+ journaltitle = {J. ACM},
+ keywords = {semantics,Relaxed memory models,verified compilation},
month = jun,
- articleno = {22},
- numpages = {50},
- keywords = {semantics, Relaxed memory models, verified compilation}
+ number = {3},
+ title = {CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency},
+ volume = {60},
+ year = {2013}
}
@article{six20_certif_effic_instr_sched,
- year = {2020},
abstract = {CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with sequential semantics, and did not attempt reordering instructions for optimization. We present here a CompCert backend for a VLIW core (i.e. with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.},
author = {Six, Cyril and Boulmé, Sylvain and Monniaux, David},
location = {New York, NY, USA},
publisher = {Association for Computing Machinery},
url = {https://doi.org/10.1145/3428197},
- date = {2020-11},
doi = {10.1145/3428197},
journaltitle = {Proc. ACM Program. Lang.},
keywords = {coq,translation validation,scheduling,static scheduling,verification,VLIW,operational semantics},
+ month = nov,
number = {OOPSLA},
title = {Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors},
- volume = {4}
+ volume = {4},
+ year = {2020}
}
@unpublished{six21_verif_super_sched_relat_optim,
- year = {2021},
author = {Six, Cyril and Gourdin, Léo and Boulmé, Sylvain and Monniaux, David},
url = {https://hal.archives-ouvertes.fr/hal-03200774},
- date = {2021-04},
file = {https://hal.archives-ouvertes.fr/hal-03200774/file/hal_prepass_scheduling.pdf},
keywords = {coq,translation validation,scheduling,static scheduling,verification,VLIW,operational semantics},
+ month = apr,
note = {working paper or preprint},
- title = {{Verified Superblock Scheduling with Related Optimizations}}
+ title = {{Verified Superblock Scheduling with Related Optimizations}},
+ year = {2021}
}
@inproceedings{six22_formal_verif_super_sched,
- author = {Six, Cyril and Gourdin, L\'{e}o and Boulm\'{e}, Sylvain and Monniaux, David and Fasse, Justus and Nardino, Nicolas},
- title = {Formally Verified Superblock Scheduling},
- year = {2022},
- isbn = {9781450391825},
+ abstract = {On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks (it may move instructions across branches), along with its performance evaluation. It is integrated within the CompCert C compiler, providing a complete machine-checked proof of semantic preservation from C to assembly. Our optimizer composes several passes designed by translation validation: program transformations are proposed by untrusted oracles, which are then validated by certified and scalable checkers. Our main checker is an architecture-independent simulation-test over superblocks modulo register liveness, which relies on hash-consed symbolic execution.},
+ author = {Six, Cyril and Gourdin, Léo and Boulmé, Sylvain and Monniaux, David and Fasse, Justus and Nardino, Nicolas},
+ location = {Philadelphia, PA, USA},
publisher = {Association for Computing Machinery},
- address = {New York, NY, USA},
url = {https://doi.org/10.1145/3497775.3503679},
- doi = {10.1145/3497775.3503679},
- abstract = {On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks (it may move instructions across branches), along with its performance evaluation. It is integrated within the CompCert C compiler, providing a complete machine-checked proof of semantic preservation from C to assembly. Our optimizer composes several passes designed by translation validation: program transformations are proposed by untrusted oracles, which are then validated by certified and scalable checkers. Our main checker is an architecture-independent simulation-test over superblocks modulo register liveness, which relies on hash-consed symbolic execution.},
booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs},
- pages = {40–54},
- numpages = {15},
- keywords = {Symbolic execution, Instruction-level parallelism, Translation validation, the COQ proof assistant},
- location = {Philadelphia, PA, USA},
- series = {CPP 2022}
+ doi = {10.1145/3497775.3503679},
+ isbn = {9781450391825},
+ keywords = {Symbolic execution,Instruction-level parallelism,Translation validation,the COQ proof assistant},
+ pages = {40--54},
+ series = {CPP 2022},
+ title = {Formally Verified Superblock Scheduling},
+ year = {2022}
}
@inproceedings{slind08_brief_overv_hol4,
- author = "Slind, Konrad and Norrish, Michael",
- title = "A Brief Overview of {HOL4}",
- booktitle = "Theorem Proving in Higher Order Logics",
- year = 2008,
- pages = "28--32",
- address = "Berlin, Heidelberg",
- editor = "Mohamed, Otmane Ait and Mu{\~{n}}oz, C{\'e}sar and Tahar, Sofi{\`e}ne",
- isbn = "978-3-540-71067-7",
+ author = {Slind, Konrad and Norrish, Michael},
+ editor = {Mohamed, Otmane Ait and Muñoz, César and Tahar, Sofiène},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer Berlin Heidelberg},
+ booktitle = {Theorem Proving in Higher Order Logics},
+ isbn = {978-3-540-71067-7},
keywords = {theorem proving;HOL},
- publisher = "Springer Berlin Heidelberg"
+ pages = {28--32},
+ title = {A Brief Overview of {HOL4}},
+ year = {2008}
}
@inproceedings{spatial,
- author = {David Koeplinger and
- Matthew Feldman and
- Raghu Prabhakar and
- Yaqi Zhang and
- Stefan Hadjis and
- Ruben Fiszel and
- Tian Zhao and
- Luigi Nardi and
- Ardavan Pedram and
- Christos Kozyrakis and
- Kunle Olukotun},
- title = {Spatial: A Language and Compiler for Application Accelerators},
+ author = {Koeplinger, David and Feldman, Matthew and Prabhakar, Raghu and Zhang, Yaqi and Hadjis, Stefan and Fiszel, Ruben and Zhao, Tian and Nardi, Luigi and Pedram, Ardavan and Kozyrakis, Christos and Olukotun, Kunle},
+ publisher = {ACM},
booktitle = {{PLDI}},
+ doi = {https://doi.org/10.1145/3192366.3192379},
pages = {296--311},
- publisher = {{ACM}},
- year = {2018},
- doi = {https://doi.org/10.1145/3192366.3192379}
+ title = {Spatial: A Language and Compiler for Application Accelerators},
+ year = {2018}
}
@article{takach16_high_level_synth,
- author = {A. {Takach}},
- title = {High-Level Synthesis: Status, Trends, and Future
- Directions},
- journal = {IEEE Design Test},
- volume = {33},
- number = {3},
- pages = {116-124},
- year = {2016},
- doi = {10.1109/MDAT.2016.2544850},
+ author = {{Takach}, A.},
url = {https://doi.org/10.1109/MDAT.2016.2544850},
- ISSN = {2168-2364},
- month = {June}
+ doi = {10.1109/MDAT.2016.2544850},
+ issn = {2168-2364},
+ journaltitle = {IEEE Design Test},
+ month = jun,
+ number = {3},
+ pages = {116--124},
+ title = {High-Level Synthesis: Status, Trends, and Future Directions},
+ volume = {33},
+ year = {2016}
}
@inproceedings{tristan08_formal_verif_trans_valid,
author = {Tristan, Jean-Baptiste and Leroy, Xavier},
- title = {Formal Verification of Translation Validators: A Case Study on
- Instruction Scheduling Optimizations},
- booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on
- Principles of Programming Languages},
- year = 2008,
- pages = {17-27},
- doi = {10.1145/1328438.1328444},
- address = {New York, NY, USA},
- isbn = 9781595936899,
location = {San Francisco, California, USA},
- numpages = 11,
publisher = {ACM},
- series = {POPL '08}
+ booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ doi = {10.1145/1328438.1328444},
+ isbn = {9781595936899},
+ pages = {17--27},
+ series = {POPL '08},
+ title = {Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations},
+ year = {2008}
}
@inproceedings{tristan10_simpl_verif_valid_softw_pipel,
@@ -1299,129 +1197,109 @@ and Morawiec, Adam",
publisher = {Association for Computing Machinery},
url = {https://doi.org/10.1145/1706299.1706311},
booktitle = {Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
- year = {2010},
doi = {10.1145/1706299.1706311},
isbn = {9781605584799},
keywords = {symbolic execution,coq,verification,translation validation,loop scheduling,compiler optimisation,software pipelining},
pages = {83--92},
series = {POPL '10},
- title = {A Simple, Verified Validator for Software Pipelining}
+ title = {A Simple, Verified Validator for Software Pipelining},
+ year = {2010}
}
@inproceedings{venkataramani07_operat,
- keywords = {operation chaining},
- author = {Girish Venkataramani and Goldstein, Seth C.},
+ author = {Venkataramani, Girish and Goldstein, Seth C.},
booktitle = {2007 IEEE/ACM International Conference on Computer-Aided Design},
+ doi = {10.1109/ICCAD.2007.4397305},
+ keywords = {operation chaining},
+ pages = {442--449},
title = {Operation chaining asynchronous pipelined circuits},
- year = {2007},
- volume = {},
- number = {},
- pages = {442-449},
- doi = {10.1109/ICCAD.2007.4397305}
+ year = {2007}
}
@article{wang20_compc,
+ abstract = {We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files. CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units. We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files.},
author = {Wang, Yuting and Xu, Xiangzhe and Wilke, Pierre and Shao, Zhong},
- title = {CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files},
- year = {2020},
- issue_date = {November 2020},
+ location = {New York, NY, USA},
publisher = {ACM},
- address = {New York, NY, USA},
- volume = {4},
- number = {OOPSLA},
url = {https://doi.org/10.1145/3428265},
doi = {10.1145/3428265},
- abstract = { We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files. CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units. We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files. },
- journal = {Proc. ACM Program. Lang.},
+ journaltitle = {Proc. ACM Program. Lang.},
+ keywords = {Generation of Object Files,Assembler Verification,Verified Separate Compilation},
month = nov,
- articleno = {197},
- numpages = {28},
- keywords = {Generation of Object Files, Assembler Verification, Verified Separate Compilation}
+ number = {OOPSLA},
+ title = {CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files},
+ volume = {4},
+ year = {2020}
}
@misc{wolf_yosys_open_synth_suite,
- author = {Clifford Wolf},
- title = {{Yosys Open SYnthesis Suite}},
+ author = {Wolf, Clifford},
url = {https://bit.ly/2kAXg0q},
+ title = {{Yosys Open SYnthesis Suite}},
urldate = {2019-01-11},
- year = 2019
+ year = {2019}
}
@misc{xilinx20_vivad_high_synth,
author = {Xilinx},
- title = {Vivado High-level Synthesis},
url = {https://bit.ly/39ereMx},
+ title = {Vivado High-level Synthesis},
urldate = {2020-07-20},
- year = 2020
+ year = {2020}
}
@misc{xilinx_vivad_desig_suite,
author = {Xilinx},
- title = {{Vivado Design Suite}},
url = {https://bit.ly/2wZAmld},
+ title = {{Vivado Design Suite}},
urldate = {2019-01-14},
- year = 2019
+ year = {2019}
}
@misc{xilinx_xst_synth_overv,
author = {Xilinx},
- title = {{XST} Synthesis Overview},
url = {https://bit.ly/2lGtkjL},
+ title = {{XST} Synthesis Overview},
urldate = {2019-01-11},
- year = 2019
+ year = {2019}
}
@inproceedings{yang11_findin_under_bugs_c_compil,
author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
- title = {Finding and Understanding Bugs in {C} Compilers},
- booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design
- and Implementation},
- year = 2011,
- pages = {283-294},
- doi = {10.1145/1993498.1993532},
- url = {https://doi.org/10.1145/1993498.1993532},
- address = {New York, NY, USA},
- isbn = 9781450306638,
- keywords = {random program generation, random testing, automated testing, compiler testing,
- compiler defect},
location = {San Jose, California, USA},
- numpages = 12,
publisher = {ACM},
- series = {PLDI '11}
+ url = {https://doi.org/10.1145/1993498.1993532},
+ booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ doi = {10.1145/1993498.1993532},
+ isbn = {9781450306638},
+ keywords = {random program generation,random testing,automated testing,compiler testing,compiler defect},
+ pages = {283--294},
+ series = {PLDI '11},
+ title = {Finding and Understanding Bugs in {C} Compilers},
+ year = {2011}
}
@inproceedings{zhao12_formal_llvm_inter_repres_verif_progr_trans,
- author = {Jianzhou Zhao and
- Santosh Nagarakatte and
- Milo M. K. Martin and
- Steve Zdancewic},
- editor = {John Field and
- Michael Hicks},
- title = {Formalizing the {LLVM} intermediate representation for verified program
- transformations},
- booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
- of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania,
- USA, January 22-28, 2012},
- pages = {427--440},
- publisher = {{ACM}},
- year = {2012},
+ author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M. K. and Zdancewic, Steve},
+ editor = {Field, John and Hicks, Michael},
+ publisher = {ACM},
url = {https://doi.org/10.1145/2103656.2103709},
+ booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012},
doi = {10.1145/2103656.2103709},
- timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
- biburl = {https://dblp.org/rec/conf/popl/ZhaoNMZ12.bib},
- bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@InProceedings{zhu13_mechan_approac_linkin_operat_seman,
- author = "Zhu, Huibiao and Liu, Peng and He, Jifeng and Qin, Shengchao",
- title = "Mechanical Approach to Linking Operational Semantics and Algebraic Semantics
- for Verilog Using Maude",
- booktitle = "Unifying Theories of Programming",
- year = 2013,
- pages = "164--185",
- address = "Berlin, Heidelberg",
- editor = "Wolff, Burkhart and Gaudel, Marie-Claude and Feliachi, Abderrahmane",
- isbn = "978-3-642-35705-3",
- publisher = "Springer Berlin Heidelberg"
+ pages = {427--440},
+ title = {Formalizing the {LLVM} intermediate representation for verified program transformations},
+ year = {2012}
+}
+
+@inproceedings{zhu13_mechan_approac_linkin_operat_seman,
+ author = {Zhu, Huibiao and Liu, Peng and He, Jifeng and Qin, Shengchao},
+ editor = {Wolff, Burkhart and Gaudel, Marie-Claude and Feliachi, Abderrahmane},
+ location = {Berlin, Heidelberg},
+ publisher = {Springer Berlin Heidelberg},
+ booktitle = {Unifying Theories of Programming},
+ isbn = {978-3-642-35705-3},
+ pages = {164--185},
+ title = {Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude},
+ year = {2013}
}
diff --git a/title.tex b/title.tex
index 8c59a5e..4571680 100644
--- a/title.tex
+++ b/title.tex
@@ -6,9 +6,9 @@
\definemakeup[title][align=middle]
\startmakeup[title]
- {\switchtobodyfont[30pt] Formal Verification of \blank[medium] High-Level Synthesis}
+ {\switchtobodyfont[30pt,ss] Formal Verification of \blank[medium] High-Level Synthesis}
\blank[1cm]
- {\bfb Late Stage Review}
+ {\bfb\ss Late Stage Review}
\blank[2cm]
{\rma Yann Herklotz Grave}
\blank[5cm]
generated by cgit (git 2.34.1) at 2024-04-29 08:50:35 +0000