diff options
Diffstat (limited to 'verified_resource_sharing.tex')
| -rw-r--r-- | verified_resource_sharing.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index c47cf66..7f5f57c 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -418,7 +418,7 @@ stack is proven correct. Proofs of the load and store instructions are not quit additional invariants need to be proven to hold for those instructions. The pass that renames variables in HTL is yet to be proven, as is the pass that generates the final Verilog. -To give a rough idea of the scale and complexity of the task: the implementation of \vericertfun{} involved the addition of about \MP{\ref{???}} lines of Coq code to \vericert{} and took the first author \MP{\ref{???}} months. The correctness proof, so far, has taken \MP{\ref{???}} lines of Coq code and \MP{\ref{???}} months. +To give a rough idea of the scale and complexity of the task: the implementation of \vericertfun{} involved adding or changing about 700 lines of Coq code in \vericert{} and took the first author 4 months. The correctness proof, so far, has required about 2300 lines of additions or changes to the Coq code and 8 months. \section{Performance evaluation} |