aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into dev/michalisdev/michalisYann Herklotz2021-10-1827-762/+4045
|\
| * [sched] Fix passes with new predicatesYann Herklotz2021-10-142-1/+3
| * [sched] Add combination of equivalent expressionsYann Herklotz2021-10-141-10/+40
| * [sched] Add true and false predicates to typeYann Herklotz2021-10-141-1/+23
| * [sched] Finish det proofs of basic Abstr semanticsYann Herklotz2021-10-131-27/+44
| * [sched] Add more proof to sem_pred_detYann Herklotz2021-10-131-1/+6
| * [sched] Add proofs of sem_pred_detYann Herklotz2021-10-131-8/+44
| * [sched] Add start to proof of sem_value_detYann Herklotz2021-10-121-0/+12
| * [sched] Remove unnecessary importsYann Herklotz2021-10-121-11/+0
| * [sched] Add more lemmas into HashTreeYann Herklotz2021-10-122-10/+37
| * [sched] Update Abstr.v to use HashTreeYann Herklotz2021-10-121-29/+97
| * [sched] Add HashTree.v for hashing arbitrary valuesYann Herklotz2021-10-121-0/+413
| * Merge branch 'dev/scheduling' of git.ymhg.org:vericert into dev/schedulingYann Herklotz2021-10-127-64/+78
| |\
| | * Fix warnings for Coq 8.13.2Yann Herklotz2021-10-097-64/+78
| * | [sched] Small changes to definitionsYann Herklotz2021-10-121-5/+5
| |/
| * End section in Abstr.vYann Herklotz2021-10-081-0/+2
| * Add abstract intermediate language to RTLPargenYann Herklotz2021-10-081-17/+49
| * Remove warnings of attributesYann Herklotz2021-10-083-126/+126
| * Make HTLgenproof passYann Herklotz2021-10-081-1/+1
| * Add proof of beq_check_correctnessYann Herklotz2021-10-081-57/+120
| * Fix naming and remove warningsYann Herklotz2021-10-072-10/+10
| * RTLPargen now uses Abstr as symbolic execution targetYann Herklotz2021-10-071-705/+1
| * Update functional units to be more generalYann Herklotz2021-10-071-14/+62
| * Add Abstr intermediate languageYann Herklotz2021-10-071-0/+749
| * [scheduling] Fix connected components of DFGYann Herklotz2021-10-011-6/+7
| * Improve pretty-printing and add undirected graphYann Herklotz2021-10-012-7/+23
| * Fix equivalence checkingYann Herklotz2021-10-012-5/+2
| * Add printers for expressions and RTLParYann Herklotz2021-10-012-0/+114
| * Fix compilation of new intermediate languagesYann Herklotz2021-10-011-2/+2
| * Improve equivalence checking using SATYann Herklotz2021-10-011-15/+22
| * Fix scheduler for operation chainingYann Herklotz2021-10-011-8/+22
| * Make all OCaml files compileYann Herklotz2021-09-292-4/+4
| * Revert "Remove more OCaml files to compile successfully without admits."Yann Herklotz2021-09-274-0/+1084
| * Add dependencies for Alectryon documentationYann Herklotz2021-09-271-2/+2
| * Compile HTLPargen againYann Herklotz2021-09-241-4/+3
| * Fix scopingYann Herklotz2021-09-241-12/+10
| * Add back top-level functionsYann Herklotz2021-09-241-40/+157
| * RTLpargen passes compilation againYann Herklotz2021-09-222-10/+18
| * Fix the comparison of predicated expressionsYann Herklotz2021-09-221-138/+174
| * Change Inductive to recordYann Herklotz2021-09-223-18/+17
| * Start adding hashing to RTLPargenYann Herklotz2021-09-202-7/+51
| * Merge branch 'master' into developYann Herklotz2021-09-189-1103/+44
| |\
| * | Add predicate semantics to abstractYann Herklotz2021-05-261-69/+296
| * | Add predicate semantics to RTLParYann Herklotz2021-05-261-7/+8
| * | Add predicate semantics to RTLBlockYann Herklotz2021-05-261-7/+8
| * | Fix if-conversion pass with positivesYann Herklotz2021-05-261-1/+1
| * | Change naturals to positive in predicatesYann Herklotz2021-05-262-45/+79
| * | Add very top-level proofYann Herklotz2021-05-231-0/+33
| * | Fix admitted in last theoremYann Herklotz2021-05-211-3/+8
| * | Finish top-level of proofYann Herklotz2021-05-212-22/+23
generated by cgit (git 2.34.1) at 2024-06-25 07:15:05 +0000