| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Icall proof progress | Michalis Pardalos | 2021-09-13 | 1 | -35/+85 |
| * | Name the externctrl correctness clauses | Michalis Pardalos | 2021-09-12 | 1 | -11/+18 |
| * | Guard join state with called module finish | Michalis Pardalos | 2021-09-11 | 3 | -6/+14 |
| * | Progress with stackframe matching for Icall | Michalis Pardalos | 2021-09-10 | 1 | -1/+8 |
| * | Prove that called module exists for Icall | Michalis Pardalos | 2021-09-10 | 1 | -2/+26 |
| * | Add adi to polybench-syn benchmark-list | Michalis Pardalos | 2021-09-08 | 1 | -0/+1 |
| * | Fix duplicated verilog module instantiations | Michalis Pardalos | 2021-09-08 | 1 | -75/+92 |
| * | Print declarations in HTL output | Michalis Pardalos | 2021-09-08 | 2 | -0/+18 |
| * | Fix renamer skipping ram_mem | Michalis Pardalos | 2021-09-03 | 1 | -1/+2 |
| * | Print control registers in HTL output | Michalis Pardalos | 2021-09-03 | 1 | -0/+13 |
| * | Print RAM in HTL output | Michalis Pardalos | 2021-09-03 | 1 | -0/+17 |
| * | Fix error in map_externctrl | Michalis Pardalos | 2021-09-03 | 1 | -1/+1 |
| * | Remove double clock | Michalis Pardalos | 2021-09-03 | 1 | -10/+2 |
| * | Do not apply externctrl to control registers | Michalis Pardalos | 2021-09-03 | 1 | -34/+18 |
| * | Address ram in renaming pass | Michalis Pardalos | 2021-09-02 | 3 | -14/+39 |
| * | Put memorygen after renaming/applyexternctrl | Michalis Pardalos | 2021-09-02 | 1 | -13/+14 |
| * | Use sumbool instead of option for decide_ram_wf | Michalis Pardalos | 2021-09-01 | 3 | -12/+12 |
| * | Start renaming from 2, fixes wf_params check | Michalis Pardalos | 2021-09-01 | 1 | -1/+1 |
| * | Give specific reasons when ApplyExternctrl fails | Michalis Pardalos | 2021-09-01 | 1 | -1/+5 |
| * | Fix control register ordering in Renaming pass | Michalis Pardalos | 2021-09-01 | 1 | -5/+7 |
| * | Give more specific reasons for Renaming failing | Michalis Pardalos | 2021-09-01 | 1 | -1/+5 |
| * | Get top-level proof passing | Michalis Pardalos | 2021-09-01 | 1 | -12/+14 |
| * | Get HTLgenproof to compile with RAM inference | Michalis Pardalos | 2021-08-31 | 1 | -2/+9 |
| * | Get Memorygen to compile again | Michalis Pardalos | 2021-08-31 | 1 | -475/+484 |
| * | Get HTLgenspec compiling with RAM inference | Michalis Pardalos | 2021-08-31 | 1 | -2/+2 |
| * | Get HTLgen compiling with RAM inference | Michalis Pardalos | 2021-08-31 | 1 | -9/+9 |
| * | Get Renaming compiling with RAM inference | Michalis Pardalos | 2021-08-31 | 3 | -24/+37 |
| * | Get ApplyExternctrl compiling with RAM inference | Michalis Pardalos | 2021-08-31 | 1 | -8/+16 |
| * | WIP | Michalis Pardalos | 2021-08-30 | 6 | -140/+160 |
| * | Merge branch 'oopsla21' into sharing-merge | Michalis Pardalos | 2021-08-26 | 91 | -1720/+8072 |
| |\ | |||||
| | * | Use main instead of top for synthesising Vericert designs | Yann Herklotz | 2021-07-24 | 1 | -1/+1 |
| | * | Update instructions and fix testv1.2.1 | Yann Herklotz | 2021-07-12 | 4 | -6/+5 |
| | * | Remove comments in docker file | Yann Herklotz | 2021-07-12 | 1 | -3/+3 |
| | * | Update the artifact description | Yann Herklotz | 2021-07-12 | 7 | -4/+204 |
| | * | Remove more OCaml files to compile successfully without admits. | Yann Herklotz | 2021-07-11 | 5 | -1085/+0 |
| | * | Remove unnecessary files and proofs | Yann Herklotz | 2021-07-11 | 7 | -16/+19 |
| | * | Update the run-legup.sh file | Yann Herklotz | 2021-07-11 | 1 | -0/+4 |
| | * | Add legup script | Yann Herklotz | 2021-07-11 | 4 | -4/+74 |
| | * | Fix the small test bench for Vericert | Yann Herklotz | 2021-07-11 | 7 | -137/+67 |
| | * | Fix some more of the benchmarks | Yann Herklotz | 2021-07-11 | 8 | -49/+35 |
| | * | Add divider benchmarks | Yann Herklotz | 2021-07-11 | 44 | -0/+3581 |
| | * | Fix makefiles and add a parent makefile | Yann Herklotz | 2021-07-10 | 4 | -3/+18 |
| | * | Fix Makefiles slightly | Yann Herklotz | 2021-07-10 | 8 | -7/+12 |
| | * | Add more documentation and clean up benchmarks | Yann Herklotz | 2021-07-10 | 12 | -158/+139 |
| | * | Add docker file and some comments | Yann Herklotz | 2021-07-09 | 2 | -0/+6 |
| | * | Clean up Memorygen file | Yann Herklotz | 2021-04-07 | 1 | -219/+1 |
| | * | Remove Admitted in the highest of top-levelsv1.2.0 | Yann Herklotz | 2021-04-07 | 1 | -5/+10 |
| | * | No admitted theorems in Memorygen proof (~‾▿‾)~ | Yann Herklotz | 2021-04-07 | 1 | -76/+99 |
| | * | Basically done with proof | Yann Herklotz | 2021-04-07 | 6 | -18/+62 |
| | * | Let everything compile again | Yann Herklotz | 2021-04-06 | 1 | -7/+18 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |