| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | * | | Minimise the proof a bit | Yann Herklotz | 2021-05-16 | 1 | -18/+12 | |
| | | | | ||||||
| | * | | Finish up step_cf_instr_correct again | Yann Herklotz | 2021-05-16 | 2 | -19/+43 | |
| | | | | ||||||
| | * | | Fix the top-level proofs with new state_match | Yann Herklotz | 2021-05-15 | 2 | -27/+164 | |
| | | | | ||||||
| | * | | Finish abstract interpretation | Yann Herklotz | 2021-05-12 | 1 | -75/+199 | |
| | | | | ||||||
| | * | | Fix admitted in first proof of sem. preservation | Yann Herklotz | 2021-05-10 | 1 | -19/+68 | |
| | | | | ||||||
| | * | | Finish correctness of semantics wrt. RTBlock | Yann Herklotz | 2021-05-06 | 1 | -84/+327 | |
| | | | | ||||||
| | * | | Add admitted proof of translations in RTLPargen | Yann Herklotz | 2021-05-03 | 1 | -27/+177 | |
| | | | | ||||||
| * | | | Check: only main uses ainstack, no calls to main | Michalis Pardalos | 2021-10-17 | 1 | -20/+66 | |
| | | | | ||||||
| * | | | Check that only main has a stacksize | Michalis Pardalos | 2021-10-11 | 2 | -12/+47 | |
| | | | | ||||||
| * | | | Get all call and return proofs passing again | Michalis Pardalos | 2021-10-08 | 1 | -4/+25 | |
| | | | | ||||||
| * | | | Maintain that initial call does not have arguments | Michalis Pardalos | 2021-10-07 | 1 | -0/+1 | |
| | | | | ||||||
| * | | | [WIP] Handle empty stack case for empty stack case | Michalis Pardalos | 2021-10-07 | 1 | -39/+65 | |
| | | | | ||||||
| * | | | Clarify ireturn proof | Michalis Pardalos | 2021-09-30 | 1 | -5/+5 | |
| | | | | ||||||
| * | | | Prove match_arrs_empty | Michalis Pardalos | 2021-09-30 | 1 | -1/+19 | |
| | | | | ||||||
| * | | | Complete alloc/free zero proofs | Michalis Pardalos | 2021-09-30 | 1 | -8/+15 | |
| | | | | ||||||
| * | | | Complete call/return proofs | Michalis Pardalos | 2021-09-30 | 1 | -68/+122 | |
| | | | | ||||||
| * | | | [WIP] Updating proof for new state matching | Michalis Pardalos | 2021-09-29 | 1 | -39/+69 | |
| | | | | ||||||
| * | | | Update match_states. Pointers based on main's sp | Michalis Pardalos | 2021-09-29 | 1 | -21/+27 | |
| | | | | ||||||
| * | | | Add assumptions about externctrl finish registers | Michalis Pardalos | 2021-09-21 | 1 | -21/+131 | |
| | | | | ||||||
| * | | | [WIP] Reset finish register after returning | Michalis Pardalos | 2021-09-20 | 2 | -9/+66 | |
| | | | | ||||||
| * | | | Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalis | Michalis Pardalos | 2021-09-19 | 5 | -15/+57 | |
| |\ \ \ | ||||||
| | * | | | 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 | |
| | | | | | ||||||
| | * | | | Merge remote-tracking branch 'upstream/master' into dev-michalis | Yann Herklotz | 2021-09-17 | 3 | -12/+52 | |
| | |\ \ \ | | | |/ | | |/| | ||||||
| | | * | | Merge remote-tracking branch 'origin/master' | Yann Herklotz | 2021-09-17 | 1 | -0/+19 | |
| | | |\ \ | ||||||
| | | | * | | Move license to the SoftwarePipelining directory | Yann Herklotz | 2021-09-15 | 1 | -0/+19 | |
| | | | | | | ||||||
| | | * | | | Fix compilation with new CompCert version | Yann Herklotz | 2021-09-17 | 1 | -8/+8 | |
| | | |/ / | ||||||
| | | * | | Fix proofs for SAT | Yann Herklotz | 2021-08-12 | 1 | -6/+27 | |
| | | | | | ||||||
| | | * | | Fix pretty printing issue in Verilog | Yann Herklotz | 2021-08-12 | 1 | -1/+1 | |
| | | | | | ||||||
| * | | | | [WIP] Fix usage of externctrl property in proof | Michalis Pardalos | 2021-09-19 | 1 | -6/+6 | |
| | | | | | ||||||
| * | | | | Add new externctrl_params_mapped to HTLspec | Michalis Pardalos | 2021-09-19 | 1 | -36/+53 | |
| | | | | | ||||||
| * | | | | [WIP] Progress on Icall proof | Michalis Pardalos | 2021-09-19 | 2 | -13/+94 | |
| | | | | | ||||||
| * | | | | Address admits relating to externctrl params | Michalis Pardalos | 2021-09-16 | 1 | -8/+35 | |
| |/ / / | ||||||
| * | | | 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 | |
| | | | | ||||||
| * | | | 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 | |
| | | | | ||||||
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |