Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | generalize bblock_equiv into bblock_simu | Sylvain Boulmé | 2019-05-07 | 1 | -1/+1 |
| | |||||
* | simplification semantique+preuve des load_q+load_o | Sylvain Boulmé | 2019-05-06 | 1 | -1/+3 |
| | |||||
* | it compiles! | David Monniaux | 2019-05-04 | 1 | -0/+42 |
| | |||||
* | begin add Plq | David Monniaux | 2019-05-03 | 1 | -0/+19 |
| | |||||
* | it compiles | David Monniaux | 2019-05-03 | 1 | -0/+14 |
| | |||||
* | rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves) | David Monniaux | 2019-05-03 | 1 | -29/+9 |
| | |||||
* | it compiles | David Monniaux | 2019-05-01 | 1 | -0/+12 |
| | |||||
* | begin load.xs | David Monniaux | 2019-05-01 | 1 | -0/+12 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactor | Cyril SIX | 2019-04-08 | 1 | -5/+5 |
|\ | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v mppa_k1c/PostpassSchedulingproof.v mppa_k1c/lib/Asmblockgenproof0.v | ||||
| * | relecture sylvain | Sylvain Boulmé | 2019-04-05 | 1 | -5/+5 |
| | | | | | | | | avec TODOs pour refactoring #90 | ||||
* | | #91 Removed completely the duplicated semantics in Asmblock | Cyril SIX | 2019-04-05 | 1 | -20/+16 |
|/ | |||||
* | #90 Asmvliw/Asmblock refactoring attempt | Cyril SIX | 2019-04-05 | 1 | -2/+2 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-work | Cyril SIX | 2019-04-03 | 1 | -17/+5 |
|\ | | | | | | | | | Conflicts: mppa_k1c/Asmblockdeps.v | ||||
| * | cleaning Asmvliw semantics | Sylvain Boulmé | 2019-04-01 | 1 | -17/+5 |
| | | |||||
* | | Preuve des load/store registre registre. Reste des modifs mineures dans les ↵ | Cyril SIX | 2019-04-03 | 1 | -5/+4 |
| | | | | | | | | preuves de Asmblockdeps | ||||
* | | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet | Cyril SIX | 2019-04-02 | 1 | -18/+46 |
|/ | |||||
* | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptable | Cyril SIX | 2019-03-29 | 1 | -3/+173 |
|\ | | | | | | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v | ||||
| * | Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpass | David Monniaux | 2019-03-28 | 1 | -3/+173 |
| |\ | |||||
| | * | slight simplification | Sylvain Boulmé | 2019-03-23 | 1 | -5/+4 |
| | | | |||||
| | * | fix for Coq.8.8 ?? | Sylvain Boulmé | 2019-03-22 | 1 | -2/+0 |
| | | | |||||
| | * | Décomposition de la preuve en une forward_simu_par_stuck et une ↵ | Cyril SIX | 2019-03-22 | 1 | -1/+4 |
| | | | | | | | | | | | | forward_simu_par | ||||
| | * | simplification of the proof | Sylvain Boulmé | 2019-03-21 | 1 | -26/+66 |
| | | | |||||
| | * | yet another step backward | Sylvain Boulmé | 2019-03-20 | 1 | -18/+39 |
| | | | |||||
| | * | one step further... | Sylvain Boulmé | 2019-03-20 | 1 | -6/+28 |
| | | | |||||
| | * | premier decoupage | Sylvain Boulmé | 2019-03-20 | 1 | -2/+56 |
| | | | |||||
| | * | Integrating Asmvliw.v in the proof chain | Cyril SIX | 2019-03-20 | 1 | -10/+24 |
| | | | |||||
| | * | Idée de preuve VLIW | Cyril SIX | 2019-03-18 | 1 | -2/+21 |
| | | | |||||
| | * | definition of VLIW semantics | Sylvain Boulmé | 2019-03-14 | 1 | -5/+4 |
| | | | |||||
* | | | on avance sur la jumptable | David Monniaux | 2019-03-22 | 1 | -0/+1 |
|/ / | |||||
* / | The parent frame pointer is now R17 instead of R14 | Cyril SIX | 2019-03-18 | 1 | -3/+3 |
|/ | |||||
* | Refactorisation des load et des store | Cyril SIX | 2019-03-08 | 1 | -3/+3 |
| | |||||
* | Refactorized Asmblock exec_basic_instr | Cyril SIX | 2019-03-08 | 1 | -1/+1 |
| | |||||
* | No more axiom remaining in PostpassScheduling.v (but still a couple ↵ | Cyril SIX | 2019-03-05 | 1 | -12/+0 |
| | | | | remaining in Asmblockdeps) | ||||
* | Proving the trans_block_header axioms | Cyril SIX | 2019-02-27 | 1 | -672/+672 |
| | |||||
* | Proving verify_schedule_correct with axioms | Cyril SIX | 2019-02-14 | 1 | -14/+0 |
| | |||||
* | Added Ointofsingle + floatconv unit test | Cyril SIX | 2019-02-12 | 1 | -1/+1 |
| | |||||
* | Added Osingleofint | Cyril SIX | 2019-02-12 | 1 | -2/+5 |
| | |||||
* | Minor refactorization | Cyril SIX | 2019-02-12 | 1 | -12/+0 |
| | |||||
* | Proof of axiom verified_schedule_header | Cyril SIX | 2019-02-12 | 1 | -59/+0 |
| | |||||
* | Proving the axiom verified_schedule_single_inst | Cyril SIX | 2019-02-12 | 1 | -2/+0 |
| | |||||
* | Proving verified_schedule_size axiom | Cyril SIX | 2019-02-11 | 1 | -5/+0 |
| | |||||
* | Un peu de refactorisation | Cyril SIX | 2019-02-07 | 1 | -60/+2 |
| | |||||
* | Removing the low_half axiom | Cyril SIX | 2019-02-05 | 1 | -8/+3 |
| | |||||
* | Preuves (en dehors du verified_schedule) terminées dans PostpassSchedulingproof | Cyril SIX | 2019-02-04 | 1 | -6/+44 |
| | |||||
* | Proof of transf_exec_control \o/ | Cyril SIX | 2019-02-04 | 1 | -2/+5 |
| | |||||
* | Proof of label_pos related things in PostpassSchedulingproof | Cyril SIX | 2019-02-04 | 1 | -15/+104 |
| | |||||
* | Encore de la tuyauterie | Cyril SIX | 2019-02-01 | 1 | -1/+91 |
| | |||||
* | Proof of transf_blocks_verified | Cyril SIX | 2019-02-01 | 1 | -9/+46 |
| | |||||
* | Décomposition de transf_find_bblock en lemmes | Cyril SIX | 2019-01-31 | 1 | -1/+22 |
| | |||||
* | Adding a "check_size" in concat2 | Cyril SIX | 2019-01-31 | 1 | -13/+30 |
| |