From 2bf1ff846a792ef3007fa1e97928697509f318f7 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 15 Apr 2021 10:38:53 +0100
Subject: Update the table

---
 results/results.org | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'results')

diff --git a/results/results.org b/results/results.org
index 741a1ee..264fd0a 100644
--- a/results/results.org
+++ b/results/results.org
@@ -607,3 +607,37 @@
 |----------------+------------+-------------+---------------+---------------------|
 | median         |  1.0575184 |  0.91083941 |     1.0246082 |          0.99245744 |
 #+TBLFM: @2$1..@-2$1='(identity remote(vericert-div,@@#$1))::@2$2..@-2$2=(remote(vericert-div,@@#$3))/(remote(legup-div,@@#$3))::@2$3..@-2$3=(remote(legup-noopt-div,@@#$3))/(remote(legup-div,@@#$3))::@2$4..@-2$4=(remote(legup-nochain-div,@@#$3))/(remote(legup-div,@@#$3))::@2$5..@-2$5=(remote(legup-noopt-nochain-div,@@#$3))/(remote(legup-div,@@#$3))::@27$2..@27$5=vmedian(@2$$#..@-2$$#)
+
+* Code count
+
+| File                    | Theorem | Code | Spec | Total |
+|-------------------------+---------+------+------+-------|
+| Compiler.v              |     180 |  132 |    0 |   312 |
+| HLSOpts.v               |       0 |    2 |    0 |     2 |
+| VericertClFlags.ml      |       0 |    9 |    0 |     9 |
+| common/IntegerExtra.v   |     587 |   98 |   15 |   700 |
+| common/Maps.v           |       0 |   32 |    0 |    32 |
+| common/Monad.v          |       0 |   35 |    0 |    35 |
+| common/Show.v           |       0 |   42 |    0 |    42 |
+| common/Statemonad.v     |       0 |   46 |    0 |    46 |
+| common/Vericertlib.v    |     124 |   51 |    0 |   175 |
+| common/ZExtra.v         |     258 |    0 |    0 |   258 |
+| hls/Array.v             |     229 |   44 |    0 |   273 |
+| hls/AssocMap.v          |     147 |   30 |    0 |   177 |
+| hls/FunctionalUnits.v   |       9 |    0 |    0 |     9 |
+| hls/HTL.v               |      65 |   50 |  181 |   296 |
+| hls/HTLgen.v            |       0 |  590 |    0 |   590 |
+| hls/HTLgenproof.v       |    2567 |    0 |    0 |  2567 |
+| hls/HTLgenspec.v        |     502 |    0 |   66 |   568 |
+| hls/Memorygen.v         |    2843 |  203 |    0 |  3046 |
+| hls/PrintHTL.ml         |       0 |   70 |    0 |    70 |
+| hls/PrintVerilog.ml     |       0 |  236 |    0 |   236 |
+| hls/ValueInt.v          |     123 |    0 |    0 |   123 |
+| hls/Verilog.v           |     235 |   78 |  431 |   744 |
+| hls/Veriloggen.v        |       0 |  104 |    0 |   104 |
+| hls/Veriloggenproof.v   |     486 |    0 |    0 |   486 |
+| extraction/Extraction.v |       0 |  184 |    0 |   184 |
+| driver/VericertDriver.v |       0 |  460 |    0 |   460 |
+|-------------------------+---------+------+------+-------|
+| Total                   |    8355 | 2496 |  693 | 11544 |
+#+TBLFM: @>$2..@>$4=vsum(@2$$#..@-1$$#)::$5=vsum(@@#$-3..@@#$-1)
-- 
cgit