compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	progress	David Monniaux	2019-04-25	1	-0/+2
\|
*	IT COMPILES	David Monniaux	2019-04-25	1	-1/+1
\|
*	begin bitfields	David Monniaux	2019-04-24	1	-1/+4
\|
*	improving comments on Asmvliw	Sylvain Boulmé	2019-04-08	1	-17/+29
\|
*	Merge remote-tracking branch 'origin/mppa-work' into mppa-refactor	Cyril SIX	2019-04-08	1	-1/+35
\|\ \| \| \| \| \| \| \| \| \| \|	Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmblock.v
* \|	relecture sylvain	Sylvain Boulmé	2019-04-05	1	-298/+69
\| \| \| \| \| \| \| \|	avec TODOs pour refactoring #90
* \|	#90 Asmvliw/Asmblock refactoring attempt	Cyril SIX	2019-04-05	1	-4/+1359
\|/
*	Merge remote-tracking branch 'origin/mppa_k1c' into mppa-work	Cyril SIX	2019-04-03	1	-20/+61
\|\ \| \| \| \| \| \| \| \|	Conflicts: mppa_k1c/Asmblockdeps.v
\| *	simpler parexec_wio_bblock_aux	Sylvain Boulmé	2019-04-01	1	-1/+0
\| \|
\| *	cleaning Asmvliw semantics	Sylvain Boulmé	2019-04-01	1	-19/+61
\| \|
* \|	Load/Store reg-reg are now proven everywhere	Cyril SIX	2019-04-03	1	-24/+14
\| \|
* \|	Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet	Cyril SIX	2019-04-02	1	-14/+34
\|/
*	Preuve de Jumptable dans Asmblockdeps.v	Cyril SIX	2019-03-29	1	-1/+9
\|
*	Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpass	David Monniaux	2019-03-28	1	-2/+4
\|
*	Preuve du forward_simu du parexec_wio_bblock_aux	Cyril SIX	2019-03-27	1	-7/+7
\|
*	Avancement dans Asmblockdeps.v	Cyril SIX	2019-03-27	1	-3/+4
\|
*	Un peu d'avancement	Cyril SIX	2019-03-26	1	-2/+13
\|
*	Integrating Asmvliw.v in the proof chain	Cyril SIX	2019-03-20	1	-3/+2
\|
*	fix the step_internal of Asmvliw	Sylvain Boulmé	2019-03-14	1	-19/+23
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Actually, we want to show that the outcome is the same for any order of "writes" in the parallel execution. (ie we ask that bundles have a deterministic semantics for parallel execution) - we relax the condition that the outcome should be given for sequential execution instead, we ask that the it is given for the "in order" writes. In theory, the semantics would also accept bundles like "R1 := R2 R2 := R1" which are deterministic for parallel execution But, of course, in practice, we will also prove the sequential execution.
*	definition of VLIW semantics	Sylvain Boulmé	2019-03-14	1	-0/+329