From 659c8340a4f07b2afabca7f3d0168804c60d4bba Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 29 Sep 2021 19:50:04 +0100 Subject: Update the presentation --- presentation/presentation.org | 164 +++++++++++++++++++++++------------------- presentation/presentation.pdf | Bin 2282809 -> 2299308 bytes 2 files changed, 90 insertions(+), 74 deletions(-) (limited to 'presentation') diff --git a/presentation/presentation.org b/presentation/presentation.org index 3786da0..9465196 100644 --- a/presentation/presentation.org +++ b/presentation/presentation.org @@ -300,8 +300,6 @@ Use CompCert, a fully verified C compiler, and add an HLS backend. :BEAMER_ACT: <2> :END: -Current progress: fully verified HLS tool for a subset of C. - Support for: all *control flow*, *fixedpoint*, *non-recursive functions* and *local arrays/structs/unions*. * Example @@ -370,7 +368,7 @@ main() { } #+end_src -** Example: HTL Overview :noexport: +** Example: HTL Overview The representation of the *finite state-machine with datapath (FSMD)* is abstract and called **HTL**. @@ -411,8 +409,8 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da #+attr_beamer: :overlay <+-> - *Control-flow* is translated into a *finite state-machine*. - Each *3AC instructions* translated into equivalent *Verilog statements*. -- Function *stack* implemented as *RAM*. -- Pointers for loads and stores translated to RAM addresses. +- Function *stack* implemented as *Verilog array*. +- Pointers for loads and stores translated to array addresses. - *Byte* addressed to *word* addressed. #+beamer: \vspace{1em} @@ -429,7 +427,7 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da :BEAMER_ACT: 3 :END: -~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ ~reg_3 <= {reg_3 + {reg_5 + 32'd0}}~ +~x3 = x3 + x5 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{reg_3 <= {reg_3 + {reg_5 + 32'd0}}} **** Only 2 :B_onlyenvNH: :PROPERTIES: @@ -437,18 +435,16 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da :BEAMER_ACT: 5-6 :END: -~x5 + x1 * 4 + 0~ - -$\quad\longrightarrow\quad$ ~{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}~ +~x5 + x1 * 4 + 0~ $\quad\longrightarrow\quad$ src_verilog[:exports code]{{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}} -** Example: Memory Inference Pass :noexport: +** Example: Memory Inference Pass - An HTL $\rightarrow$ HTL translation removes loads and stores. - Replaced by accesses to a proper *RAM*. #+beamer: \vspace{1em} -~stack[{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]~ +src_verilog[:exports code]{stack[{{{reg_5 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}]} #+beamer: \vspace{1em} @@ -463,6 +459,69 @@ u_en <= ( ~ u_en); wr_en <= 32'd0; addr <= {{{reg_3 + 32'd0} + {reg_1 * 32'd4}} / 32'd4}; #+end_src +** Verilog Syntax + +*** Column 1 :B_column: +:PROPERTIES: +:BEAMER_COL: 0.45 +:END: + +**** No highlight :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <1> +:END: + +#+attr_latex: :options fontsize=\footnotesize +#+begin_src verilog +module top(input clk, input [31:0] in1, + output reg [31:0] out1); + reg [31:0] reg_1, tmp; + + always @(posedge clk) begin + reg1 <= in1; + end + + always @(posedge clk) begin + tmp = reg1; + out1 <= tmp; + end +endmodule +#+end_src + +**** Highlight :B_onlyenvNH: +:PROPERTIES: +:BEAMER_env: onlyenvNH +:BEAMER_ACT: <2> +:END: + +#+attr_latex: :options highlightlines={5-7,9-12},fontsize=\footnotesize +#+begin_src verilog +module top(input clk, input [31:0] in1, + output reg [31:0] out1); + reg [31:0] reg_1, tmp; + + always @(posedge clk) begin + reg1 <= in1; + end + + always @(posedge clk) begin + tmp = reg1; + out1 <= tmp; + end +endmodule +#+end_src + +*** Column 2 +:PROPERTIES: +:BEAMER_COL: 0.55 +:END: + +#+attr_beamer: :overlay <+-> +- Verilog example for a simple shift register. +- Always block run in parallel + + ** Example: Translation (HTL $\rightarrow$ Verilog) :B_frame: *** Column @@ -630,68 +689,6 @@ endmodule - Control logic is translated into another case statement with a reset. * Verification -** Verilog Syntax - -*** Column 1 :B_column: -:PROPERTIES: -:BEAMER_COL: 0.45 -:END: - -**** No highlight :B_onlyenvNH: -:PROPERTIES: -:BEAMER_env: onlyenvNH -:BEAMER_ACT: <1> -:END: - -#+attr_latex: :options fontsize=\small -#+begin_src verilog -module top(input clk, input [31:0] in1, - output reg [31:0] out1); - reg [31:0] reg_1, tmp; - - always @(posedge clk) begin - reg1 <= in1; - end - - always @(posedge clk) begin - tmp = reg1; - out1 <= tmp; - end -endmodule -#+end_src - -**** Highlight :B_onlyenvNH: -:PROPERTIES: -:BEAMER_env: onlyenvNH -:BEAMER_ACT: <2> -:END: - -#+attr_latex: :options highlightlines={5-7,9-12},fontsize=\small -#+begin_src verilog -module top(input clk, input [31:0] in1, - output reg [31:0] out1); - reg [31:0] reg_1, tmp; - - always @(posedge clk) begin - reg1 <= in1; - end - - always @(posedge clk) begin - tmp = reg1; - out1 <= tmp; - end -endmodule -#+end_src - -*** Column 2 -:PROPERTIES: -:BEAMER_COL: 0.55 -:END: - -#+attr_beamer: :overlay <+-> -- Verilog example for a simple shift register. -- Always block run in parallel - ** Verilog Semantics (Adapted from Lööw et al. (2019)) - Top-level semantics are *small-step operational semantics*. @@ -956,6 +953,25 @@ Prove the simulation diagram correct: - there exists 1 or more steps in Verilog, - such that after 1 step in 3AC, the resulting states match. +** Main Challenges in Proof + +*** Translation of memory model +:PROPERTIES: +:BEAMER_ENV: block +:BEAMER_ACT: <1-> +:END: + +*Abstract/infinite memory model* translated into *concrete/finite RAM*. + +*** Integration of Verilog Semantics +:PROPERTIES: +:BEAMER_ENV: block +:BEAMER_ACT: <2-> +:END: + +- *Verilog semantics* differs from CompCert's main assumptions of intermediate language semantics. +- Abstract values like the *program counter* now correspond to *values in registers*. + * Results ** With Division approximately 27$\times$ slower @@ -1117,7 +1133,7 @@ Fuzzed Vericert with Csmith to check correctness theorem. Written a formally verified high-level synthesis tool in *Coq* based on *CompCert*. #+attr_beamer: :overlay <+-> -- Base translation *proven correct* by proving translation of CFG into FSMD. +- HLS tool *proven correct in Coq* by proving translation of CFG into FSMD. - Small optimisations implemented such as *Ram Inference*. - Performance without divisions comparable to LegUp without optimisations. diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf index 74f3beb..b491429 100644 Binary files a/presentation/presentation.pdf and b/presentation/presentation.pdf differ -- cgit