aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgenproof1.v
Commit message (Collapse)AuthorAgeFilesLines
* Exploiting immediate comparisonsCyril SIX2019-05-091-30/+131
|
* little fixDavid Monniaux2019-05-041-1/+1
|
* rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-14/+14
|
* does not yet work, arity mismatchDavid Monniaux2019-05-011-0/+1
|
* it compilesDavid Monniaux2019-05-011-10/+89
|
* ça avanceDavid Monniaux2019-05-011-5/+78
|
* pass one proofDavid Monniaux2019-05-011-7/+2
|
* translate load.xsDavid Monniaux2019-05-011-1/+6
|
* indexed2XS beginDavid Monniaux2019-05-011-0/+4
|
* srsdDavid Monniaux2019-04-291-11/+9
|
* begin using shrxDavid Monniaux2019-04-291-24/+9
|
* Merge remote-tracking branch 'origin/mppa-work' into mppa-refactorCyril SIX2019-04-081-63/+264
|\ | | | | | | | | | | Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmblock.v
| * Oselectf, Oselectfs with conditionDavid Monniaux2019-04-051-17/+111
| |
| * selectl with conditionDavid Monniaux2019-04-051-9/+56
| |
| * Select cmpluDavid Monniaux2019-04-051-0/+18
| |
| * select cmpuDavid Monniaux2019-04-051-3/+23
| |
| * factor out some proofsDavid Monniaux2019-04-051-6/+3
| |
| * some more Oselect comparisonsDavid Monniaux2019-04-041-1/+12
| |
| * OselectDavid Monniaux2019-04-041-4/+5
| |
| * prepare for conditions in cmoveDavid Monniaux2019-04-041-4/+4
| |
| * ternary ops for float/doubleDavid Monniaux2019-04-031-0/+28
| |
| * ternary ops in AES and TEADavid Monniaux2019-04-031-2/+2
| |
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-031-74/+232
| |\
| * | selectl generationDavid Monniaux2019-03-261-3/+13
| | |
| * | selectlDavid Monniaux2019-03-251-0/+14
| | |
| * | more on cmoveDavid Monniaux2019-03-251-63/+24
| | |
* | | Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-6/+6
|\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v mppa_k1c/PostpassSchedulingproof.v mppa_k1c/lib/Asmblockgenproof0.v
| * | | relecture sylvainSylvain Boulmé2019-04-051-6/+6
| | |/ | |/| | | | | | | avec TODOs pour refactoring #90
* / | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-16/+13
|/ /
* | Preuve des load/store registre registre. Reste des modifs mineures dans les ↵Cyril SIX2019-04-031-29/+157
| | | | | | | | preuves de Asmblockdeps
* | Preuve du transl_load et transl_store registre offsetCyril SIX2019-04-031-25/+84
| |
* | We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admittedCyril SIX2019-04-031-34/+6
| |
* | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-13/+12
|/
* Enlevé la dépendance mémoire de PcbuCyril SIX2019-03-131-3/+3
|
* Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patchCyril SIX2019-03-081-2/+310
|\
| * Preuves du branchement avec des floatCyril SIX2019-03-071-25/+242
| |
| * Fix minor proofCyril SIX2019-03-071-0/+91
| |
* | remove dep of exec_arith_instr on memory.Sylvain Boulmé2019-03-071-31/+23
| | | | | | | | | | | | TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible.
* | Experiment Patch of Memory ModelSylvain Boulmé2019-03-071-10/+16
|/
* Added double comparisonsCyril SIX2019-03-011-0/+70
|
* Ajouté la négation des comparateurs singleCyril SIX2019-03-011-1/+39
|
* Implemented float comparisons (no branching yet, and no negation)Cyril SIX2019-03-011-0/+32
|
* OshrxlimmCyril SIX2019-02-081-16/+17
|
* Removing the low_half axiomCyril SIX2019-02-051-16/+18
|
* Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ↵Cyril SIX2019-01-291-33/+45
| | | | ireg au lieu de preg
* Added sxwd and zxwd supportCyril SIX2019-01-221-5/+5
|
* Changed ABI to match GCC - interoperability not tested yetCyril SIX2018-11-231-98/+98
|
* MBload provedCyril SIX2018-11-071-18/+12
|
* MBop provedCyril SIX2018-11-071-95/+97
|
* Changes in Asmblockgenproof1 -> MBcond provedCyril SIX2018-11-071-28/+45
|
generated by cgit (git 2.34.1) at 2024-07-04 14:08:48 +0000