| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Fix infinite loop in proofdev-michalis | Yann Herklotz | 2021-09-19 | 1 | -3/+3 |
| * | Add xomega tactic into Vericertlib | Yann Herklotz | 2021-09-17 | 1 | -0/+2 |
| * | Update CompCert | Yann Herklotz | 2021-09-17 | 1 | -0/+0 |
| * | Merge remote-tracking branch 'upstream/master' into dev-michalis | Yann Herklotz | 2021-09-17 | 13 | -123/+284 |
| |\ | |||||
| | * | Merge remote-tracking branch 'origin/master' | Yann Herklotz | 2021-09-17 | 6 | -81/+131 |
| | |\ | |||||
| | | * | Update docs | Yann Herklotz | 2021-09-16 | 2 | -2/+2 |
| | | * | Add number of pages correctly | Yann Herklotz | 2021-09-15 | 1 | -1/+1 |
| | | * | Fix a typo in README.org | Yann Herklotz | 2021-09-15 | 1 | -1/+1 |
| | | * | Add DOI to article | Yann Herklotz | 2021-09-15 | 2 | -1/+2 |
| | | * | Add CITATION.cff | Yann Herklotz | 2021-09-15 | 1 | -0/+46 |
| | | * | Fix linguist-vendored for repository statistics | Yann Herklotz | 2021-09-15 | 1 | -1/+1 |
| | | * | Add more information about paper to README | Yann Herklotz | 2021-09-15 | 1 | -48/+64 |
| | | * | Move license to the SoftwarePipelining directory | Yann Herklotz | 2021-09-15 | 2 | -32/+19 |
| | * | | Fix compilation with new CompCert version | Yann Herklotz | 2021-09-17 | 4 | -34/+16 |
| | |/ | |||||
| | * | Fix proofs for SAT | Yann Herklotz | 2021-08-12 | 1 | -6/+27 |
| | * | Add more artifact documentation | Yann Herklotz | 2021-08-12 | 2 | -4/+112 |
| | * | Fix pretty printing issue in Verilog | Yann Herklotz | 2021-08-12 | 1 | -1/+1 |
| * | | Complete callstate proof | Michalis Pardalos | 2021-09-16 | 1 | -6/+43 |
| * | | Progress with callstate proof | Michalis Pardalos | 2021-09-15 | 1 | -8/+11 |
| * | | Progress with icall proof | Michalis Pardalos | 2021-09-15 | 1 | -16/+106 |
| * | | Progress with mem_alloc_zero | Michalis Pardalos | 2021-09-15 | 1 | -3/+85 |
| * | | Prove mem_free_stack_match | Michalis Pardalos | 2021-09-14 | 1 | -6/+86 |
| * | | Add hammer tactics | Michalis Pardalos | 2021-09-13 | 1 | -0/+3 |
| * | | 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 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |