aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)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-07-07 19:53:25 +0000