aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | | Add helper functions to FunctionalUnitsYann Herklotz2021-11-151-3/+22
* | | 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
generated by cgit (git 2.34.1) at 2024-05-14 15:22:50 +0000