aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTL.v
Commit message (Expand)AuthorAgeFilesLines
* Add memory disableYann Herklotz2021-03-311-2/+3
* Add many lemmas about arraysYann Herklotz2021-03-211-17/+17
* Prove idempotency of array mergeYann Herklotz2021-03-111-4/+8
* Update RAM generation proofsYann Herklotz2021-03-091-4/+12
* Add RAM semantics to HTL and fix proofYann Herklotz2021-03-031-3/+40
* Add RAM to HTLYann Herklotz2021-03-021-0/+1
* Fix imports to remove warnings when compilingYann Herklotz2021-01-221-5/+14
* Add correct copyright notices in filesYann Herklotz2021-01-101-0/+1
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+171