aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Fix proofs for ptr64vericert-kvxYann Herklotz2022-03-145-64/+13
|
* Add scheduling oracle to VerilogYann Herklotz2022-03-1438-8163/+12886
|
* Add always inliningYann Herklotz2022-03-131-4/+1
|
* Small fixes to make extraction passYann Herklotz2022-03-104-20/+6
|
* Update .gitignoreYann Herklotz2022-03-101-0/+3
|
* Update Verilog back endYann Herklotz2022-03-1031-3411/+1092
|
* Fix compilation of verilog back endYann Herklotz2022-03-102-102/+77
|
* Replace omega by liaYann Herklotz2022-03-107-52/+57
|
* Add proof of splitlong_ptr32Yann Herklotz2022-03-101-0/+3
|
* Add Verilog backendYann Herklotz2022-03-1033-0/+16929
|
* fix missing "formally"CPP22_mainSylvain Boulmé2021-12-101-1/+1
|
* authors and papers links for the CPP'22 versionSylvain Boulmé2021-12-062-2/+14
|
* more explanation on the web page.Sylvain Boulmé2021-12-031-0/+2
|
* update for CPP_2022 publicationSylvain Boulmé2021-12-021-5/+6
|
* opweights u74Léo Gourdin2021-09-171-0/+139
|
* Revert "[MERGE] weak-software-pipelining in RTLpath"Léo Gourdin2021-09-1647-3987/+229
| | | | This reverts commit d0f23ce9e96a8ef984dbdd47a0848bcdd8f43d7e.
* latest coq+ocaml versionsSylvain Boulmé2021-09-151-35/+12
|
* update gitlab-CI from kvx-workSylvain Boulmé2021-09-151-12/+35
|
* [MERGE] weak-software-pipelining in RTLpathLéo Gourdin2021-09-0247-229/+3987
|\
| * Fix small errorJustus Fasse2021-08-241-5/+5
| | | | | | | | (was already included for the benchmark runs for the M2 report)
| * Hopefully a proper fix to code motion below side exits + NO register renamingJustus Fasse2021-08-211-0/+23
| |
| * Revert "Fix error"Justus Fasse2021-08-211-17/+5
| | | | | | | | | | | | This reverts commit a0119e5987a1cd84f2baa9286f39b1fc6498af23. Fix applied at wrong place
| * Fix errorJustus Fasse2021-08-211-5/+17
| | | | | | | | | | | | | | When code motion past side exits is NOT combined with general register renaming, the renaming necessary to make it safe to duplicate instructions may cause final restoration code to be inserted. Final restoration code is trated specially by its own function.
| * Remove hopefully useless compiler passesJustus Fasse2021-08-212-16/+5
| |
| * **Ugly** proof of simu_check_single_correctJustus Fasse2021-08-181-8/+31
| |
| * Match naming convention of surrounding code.Justus Fasse2021-08-181-2/+2
| |
| * Merge branch 'kvx-work' into weak-software-pipeliningJustus Fasse2021-08-1716-358/+1353
| |\
| * | Modified logic to detect inner loops spanned by a superblockJustus Fasse2021-08-171-3/+10
| | |
| * | Remove done TODO commentJustus Fasse2021-08-171-2/+2
| | |
| * | Work-around for prepass-past-side-exits error.Justus Fasse2021-08-171-11/+17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before, downward scheduling would sometimes give an unverifiable result because instructions are duplicated before restoration instructions and aliasing are applied. If for example a loop increment was moved below multiple side-exits, the restoration code would still mess up the correct duplication of the instruction because the aliasing logic for later side exits would overwrite this change. As a work-around, this commit ensures that the aliasing logic for side-exits is applied in-order. This may leave aliasing code that is utterly useless, which should be cleaned up by DCE.
| * | Make warning about worse schedule with relaxed problem non-fatal unlessJustus Fasse2021-08-171-1/+3
| | | | | | | | | | | | | | | | | | in debug mode. Compiling glpk-4.65 exhibited this problem but not when using the ILP-based instruction scheduling.
| * | Issue warning when idealized final time is larger than default finalJustus Fasse2021-08-171-2/+6
| | | | | | | | | | | | time
| * | Make specifying of prepass past side exits heuristic optionalJustus Fasse2021-08-171-0/+1
| | |
| * | Fix compilation errorJustus Fasse2021-08-161-1/+3
| | |
| * | Use modified dependency calculation that is more generous (timing-wise)Justus Fasse2021-08-161-1/+1
| | | | | | | | | | | | | | | | | | with regard to scheduling constraints necessitated by code outside of the superblock. This behavior more closely matches that of the other dependency calculations giving a more fair comparison.
| * | Supply correct arguments to functionJustus Fasse2021-08-161-1/+1
| | |
| * | Remove useless commentJustus Fasse2021-08-161-1/+0
| | |
| * | Remove duplicate function definitionJustus Fasse2021-08-161-8/+0
| | |
| * | Better relative estimates by systematically supplying correct livenessJustus Fasse2021-08-161-1/+2
| | | | | | | | | | | | | | | | | | information. Correct in the sense that they match the expected scheduling constraints.
| * | Insert final restoration code at very end of superblock if possibleJustus Fasse2021-08-161-22/+23
| | |
| * | More appropriate name for functionJustus Fasse2021-08-161-5/+2
| | |
| * | Experimenting with compiler passesJustus Fasse2021-08-162-0/+19
| | |
| * | Do not restore unnecessary instructions before a predicted IcondJustus Fasse2021-08-111-10/+16
| | | | | | | | | | | | | | | | | | | | | If the Icond is the last instruction of the path, the live_renames includes all the live renames for all successors (s_output_regs). However not all of those need to be stricly restored before the Icond. Some can be restored afterwards.
| * | Add missing dependency for restoration_instructions'Justus Fasse2021-08-111-0/+24
| | |
| * | Allow restoration instructions at the very end of the path.Justus Fasse2021-08-111-2/+18
| | | | | | | | | | | | | | | This becomes necessary once we allow register renaming for the originally last instruction of the path.
| * | More aggressive register renamingJustus Fasse2021-08-111-5/+12
| | |
| * | Make it easier to insert debugging codeJustus Fasse2021-08-111-3/+2
| | |
| * | Better variable name and an early exit in rename_regsJustus Fasse2021-08-111-5/+17
| | |
| * | Forgotten changeJustus Fasse2021-08-111-1/+2
| | | | | | | | | | | | (return expected final time from prepass scheduling)
| * | Do not incur latency hit for the fake-read of the memory by a side exitJustus Fasse2021-08-101-2/+16
| | |
generated by cgit (git 2.34.1) at 2024-05-19 08:41:07 +0000