diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-19 01:46:11 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-19 01:46:11 +0100 |
| commit | 04f1a0ed87c2d95ec977ac03d20bda02dc313d08 (patch) | |
| tree | c07c61cb0b0039b1efde22e199e242651e002919 | |
| parent | 7e4c8a22030c30f8cca793d91ec27cdd5d4ef8b3 (diff) | |
| download | vericert-docs-04f1a0ed87c2d95ec977ac03d20bda02dc313d08.tar.gz vericert-docs-04f1a0ed87c2d95ec977ac03d20bda02dc313d08.zip | |
Add random
| -rw-r--r-- | documentation.org | 34 |
1 files changed, 33 insertions, 1 deletions
diff --git a/documentation.org b/documentation.org index c8cf73d..f86be91 100644 --- a/documentation.org +++ b/documentation.org @@ -5,7 +5,6 @@ * Vericert :PROPERTIES: :EXPORT_FILE_NAME: _index -:EXPORT_DATE: <2021-01-16 Sat> :END: A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]]. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness. @@ -188,6 +187,38 @@ $ echo $? 50 #+end_src +** Scheduling +:PROPERTIES: +:EXPORT_FILE_NAME: scheduling +:EXPORT_HUGO_SECTION: docs +:END: + +Scheduling + +** If-conversion +:PROPERTIES: +:EXPORT_FILE_NAME: if-conversion +:EXPORT_HUGO_SECTION: docs +:END: + +If-conversion + +** Loop pipelining +:PROPERTIES: +:EXPORT_FILE_NAME: loop-pipelining +:EXPORT_HUGO_SECTION: docs +:END: + +Loop pipelining + +** Functions +:PROPERTIES: +:EXPORT_FILE_NAME: function-support +:EXPORT_HUGO_SECTION: docs +:END: + +Functions. + * Coq Style Guide :PROPERTIES: :CUSTOM_ID: coq-style-guide @@ -550,3 +581,4 @@ A small standalone Coq file that exhibits many of the style points. Notation "x '##'" := (bar x x) (at level 40) : Z_scope. End BarNotations. #+end_src + |