diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-10 18:38:04 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-10 18:38:04 +0100 |
| commit | 4d019a44c0fc9d78dd498d4775d904f6a846d29f (patch) | |
| tree | fed749efbc0fc9416bdd23cd2cae04e9cfe40e74 /limitations.tex | |
| parent | a84ed32608424bfc9d941caf49c45b9f643120b4 (diff) | |
| download | oopsla21_fvhls-4d019a44c0fc9d78dd498d4775d904f6a846d29f.tar.gz oopsla21_fvhls-4d019a44c0fc9d78dd498d4775d904f6a846d29f.zip | |
Some final changes
Diffstat (limited to 'limitations.tex')
| -rw-r--r-- | limitations.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/limitations.tex b/limitations.tex index a470028..cedd3b4 100644 --- a/limitations.tex +++ b/limitations.tex @@ -38,7 +38,7 @@ The introduction of pipelined operators to \vericert{}, especially for division, \paragraph{Limitations with I/O} -\vericert{} is currently limited in terms of I/O because the main function cannot accept any arguments if the Clight program is to be well-formed.\footnote{Technically, \vericert{} (and indeed, \compcert{}) can compile main functions that have arbitrary arguments and will handle those inputs appropriately, but the correctness theorem offers no guarantees about such programs.} Moreover, external function calls that produce traces have not been implemented yet, but once they have, they could enable the C program to read and write values on a bus that is shared with various other components in the hardware design. +\vericert{} is currently limited in terms of I/O because the main function cannot accept any arguments if the Clight program is to be well-formed.\footnote{Technically, \vericert{} (and indeed, \compcert{}) can compile main functions that have arbitrary arguments and will handle those inputs appropriately, but the correctness theorem offers no guarantees about such programs.} Moreover, external function calls that produce traces have not been implemented yet, but these could enable the C program to read and write values on a bus that is shared with various other components in the hardware design. \paragraph{Lack of support for global variables} In \compcert{}, each global variable is stored in its own memory. A generalisation of our translation of the stack into a RAM block could therefore translate global variables in the same manner. This would require a slight generalisation of pointers so that they store provenance information to ensure that each pointer accesses the right RAM. It would also be necessary to generalise the RAM interface so that it decodes the provenance information and indexes the correct array. |