aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL_Livecheck.v
Commit message (Expand)AuthorAgeFilesLines
* non trapping loadsLéo Gourdin2021-07-231-6/+8
* Preparation for scheduling proof, main lemmas okLéo Gourdin2021-06-141-1/+0
* End of liveness proofLéo Gourdin2021-06-071-54/+45
* ugly complete version of liveness proof (I will clean in next commits)Léo Gourdin2021-06-071-34/+40
* advance for tr_input proofLéo Gourdin2021-06-071-24/+171
* preparation and starting final lemmaLéo Gourdin2021-06-041-21/+100
* Some advance in Liveness lemmasLéo Gourdin2021-06-041-71/+138
* update a more general version of the liveness checkerLéo Gourdin2021-06-031-93/+118
* lemmas on entrypoint, tr_inputs, eqlive_regs, ...Léo Gourdin2021-06-021-21/+112
* some advance in main liveness lemmasLéo Gourdin2021-06-021-28/+68
* Some others main lemmasLéo Gourdin2021-06-011-7/+33
* preparing liveness proof main theoremLéo Gourdin2021-06-011-2/+43
* Lemma liveness_checker_correctLéo Gourdin2021-06-011-0/+12
* Lemma list_iblock_checker_correctLéo Gourdin2021-06-011-0/+20
* Dupmap bugfix and some advance in LivegenLéo Gourdin2021-05-311-21/+78
* BTL Scheduler oracle and some draftsLéo Gourdin2021-05-311-2/+45
* starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-281-0/+44
generated by cgit (git 2.34.1) at 2024-05-08 18:45:51 +0000