From cd960912fc526bcca77108f7a9756cd48de0476f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 19 Apr 2022 09:51:33 +0100 Subject: Add changes --- bibliography.bib | 2 +- chapters/hls.tex | 4 ++-- lsr_env.tex | 5 +++-- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/bibliography.bib b/bibliography.bib index a04d5a0..2d4720c 100644 --- a/bibliography.bib +++ b/bibliography.bib @@ -451,7 +451,7 @@ and Morawiec, Adam", url = {https://doi.org/10.1145/3485494}, date = {2021-10}, doi = {10.1145/3485494}, - journaltitle = {Proc. ACM Program. Lang.}, + journal = {Proceedings of the ACM on Programming Languages}, keywords = {high-level synthesis,Coq,Verilog,CompCert,C}, number = {OOPSLA}, title = {Formal Verification of High-Level Synthesis}, diff --git a/chapters/hls.tex b/chapters/hls.tex index fafb815..1276450 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -11,8 +11,8 @@ \startsynopsis This chapter outlines the base implementation of a formally verified high-level synthesis tool - called Vericert~\citef{herklotz21_veric}. This chapter is based on a paper describing the initial - implementation in detail~\citef{herklotz21_formal_verif_high_level_synth}. + called Vericert. This chapter is based on a paper describing the initial implementation in + detail~\citef{herklotz21_formal_verif_high_level_synth}. \stopsynopsis We have designed a new HLS tool in the Coq theorem prover and proved that any output design it diff --git a/lsr_env.tex b/lsr_env.tex index 547f786..0f6c356 100644 --- a/lsr_env.tex +++ b/lsr_env.tex @@ -27,9 +27,10 @@ % Layout % ========================================================================== \setuppapersize[A4][A4] +\definefontfeature [default][default][protrusion=quality,expansion=quality] +\setupalign[hz,hanging,lesshyphenation,verytolerant] \setupbodyfont[ebgaramondlato,11pt] %\setupalign[hz,hanging,nothyphenated] -\setupalign[hz,hanging,lesshyphenation,verytolerant] \setupinterlinespace[big] \setuppagenumbering[location=none] @@ -37,7 +38,7 @@ \setuplayout[ edgedistance=1cm, backspace=2cm, - rightmargin=5cm, + rightmargin=4.5cm, leftmargin=0cm, topspace=1cm, header=1cm, -- cgit