aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Start work on Inop proofYann Herklotz2022-04-201-0/+3
|
* Extract some lemmas from the main proofYann Herklotz2022-04-182-24/+87
|
* Proof of the initial state matchingYann Herklotz2022-04-122-3/+38
|
* Add intermediate filesYann Herklotz2022-04-084-78/+143
|
* Work on the match_states definitionYann Herklotz2022-04-053-17/+26
|
* Add basic blocks to the stackframeYann Herklotz2022-04-055-32/+54
|
* Add whole basic block into stateYann Herklotz2022-04-023-73/+48
|
* Add list of bb to semanticsYann Herklotz2022-03-317-96/+99
|
* Work on semantics for RTLBlockInstrYann Herklotz2022-03-284-22/+57
|
* Add specification for RTLBlockgenproofYann Herklotz2022-03-282-16/+53
|
* Work on specification of RTLBlock generationYann Herklotz2022-03-284-162/+258
|
* Add sphinx documentationYann Herklotz2022-03-262-89/+138
|
* Remove literal files againYann Herklotz2022-03-2621-273/+570
|
* Add more documentationYann Herklotz2022-03-245-149/+73
|
* Rename lit directoryYann Herklotz2022-03-246-16/+18
|
* Change origin of tangled filesYann Herklotz2022-03-238-21/+19
|
* Add back equalitiesYann Herklotz2022-03-221-2/+0
|
* Add first descriptions to org fileYann Herklotz2022-03-222-45/+30
|
* Add literate Coq fileYann Herklotz2022-03-222-7/+3
|
* Add comments to allow for literate detanglingYann Herklotz2022-03-227-18/+362
|
* Add nops to partition generationYann Herklotz2022-03-221-4/+4
|
* Move forall_ptree into commonYann Herklotz2022-03-222-42/+43
|
* Fix proofs in Sat.vYann Herklotz2022-03-221-1/+1
|
* Remove main binaryYann Herklotz2022-03-221-0/+0
|
* Add RTLBlockgenproofYann Herklotz2022-03-221-0/+52
|
* Delete extra data files and scriptsYann Herklotz2022-03-221-0/+0
|
* Update copyright noticeYann Herklotz2022-03-171-1/+1
|
* Start work on reverse if-conversionYann Herklotz2022-03-072-1/+84
|
* Fix RAW dependency calculation for predicatesYann Herklotz2022-03-061-0/+3
|
* Add back proof of beq2_correctYann Herklotz2022-03-031-23/+76
|
* Fix AbstrYann Herklotz2022-03-031-30/+17
|
* Update Coq version to 8.14.1Yann Herklotz2022-03-024-76/+61
|
* Add ptsets.ml library from CompCert for BourdoncleYann Herklotz2022-02-282-0/+791
|
* Final updates to the current documentationYann Herklotz2022-02-253-18/+18
|
* Fix up some more documentationYann Herklotz2022-02-257-146/+68
|
* Start converting commentsYann Herklotz2022-02-253-85/+45
|
* Add PrintLoops for bourdoncle codeYann Herklotz2021-12-091-0/+22
|
* Add bourdoncle to buildYann Herklotz2021-12-097-27/+63
|
* Add a printer for RTLParFUYann Herklotz2021-11-181-0/+120
|
* Fix operation chaining in schedulerYann Herklotz2021-11-181-8/+12
| | | | It now respects the delays properly.
* Remove unnecessary proof from RTLParFUgenYann Herklotz2021-11-181-1/+0
|
* Fix compilation with new HTL languageYann Herklotz2021-11-1811-160/+162
|
* Add bourdoncle codeYann Herklotz2021-11-184-0/+304
|
* Rename pipeliningYann Herklotz2021-11-1813-0/+0
|
* Fix generation of RTLParFUYann Herklotz2021-11-176-46/+27
|
* Merge remote-tracking branch 'origin/dev/divider' into dev/schedulingYann Herklotz2021-11-1610-69/+349
|\
| * Get some Verilog output with dividersdev/dividerYann Herklotz2021-02-222-11/+22
| |
| * Fix Scheduling to add missing statesYann Herklotz2021-02-221-14/+34
| |
| * Fix arguments to RBassign and pipedYann Herklotz2021-02-224-5/+10
| |
| * Add operation pipeliningYann Herklotz2021-02-222-8/+137
| |
generated by cgit (git 2.34.1) at 2024-06-29 00:37:26 +0000