aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)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
|