aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Define RTLPar semanticsYann Herklotz2021-01-222-172/+85
* Add top-level semantics definitionsYann Herklotz2021-01-221-0/+17
* Update documentationYann Herklotz2021-01-221-0/+0
* Add semantics for RTLBlockYann Herklotz2021-01-222-12/+68
* Merge branch 'master' into developYann Herklotz2021-01-225-84/+172
|\
| * Add change log and rename READMEYann Herklotz2021-01-223-84/+169
| * Add documentation repository as submoduleYann Herklotz2021-01-222-0/+3
* | 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
|/
* Remove github pages from repositoryYann Herklotz2021-01-202-30/+1
* Delete documents folder and move to separate repositoryYann Herklotz2021-01-20123-529786/+0
* Fix links on main pageYann Herklotz2021-01-151-1/+1
* More tweaks to the CSSYann Herklotz2021-01-153-5/+5
* Increase font sizeYann Herklotz2021-01-151-9/+9
* Actually update cssYann Herklotz2021-01-151-94/+174
* Fix website build by adding correct pathYann Herklotz2021-01-151-1/+1
* Update websiteYann Herklotz2021-01-154-6/+6
* Fix inconsistencies in websiteYann Herklotz2021-01-152-7/+4
* 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 files to .gitignoreYann Herklotz2021-01-101-0/+12
* Add correct copyright notices in filesYann Herklotz2021-01-1013-0/+118
* Add comments to pipelining codeYann Herklotz2021-01-063-9/+25
* Update license for SoftwarePipeliningYann Herklotz2021-01-061-4/+5
* Invert logic on the variant functionYann Herklotz2020-12-301-2/+2
* Fix whitespaceYann Herklotz2020-12-176-752/+748
* Add .DS_Store to .gitignoreYann Herklotz2020-12-171-0/+1
* Modify array test case to be suitable for loop pipeliningYann Herklotz2020-12-171-3/+5
* Add license mentioning copyright of SoftwarePipeliningYann Herklotz2020-12-171-0/+31
* Add extraction and loop pipelining stageYann Herklotz2020-12-173-3/+19
* Add build files for loop pipeliningYann Herklotz2020-12-173-4/+5
* Modify software pipelining for buildYann Herklotz2020-12-1712-247/+198
* Add Software pipelining stage by tristan et al.Yann Herklotz2020-12-1712-0/+2429
* Fix main buildv1.1.0Yann Herklotz2020-12-172-2/+1
* Update compcert dependency to 3.8Yann Herklotz2020-11-281-0/+0