Formal verification of high-level synthesis

I, Yann Herklotz Grave, declare that the work presented in this thesis is my own, and that any other work has been appropriately referenced. Abbreviations ALAP as late as possible ASAP as soon as possible ASIC application-specific integrated circuit Asm CompCert assembly language AsmBlock CompCert KVX assembly block language AST abstract syntax tree BRAM block random-access memory Btl block transfer language C#minor CompCert intermediate language CDFG control-and data-flow graph CFG control-flow graph Clight CompCert intermediate language Cminor CompCert intermediate language CminorSel CompCert intermediate language CPU central processing unit DFG data-flow graph DRAM dynamic random-access memory DSL domain-specific language Abbreviations DSP digital signal processor FPGA field-programmable gate array FSM finite-state machine FSMD finite-state machine with data path GPU graphics processing unit HDL hardware description language HLS high-level synthesis IP core intellectual property core IR intermediate representation LP linear programming LSQ load-store queue Ltl linear transfer language LUT look-up table Mach CompCert intermediate language Rtl register transfer language SAT satisfiability SDC system of difference constraints SMT satisfiability modulo theories SSA static single assignment VLIW very large instruction word 1.3 Publications OOPSLA 2021 Next, we introduce Vericert and describe an initial translation from C

to Verilog using CompCert, without optimisations. This article is the basis for the dissertation, making up parts of chapters 3, 4 and 6.