diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-15 10:38:53 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-15 10:38:53 +0100 |
| commit | 2bf1ff846a792ef3007fa1e97928697509f318f7 (patch) | |
| tree | de842907b30c337f3c20a35f36fc17ede8147fd7 /results | |
| parent | 6363b3998d65dc7a4e45cec0db9b41f69f45fb31 (diff) | |
| download | oopsla21_fvhls-2bf1ff846a792ef3007fa1e97928697509f318f7.tar.gz oopsla21_fvhls-2bf1ff846a792ef3007fa1e97928697509f318f7.zip | |
Update the table
Diffstat (limited to 'results')
| -rw-r--r-- | results/results.org | 34 |
1 files changed, 34 insertions, 0 deletions
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) |