diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-11 15:58:09 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-11 16:55:51 +0100 |
| commit | f1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a (patch) | |
| tree | 096bb355bcbb3b465bd531cc793f7391e2c49d83 /reviews | |
| parent | 9c107a5bd8330ca9b5b6bdadf715b2a48dda1489 (diff) | |
| download | oopsla21_fvhls-f1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a.tar.gz oopsla21_fvhls-f1e4ebdba3c05e1c5d83eeb338c62fc3227b1a1a.zip | |
Add new results
Diffstat (limited to 'reviews')
| -rw-r--r-- | reviews/pldi.org | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/reviews/pldi.org b/reviews/pldi.org index 2f14d3e..5522a4a 100644 --- a/reviews/pldi.org +++ b/reviews/pldi.org @@ -25,7 +25,7 @@ topics" :PROPERTIES: :CUSTOM_ID: paper-summary :END: -"High-level synthesis" (HSL) is a term of art for compiling C programs +"High-level synthesis" (HLS) is a term of art for compiling C programs to hardware designs. This paper presents the first mechanized proof of soundness for an HLS compiler. The implementation and proof are carried out in Coq and build on CompCert, targeting Verilog. Evaluation shows |