aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add RTLParFU to top-levelYann Herklotz2021-11-141-0/+2
* Replace HTLPargen by HTLParFUgenYann Herklotz2021-11-142-896/+19
* Improve simplification of predicatesYann Herklotz2021-11-141-2/+10
* Add proper functional unit generationYann Herklotz2021-11-142-23/+98
* Add helper functions to FunctionalUnitsYann Herklotz2021-11-141-0/+74
* Improve Makefile for polybenchYann Herklotz2021-11-142-14/+14
* Add the tseytin transformation insteadYann Herklotz2021-11-142-219/+359
* Add RTLPar with functional unitsYann Herklotz2021-11-133-0/+1302
* Add commented out pretty printing for AbstrYann Herklotz2021-11-131-0/+39
* Move lp_solve to the /temp directoryYann Herklotz2021-11-131-4/+6
* Small progress on the proof of correctnessYann Herklotz2021-11-131-1/+5
* Simplify the RTLPargen update functionYann Herklotz2021-11-131-11/+21
* Fix pretty printing of predicatesYann Herklotz2021-11-131-3/+3
* Improve simplification of predicatesYann Herklotz2021-11-131-57/+80
* Add if-conversion to makefileYann Herklotz2021-11-131-1/+1
* Remove verilator from MakefileYann Herklotz2021-11-132-2/+3
* Rename the verilator scriptYann Herklotz2021-11-131-0/+0
* Prove some of the theorems furtherYann Herklotz2021-11-111-14/+17
* Add documentation to RTLPargenYann Herklotz2021-11-111-18/+72
* Add documentation to RTLBlockInstrYann Herklotz2021-11-111-11/+62
* Add simplify operation and simplify IfConversionYann Herklotz2021-11-112-4/+60
* Fix the scheduler to not remove dead codeYann Herklotz2021-11-111-1/+1
* Add alectryon to default.nixYann Herklotz2021-11-111-0/+1
* Update testbench with verilator supportYann Herklotz2021-11-112-16/+24
* Add files to .gitignoreYann Herklotz2021-11-111-0/+10
* Only add use nix to .envrcYann Herklotz2021-11-111-8/+1
* Add a Verilator driverYann Herklotz2021-11-111-0/+35
* Uncomment many more proofsYann Herklotz2021-11-022-917/+752
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2021-11-021-8/+6
|\
| * Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2021-11-014-170/+335
| |\
| * | [sched] Simplify some of the Lemma statementsYann Herklotz2021-11-011-8/+6
* | | No admitted theorems in RTLPargenproof.vYann Herklotz2021-11-022-13/+14
| |/ |/|
* | Add work on RTLPargenproof.vYann Herklotz2021-11-012-140/+165
* | Add RTLBlockInstr proofsYann Herklotz2021-11-011-0/+23
* | Add Admitted theorems for existence proofsYann Herklotz2021-11-011-9/+2
* | Add construction of state in semYann Herklotz2021-10-311-23/+147
|/
* Fix compilation issues with new typesYann Herklotz2021-10-304-46/+37
* Make Abstr pass with admitted to check top-levelYann Herklotz2021-10-301-45/+110
* Add a predicate to RBsetpredYann Herklotz2021-10-303-6/+6
* Remove admitted from subproofYann Herklotz2021-10-291-6/+57
* Add intermediate step in proof of sem presYann Herklotz2021-10-272-24/+108
* Work more on equivalence of SATYann Herklotz2021-10-263-34/+137
* Continue on semantics preservation proofYann Herklotz2021-10-241-198/+178
* Fix if-conversion and translation with PlitYann Herklotz2021-10-242-5/+5
* Add type-class proofs to Predicate.vYann Herklotz2021-10-242-12/+217
* Add setoid typeclassYann Herklotz2021-10-211-15/+21
* Add work towards decidability of SAT solverYann Herklotz2021-10-217-279/+377
* Start to prove termination of SATYann Herklotz2021-10-203-244/+266
* Continuations on proof of predicatesYann Herklotz2021-10-192-127/+151
* [sched] Fix passes with new predicatesYann Herklotz2021-10-142-1/+3
generated by cgit (git 2.34.1) at 2024-07-02 22:55:48 +0000