aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
* [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
|\
| * Fix compilation with new CompCert versionYann Herklotz2021-09-171-8/+8
| * Fix proofs for SATYann Herklotz2021-08-121-6/+27
| * Fix pretty printing issue in VerilogYann Herklotz2021-08-121-1/+1
| * Remove more OCaml files to compile successfully without admits.Yann Herklotz2021-07-114-1084/+0
| * Remove unnecessary files and proofsYann Herklotz2021-07-114-9/+12
| * Add legup scriptYann Herklotz2021-07-111-1/+1
* | 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
generated by cgit (git 2.34.1) at 2024-07-02 18:42:45 +0000