aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | | | | Also formatted some files so that they are under 80 columns, which is much nicer to read.
* Define RTLPar semanticsYann Herklotz2021-01-222-172/+85
| | | | | | These semantics are similar to the RTLBlock semantics, except that more states are needed to reason about the parallel execution in multiple cycles.
* 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
| | | | Proof that correct items are returned from an empty forest.
* 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
|
* Add Software pipelining stage by tristan et al.Yann Herklotz2020-12-1712-0/+2429
|
* Update Compiler proof with all optimisationsYann Herklotz2020-11-281-39/+72
|
* Fix build for Coq 8.12.1Yann Herklotz2020-11-268-26/+255
|
* Update documentation for Compiler.vYann Herklotz2020-11-261-0/+84
|
* More fixes to the proofYann Herklotz2020-11-141-4/+5
|
* [Fix #9] Fix correctness proof for OshrximmYann Herklotz2020-11-141-4/+90
| | | | This removes all the admitted.
* Fix compilation issueYann Herklotz2020-11-103-12/+12
|
* Change and add back HTLgenYann Herklotz2020-11-094-10/+33
|
* Update definition of VnegYann Herklotz2020-11-072-2/+2
|
* Finish implementation of shrx_shrx_alt_equivYann Herklotz2020-11-051-74/+133
|
* Comment out blockgenYann Herklotz2020-11-041-1/+2
|
* Quick compile fixYann Herklotz2020-11-042-2/+6
|
generated by cgit (git 2.34.1) at 2024-06-30 21:49:10 +0000