aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
* | 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
* | Fix whitespaceYann Herklotz2020-12-176-752/+748
* | Add extraction and loop pipelining stageYann Herklotz2020-12-173-3/+19
* | Modify software pipelining for buildYann Herklotz2020-12-1712-247/+198