aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
* Finish final forward simulation correctnessYann Herklotz2023-08-1013-7127/+67
* Abort steytin proofsYann Herklotz2023-08-101-2/+2
* Add Bambu synthesis and ClockRegistersYann Herklotz2023-08-101-0/+245
* Fix backend hardware generation and schedulingYann Herklotz2023-08-106-42/+80
* Remove tseytin transformation temporarilyYann Herklotz2023-08-101-1/+1
* 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-2917-2662/+6789
* Add equivalence classesYann Herklotz2023-07-116-191/+334
* Add if-conversion decision procedureYann Herklotz2023-07-065-27/+53
* Finish some proofs and remove unnecessary AdmittedYann Herklotz2023-06-265-32/+74
* Finish mutual exclusivity checkYann Herklotz2023-06-254-30/+121
* Finish SMT proofYann Herklotz2023-06-231-3/+100
* Add SMTCoq solver as dependencyYann Herklotz2023-06-216-47/+216
* 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
* 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-026-44/+304
* 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-304-11/+125
* Prove more admitted theoremsYann Herklotz2023-05-295-47/+169
* 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
* Finish proofs in GiblePargenproofBackward.vYann Herklotz2023-05-271-26/+101
* Add proofs of gather_predicatesYann Herklotz2023-05-261-25/+196
* Finish predicate inclusion proofsYann Herklotz2023-05-251-48/+99
* Finish gather_predicate proofsYann Herklotz2023-05-241-17/+502
* Prove evaluability of predicates throughoutYann Herklotz2023-05-221-61/+126
* Work on smaller evaluability proofYann Herklotz2023-05-221-49/+88
* Finish abstr_seq_reverse_correct_foldYann Herklotz2023-05-213-35/+116
generated by cgit (git 2.34.1) at 2024-06-25 23:26:02 +0000