aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add benchmarking of unhashed commandsdebug/unhashedYann Herklotz2023-09-183-38/+235
* Add unhashed functions for comparisonsYann Herklotz2023-09-174-25/+116
* Add Bambu synthesis and ClockRegistersYann Herklotz2023-08-114-0/+414
* Fix backend hardware generation and schedulingYann Herklotz2023-08-1113-66/+114
* Put every load/store into it's own cycleYann Herklotz2023-08-023-179/+204
* Finish datapath memory generationYann Herklotz2023-08-022-409/+546
* Fixing store transformationYann Herklotz2023-08-013-96/+179
* Add fixes to main memory generation proofYann Herklotz2023-07-312-799/+808
* Remove RTLParFu and fix DMemorygen.vYann Herklotz2023-07-315-1974/+1949
* Add beginning to memory generation proofYann Herklotz2023-07-2922-2671/+6810
* Add equivalence classesYann Herklotz2023-07-1110-192/+552
* Add if-conversion decision procedureYann Herklotz2023-07-066-29/+60
* Fix man file generationYann Herklotz2023-06-262-4/+3
* Update cohpred with renamed filesYann Herklotz2023-06-261-0/+0
* Add COHPREDSTAMP to .gitignoreYann Herklotz2023-06-261-0/+2
* Finish some proofs and remove unnecessary AdmittedYann Herklotz2023-06-267-33/+76
* Finish mutual exclusivity checkYann Herklotz2023-06-255-31/+150
* Finish SMT proofYann Herklotz2023-06-231-3/+100
* Add SMTCoq solver as dependencyYann Herklotz2023-06-2114-71/+233
* Update makefile to build cohpredYann Herklotz2023-06-191-2/+6
* Update cohpred libraryYann Herklotz2023-06-181-0/+0
* Update cohpred git submoduleYann Herklotz2023-06-142-1/+1
* Add CohPred and SMTCoq dependencyYann Herklotz2023-06-124-2/+29
* Finish complete evaluability proofYann Herklotz2023-06-101-19/+88
* Try to prove main theoremYann Herklotz2023-06-101-0/+5
* Add more to proof of evaluabilityYann Herklotz2023-06-102-1/+57
* Finish abstract_sequence_evaluable_mYann Herklotz2023-06-091-1/+104
* Prove abstract_sequence_evaluableYann Herklotz2023-06-091-0/+2
* Finish abstract_sequence_evaluable_fold2Yann Herklotz2023-06-091-5/+42
* Finish abstract_sequence_evaluable_foldYann Herklotz2023-06-091-12/+68
* Add outline of proof of evaluable when predicate is falseYann Herklotz2023-06-091-19/+54
* Add proof outline for evaluabilityYann Herklotz2023-06-082-20/+44
* Work towards proving evaluabilityYann Herklotz2023-06-053-38/+169
* Move around generating functionsYann Herklotz2023-06-032-68/+68
* Add lp_solve dependency to nixYann Herklotz2023-06-021-1/+1
* Fix proof of predicates completelyYann Herklotz2023-06-022-7/+24
* Fix top-level proof with Isetpred missingYann Herklotz2023-06-021-12/+55
* Finished the propert version of from_predicated_sem_pred_expr2Yann Herklotz2023-06-027-44/+316
* Finish from_predicated_sem_pred_exprYann Herklotz2023-05-311-8/+97
* Remove unnecessary assumption from sem_merge_listYann Herklotz2023-05-301-4/+3
* Fix other proofs and attempt from_predicated proofYann Herklotz2023-05-301-7/+26
* Prove merge list_translationYann Herklotz2023-05-301-2/+16
* Prove fold_right over ElistYann Herklotz2023-05-301-4/+74
* Finish second flap2 proofYann Herklotz2023-05-301-1/+9
* Finished painful product proofYann Herklotz2023-05-305-13/+127
* Prove more admitted theoremsYann Herklotz2023-05-296-47/+190
* Finish two AbstrSemIdent false proofsYann Herklotz2023-05-281-11/+50
* Finish max predicate proofYann Herklotz2023-05-281-1/+78
* Finish proofs in GiblePargenproofForward.vYann Herklotz2023-05-282-5/+49
* Work on forward proofsYann Herklotz2023-05-282-1/+18
generated by cgit (git 2.34.1) at 2024-04-28 20:45:23 +0000