aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
...
| * | Minimise the proof a bitYann Herklotz2021-05-161-18/+12
| * | Finish up step_cf_instr_correct againYann Herklotz2021-05-162-19/+43
| * | Fix the top-level proofs with new state_matchYann Herklotz2021-05-152-27/+164
| * | Finish abstract interpretationYann Herklotz2021-05-121-75/+199
| * | Fix admitted in first proof of sem. preservationYann Herklotz2021-05-101-19/+68
| * | Finish correctness of semantics wrt. RTBlockYann Herklotz2021-05-061-84/+327
| * | Add admitted proof of translations in RTLPargenYann Herklotz2021-05-031-27/+177
* | | Check: only main uses ainstack, no calls to mainMichalis Pardalos2021-10-171-20/+66
* | | Check that only main has a stacksizeMichalis Pardalos2021-10-112-12/+47
* | | Get all call and return proofs passing againMichalis Pardalos2021-10-081-4/+25
* | | Maintain that initial call does not have argumentsMichalis Pardalos2021-10-071-0/+1
* | | [WIP] Handle empty stack case for empty stack caseMichalis Pardalos2021-10-071-39/+65
* | | Clarify ireturn proofMichalis Pardalos2021-09-301-5/+5
* | | Prove match_arrs_emptyMichalis Pardalos2021-09-301-1/+19
* | | Complete alloc/free zero proofsMichalis Pardalos2021-09-301-8/+15
* | | Complete call/return proofsMichalis Pardalos2021-09-301-68/+122
* | | [WIP] Updating proof for new state matchingMichalis Pardalos2021-09-291-39/+69
* | | Update match_states. Pointers based on main's spMichalis Pardalos2021-09-291-21/+27
* | | Add assumptions about externctrl finish registersMichalis Pardalos2021-09-211-21/+131
* | | [WIP] Reset finish register after returningMichalis Pardalos2021-09-202-9/+66
* | | Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalisMichalis Pardalos2021-09-193-15/+36
|\ \ \
| * | | Fix infinite loop in proofdev-michalisYann Herklotz2021-09-191-3/+3
| * | | Merge remote-tracking branch 'upstream/master' into dev-michalisYann Herklotz2021-09-172-12/+33
| |\ \ \ | | | |/ | | |/|
| | * | Fix compilation with new CompCert versionYann Herklotz2021-09-171-8/+8
| | * | Fix proofs for SATYann Herklotz2021-08-121-6/+27
| | * | Fix pretty printing issue in VerilogYann Herklotz2021-08-121-1/+1
* | | | [WIP] Fix usage of externctrl property in proofMichalis Pardalos2021-09-191-6/+6
* | | | Add new externctrl_params_mapped to HTLspecMichalis Pardalos2021-09-191-36/+53
* | | | [WIP] Progress on Icall proofMichalis Pardalos2021-09-191-13/+59
* | | | Address admits relating to externctrl paramsMichalis Pardalos2021-09-161-8/+35
|/ / /
* | | Complete callstate proofMichalis Pardalos2021-09-161-6/+43
* | | Progress with callstate proofMichalis Pardalos2021-09-151-8/+11
* | | Progress with icall proofMichalis Pardalos2021-09-151-16/+106
* | | Progress with mem_alloc_zeroMichalis Pardalos2021-09-151-3/+85
* | | Prove mem_free_stack_matchMichalis Pardalos2021-09-141-6/+86
* | | Add hammer tacticsMichalis Pardalos2021-09-131-0/+3
* | | Icall proof progressMichalis Pardalos2021-09-131-35/+85
* | | Name the externctrl correctness clausesMichalis Pardalos2021-09-121-11/+18
* | | Guard join state with called module finishMichalis Pardalos2021-09-113-6/+14
* | | Progress with stackframe matching for IcallMichalis Pardalos2021-09-101-1/+8
* | | Prove that called module exists for IcallMichalis Pardalos2021-09-101-2/+26
* | | Fix duplicated verilog module instantiationsMichalis Pardalos2021-09-081-75/+92
* | | Print declarations in HTL outputMichalis Pardalos2021-09-082-0/+18
* | | Fix renamer skipping ram_memMichalis Pardalos2021-09-031-1/+2
* | | Print control registers in HTL outputMichalis Pardalos2021-09-031-0/+13
* | | Print RAM in HTL outputMichalis Pardalos2021-09-031-0/+17
* | | Fix error in map_externctrlMichalis Pardalos2021-09-031-1/+1
* | | Remove double clockMichalis Pardalos2021-09-031-10/+2
* | | Do not apply externctrl to control registersMichalis Pardalos2021-09-031-34/+18
* | | Address ram in renaming passMichalis Pardalos2021-09-023-14/+39
generated by cgit (git 2.34.1) at 2024-06-25 07:20:32 +0000