aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
* Add temporary fixes to get everything to compiledev/predicated-executionYann Herklotz2021-02-127-36/+386
* Fix state generation for if-conversionYann Herklotz2021-02-034-14/+21
* Fix scheduling for if-conversionYann Herklotz2021-02-031-14/+90
* Add predicated values and instructionsYann Herklotz2021-02-027-41/+92
* Add if conversion passYann Herklotz2021-02-021-3/+65
* Add if conversion passYann Herklotz2021-02-021-0/+32
* Add Vrange and predicatesYann Herklotz2021-02-028-66/+95
* Fix OCaml files for compilationYann Herklotz2021-01-314-92/+94
* Fix compilation of CoqYann Herklotz2021-01-302-19/+48
* Fix proofs with better defined equalityYann Herklotz2021-01-302-31/+57
* Fix definitions of proofs some moreYann Herklotz2021-01-294-106/+162
* Fix the proof for RTLPargenYann Herklotz2021-01-291-32/+33
* Fix HTLPargen and RTLPargenYann Herklotz2021-01-292-56/+178
* Refactoring RTLBlock and RTLParYann Herklotz2021-01-293-297/+205
* Finish all proofs except executing basic blocksYann Herklotz2021-01-271-1/+4
* Add more proofs for RTLPargen correctnessYann Herklotz2021-01-273-26/+97
* Add basic block matching and proofYann Herklotz2021-01-261-3/+78
* Remove the schedule oracleYann Herklotz2021-01-262-518/+515
* Add an inductive to enter the basic blockYann Herklotz2021-01-261-3/+3
* Use basic blocks in context to help proofYann Herklotz2021-01-261-11/+15
* Add destruction to context match expressionsYann Herklotz2021-01-261-2/+5
* Remove match on basic blocksYann Herklotz2021-01-231-6/+0
* Add match_states for RTLPargen proofYann Herklotz2021-01-222-4/+78
* Fix imports to remove warnings when compilingYann Herklotz2021-01-227-49/+101
* Fix types with new changes in RTLBlockYann Herklotz2021-01-224-91/+133
* Define RTLPar semanticsYann Herklotz2021-01-222-172/+85
* Add top-level semantics definitionsYann Herklotz2021-01-221-0/+17
* Add semantics for RTLBlockYann Herklotz2021-01-222-12/+68
* Add semantics for RTLBlockInstr and RTLBlockYann Herklotz2021-01-222-22/+72
* Share code between RTLBlock and ParYann Herklotz2021-01-214-149/+314
* Fix imports in Coq modulesYann Herklotz2021-01-217-116/+162
* Improve expression equality proofYann Herklotz2021-01-211-57/+17
* Translate from RTLBlock to RTLParYann Herklotz2021-01-131-201/+39
* Correct translation of scheduling with oracle checkYann Herklotz2021-01-131-4/+53
* Remove HTLSchedulegenYann Herklotz2021-01-131-42/+0
* Add missing modules to extraction and compileYann Herklotz2021-01-132-4/+5
* Add RTLPargen.vYann Herklotz2021-01-131-0/+27
* Add HTLPargen translationYann Herklotz2021-01-131-50/+130
* Add conversion from RTLPar to HTLYann Herklotz2021-01-121-0/+633
* Add calculations of max_reg and state in RTLParYann Herklotz2021-01-121-0/+42
* Remove unnecessary definition of checkYann Herklotz2021-01-121-6/+4
* Add concat function to abstract_sequenceYann Herklotz2021-01-121-4/+11
* Define scheduleoracle functionYann Herklotz2021-01-121-6/+131
* Add proof of empty itemsYann Herklotz2021-01-111-0/+10
* Improve definition of forest for infinite registersYann Herklotz2021-01-111-4/+10
* Add top level semantics for forestsYann Herklotz2021-01-111-1/+19
* Add equality check for symbolic expressionsYann Herklotz2021-01-111-0/+347
* Add correct copyright notices in filesYann Herklotz2021-01-1013-0/+118
* Add comments to pipelining codeYann Herklotz2021-01-063-9/+25
* Invert logic on the variant functionYann Herklotz2020-12-301-2/+2
generated by cgit (git 2.34.1) at 2024-06-29 16:07:29 +0000