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

	Commit message (Collapse)	Author	Age	Files	Lines
*	new instructions at asm level	David Monniaux	2019-05-10	1	-1/+53
\|
*	simplification semantique+preuve des load_q+load_o	Sylvain Boulmé	2019-05-06	1	-7/+7
\|
*	big proofs for so / lo	David Monniaux	2019-05-04	1	-1/+83
\|
*	begin add Plq	David Monniaux	2019-05-03	1	-9/+22
\|
*	use sq to save pairs of registers	David Monniaux	2019-05-03	1	-3/+2
\|
*	Merge remote-tracking branch 'origin/mppa-work' into mppa-peephole	David Monniaux	2019-05-03	1	-12/+2
\|\
\| *	rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)	David Monniaux	2019-05-03	1	-12/+2
\| \|
* \|	getting stuck need to move offsets	David Monniaux	2019-05-03	1	-6/+21
\| \|
* \|	find consecutive writes	David Monniaux	2019-05-02	1	-0/+51
\|/
*	does not yet work, arity mismatch	David Monniaux	2019-05-01	1	-15/+1
\|
*	it compiles	David Monniaux	2019-05-01	1	-6/+8
\|
*	translate load.xs	David Monniaux	2019-05-01	1	-4/+4
\|
*	begin load.xs	David Monniaux	2019-05-01	1	-0/+23
\|
*	removed fake ops for int32 -> double	David Monniaux	2019-04-29	1	-4/+0
\|
*	Srsd / Srsw	David Monniaux	2019-04-29	1	-0/+8
\|
*	begin add bitfield insertion	David Monniaux	2019-04-27	1	-2/+16
\|
*	moved operators to specific file instead of common file	David Monniaux	2019-04-27	1	-4/+5
\|
*	start of extfzl/extfsl	David Monniaux	2019-04-25	1	-0/+4
\|
*	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