aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add work on abstract predicatesYann Herklotz2022-07-146-96/+377
* Working on scheduling proofYann Herklotz2022-07-044-55/+224
* Try and fix pargenproofYann Herklotz2022-07-042-9/+7
* Add work on schedulingYann Herklotz2022-07-034-56/+64
* Update ifconversion definitionYann Herklotz2022-07-012-65/+73
* Finish DeadBlocksproofYann Herklotz2022-07-013-101/+158
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-07-012-75/+466
|\
| * Working on extending ifconversion proofYann Herklotz2022-06-302-0/+20
| * Remove useless commentsYann Herklotz2022-06-301-9/+0
| * Finish if-conversion proofYann Herklotz2022-06-301-1/+148
| * Nearly finished if-conversion proofYann Herklotz2022-06-302-65/+298
* | Add dead code elimination proof mostlyYann Herklotz2022-07-011-0/+1052
|/
* Update proofYann Herklotz2022-06-303-37/+125
* Work on if-conversion proofYann Herklotz2022-06-283-47/+282
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-06-282-21/+92
|\
| * Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-06-2814-53/+89
| |\
| * | Add if-conversion specYann Herklotz2022-06-282-21/+92
* | | Update if-conversion functionYann Herklotz2022-06-282-3/+10
| |/ |/|
* | Update build files for documentationYann Herklotz2022-06-243-7/+10
* | Update documentation for GibleYann Herklotz2022-06-245-15/+19
* | Move nix config to flakeYann Herklotz2022-06-246-31/+60
|/
* Work on the if-conversion proofYann Herklotz2022-06-092-32/+49
* Rearrange definitions and create IfConversion templateYann Herklotz2022-06-066-105/+301
* Finish CondElim proof and fix Gible semanticsYann Herklotz2022-06-063-134/+246
* Fix many more lemmasYann Herklotz2022-06-054-109/+329
* Remove inv H1 from condelim proofYann Herklotz2022-06-051-3/+3
* Add condelim proofYann Herklotz2022-06-051-85/+169
* work on condelimproofYann Herklotz2022-06-041-66/+72
* Add to condelim proofYann Herklotz2022-06-041-2/+111
* Working towards ElimCond proofYann Herklotz2022-06-032-34/+87
* Work on CondElim proofYann Herklotz2022-06-036-24/+111
* Add an example of a recursive moore FSMYann Herklotz2022-05-311-0/+184
* Do not remove dependencies from control-flowYann Herklotz2022-05-311-1/+6
* Use the .sv extension for VerilogYann Herklotz2022-05-311-3/+3
* Place both case statements into the same always blockYann Herklotz2022-05-311-4/+5
* Abstract useful function into Predicate.vYann Herklotz2022-05-311-0/+7
* Fix hardware generationYann Herklotz2022-05-311-59/+79
* Fix GibleSeqgenproof with new semanticsYann Herklotz2022-05-312-54/+70
* Fix update function for control-flowYann Herklotz2022-05-311-1/+12
* Update the Gible semantics with correct terminationYann Herklotz2022-05-311-9/+10
* Add new translations to top-levelYann Herklotz2022-05-311-1/+7
* Fix paths in MakefileYann Herklotz2022-05-311-2/+2
* Simplify if-conversion passYann Herklotz2022-05-311-30/+80
* Add new translation passes for if-conversionYann Herklotz2022-05-313-0/+337
* Fix code generation in partitioning and schedulingYann Herklotz2022-05-274-9/+54
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-2724-656/+374
* Add new block generation for GibleYann Herklotz2022-05-266-457/+298
* Translate the base languagesYann Herklotz2022-05-257-437/+431
* Famous proven but not tested has been fixedYann Herklotz2022-05-124-14/+14
* Completely finish RTLBlockgenproofYann Herklotz2022-05-122-24/+171