| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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 | 1 | -1/+2 |
| | | | | | | | 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. | ||||
| * | Get HTLgenspec compiling with RAM inference | Michalis Pardalos | 2021-08-31 | 1 | -2/+2 |
| | | |||||
| * | Move list lemmas to own file | Michalis Pardalos | 2021-08-22 | 1 | -21/+1 |
| | | |||||
| * | Add length args = length params to Icall spec | Michalis Pardalos | 2021-08-21 | 1 | -44/+80 |
| | | |||||
| * | Strengthen HTLgenspec | Michalis Pardalos | 2021-08-20 | 1 | -9/+14 |
| | | |||||
| * | Find called module in Icall proof | Michalis Pardalos | 2021-08-19 | 1 | -1/+1 |
| | | |||||
| * | Complete HTLspec (mostly) | Michalis Pardalos | 2021-08-12 | 1 | -17/+66 |
| | | |||||
| * | Correct lookup for called funcs, simplify tr_module | Michalis Pardalos | 2021-08-04 | 1 | -15/+29 |
| | | |||||
| * | Check whether callee is internal for Icall | Michalis Pardalos | 2021-08-02 | 1 | -6/+0 |
| | | |||||
| * | Add "join state is <=Int.max_unsigned" to HTLgenspec | Michalis Pardalos | 2021-06-10 | 1 | -1/+2 |
| | | |||||
| * | Add "internal calls only" into translation spec | Michalis Pardalos | 2021-05-18 | 1 | -20/+30 |
| | | | | | | | | Necessary, as external calls are present in RTL, but we should not translate them. This will need to be added as a check into the HTL translation. Admitted in HTLgenspec for now. | ||||
| * | Most of Ireturn proof | Michalis Pardalos | 2021-05-16 | 1 | -1/+1 |
| | | |||||
| * | Update HTL proof for resource sharing (WIP) | Michalis Pardalos | 2021-05-14 | 1 | -1/+3 |
| | | |||||
| * | Remove reverse matching from monad_crush | Michalis Pardalos | 2021-05-12 | 1 | -2/+2 |
| | | | | | Unnecessary | ||||
| * | Change tr_module to show registers are different | Michalis Pardalos | 2021-05-12 | 1 | -6/+6 |
| | | | | | Proof passed with no changes | ||||
| * | Fix added tr_code constructors | Michalis Pardalos | 2021-05-10 | 1 | -12/+19 |
| | | | | | | They did not indicate what instruction they cover. Now tr_code_call and tr_code_instr only apply to Icall and Ireturn respectively. | ||||
| * | Clean up HTLgenspec | Michalis Pardalos | 2021-05-10 | 1 | -127/+130 |
| | | |||||
| * | Remove unused lemmas in HTLgenspec | Michalis Pardalos | 2021-05-10 | 1 | -414/+33 |
| | | |||||
| * | Delete inv_incr tactic (unused) | Michalis Pardalos | 2021-05-10 | 1 | -51/+0 |
| | | |||||
| * | Get entire HTLgenspec proof passing | Michalis Pardalos | 2021-05-10 | 1 | -14/+26 |
| | | |||||
| * | Progress on tr_module proof | Michalis Pardalos | 2021-05-08 | 1 | -52/+80 |
| | | |||||
| * | Fully clean up the iter_expand_instr_spec proof | Michalis Pardalos | 2021-05-07 | 1 | -146/+67 |
| | | |||||
| * | Complete iter_expand_instr_spec proof | Michalis Pardalos | 2021-05-07 | 1 | -14/+23 |
| | | |||||
| * | Prove a spec for the mapping of function params | Michalis Pardalos | 2021-05-06 | 1 | -38/+111 |
| | | | | | | Extracted the traversal of call args into a function and gave it a spec, so that it can be used to prove the overall spec for the Icall instruction. | ||||
| * | Solve easier branches of the transf_instr proof | Michalis Pardalos | 2021-05-06 | 1 | -29/+64 |
| | | | | | What remains is the ones about the mapping of parameter registers. | ||||
| * | Clean up iter_expand_instr_spec proof | Michalis Pardalos | 2021-05-05 | 1 | -21/+10 |
| | | |||||
| * | Solve iter_expand_instr_spec by tactic (not Icall) | Michalis Pardalos | 2021-05-05 | 1 | -105/+179 |
| | | |||||
| * | Add lemmas relating to new HTLgen operations | Michalis Pardalos | 2021-05-03 | 1 | -49/+71 |
| | | |||||
| * | Add some statements about externctrl to tr_code | Michalis Pardalos | 2021-05-03 | 1 | -9/+13 |
| | | |||||
| * | Give a (questionable) translation spec for HTLgen | Michalis Pardalos | 2021-05-02 | 1 | -12/+24 |
| | | | | | | I am not yet convinced it is the right one, particularly around the way I've used existentials. I will be updating it as I progress with the proof. | ||||
| * | Simplify some HTLgenspec proofs | Michalis Pardalos | 2021-05-02 | 1 | -2/+2 |
| | | |||||
| * | Tie all modules' clock to main | Michalis Pardalos | 2021-04-30 | 1 | -4/+33 |
| | | |||||
| * | Get HTLgenproof to compile | Michalis Pardalos | 2021-04-20 | 1 | -86/+87 |
| | | |||||
| * | [WIP] HTLgenspec proof | Michalis Pardalos | 2021-04-17 | 1 | -46/+34 |
| | | |||||
| * | Add idle state after return | Michalis Pardalos | 2021-03-01 | 1 | -27/+30 |
| | | |||||
| * | Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵ | Yann Herklotz | 2021-02-16 | 1 | -13/+49 |
| | | | | | michalis-merge | ||||
| * | Fix imports to remove warnings when compiling | Yann Herklotz | 2021-01-22 | 1 | -4/+14 |
| | | |||||
| * | Add correct copyright notices in files | Yann Herklotz | 2021-01-10 | 1 | -0/+1 |
| | | |||||
| * | Add RTLBlock intermediate language | Yann Herklotz | 2020-08-30 | 1 | -0/+641 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |