aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL_Livecheck.v
Commit message (Collapse)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-20 00:35:41 +0000