aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | | [WIP] Reset finish register after returningMichalis Pardalos2021-09-202-9/+66
* | | Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalisMichalis Pardalos2021-09-1915-126/+289
|\ \ \
| * | | Fix infinite loop in proofdev-michalisYann Herklotz2021-09-191-3/+3
| * | | Add xomega tactic into VericertlibYann Herklotz2021-09-171-0/+2
| * | | Update CompCertYann Herklotz2021-09-171-0/+0
| * | | Merge remote-tracking branch 'upstream/master' into dev-michalisYann Herklotz2021-09-1713-123/+284
| |\ \ \ | | | |/ | | |/|
| | * | Merge remote-tracking branch 'origin/master'Yann Herklotz2021-09-176-81/+131
| | |\ \
| | | * | Update docsYann Herklotz2021-09-162-2/+2
| | | * | Add number of pages correctlyYann Herklotz2021-09-151-1/+1
| | | * | Fix a typo in README.orgYann Herklotz2021-09-151-1/+1
| | | * | Add DOI to articleYann Herklotz2021-09-152-1/+2
| | | * | Add CITATION.cffYann Herklotz2021-09-151-0/+46
| | | * | Fix linguist-vendored for repository statisticsYann Herklotz2021-09-151-1/+1
| | | * | Add more information about paper to READMEYann Herklotz2021-09-151-48/+64
| | | * | Move license to the SoftwarePipelining directoryYann Herklotz2021-09-152-32/+19
| | * | | Fix compilation with new CompCert versionYann Herklotz2021-09-174-34/+16
| | |/ /
| | * | Fix proofs for SATYann Herklotz2021-08-121-6/+27
| | * | Add more artifact documentationYann Herklotz2021-08-122-4/+112
| | * | 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-192-13/+94
* | | | 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
* | | Add adi to polybench-syn benchmark-listMichalis Pardalos2021-09-081-0/+1
* | | 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
* | | Put memorygen after renaming/applyexternctrlMichalis Pardalos2021-09-021-13/+14
* | | Use sumbool instead of option for decide_ram_wfMichalis Pardalos2021-09-013-12/+12
* | | Start renaming from 2, fixes wf_params checkMichalis Pardalos2021-09-011-1/+1
* | | Give specific reasons when ApplyExternctrl failsMichalis Pardalos2021-09-011-1/+5
* | | Fix control register ordering in Renaming passMichalis Pardalos2021-09-011-5/+7
* | | Give more specific reasons for Renaming failingMichalis Pardalos2021-09-011-1/+5