| Commit message (Collapse) | 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 |
| | | | | | | | | | | | | | Needed to match RTL semantics, since the join state executes once before the call is initiated, and we need the destination register to not be affected until after the call has returned. | ||||
| * | | 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 |