aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgen.v
Commit message (Expand)AuthorAgeFilesLines
* Add beginning to memory generation proofYann Herklotz2023-07-291-23/+24
* Add if-conversion decision procedureYann Herklotz2023-07-061-6/+6
* Add global monad notation using InstancesYann Herklotz2022-09-261-1/+1
* Work on implementing abstract predicatesYann Herklotz2022-07-191-0/+1
* Fix compilation with new HTL languageYann Herklotz2021-11-181-12/+11
* Merge remote-tracking branch 'origin/dev/divider' into dev/schedulingYann Herklotz2021-11-161-0/+1
|\
| * Add new instructions for pipelinesYann Herklotz2021-02-211-1/+2
| * Add beginning to scheduling divisionYann Herklotz2021-02-151-0/+1
* | Fix warnings for Coq 8.13.2Yann Herklotz2021-10-091-7/+7
* | Basically done with proofYann Herklotz2021-04-071-4/+6
* | Finish load and store proof, but broke top-levelYann Herklotz2021-04-061-24/+24
* | Add RAM to HTLYann Herklotz2021-03-021-0/+1
|/
* Fix imports to remove warnings when compilingYann Herklotz2021-01-221-9/+20
* Add correct copyright notices in filesYann Herklotz2021-01-101-0/+1
* Change and add back HTLgenYann Herklotz2020-11-091-4/+4
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+654
generated by cgit (git 2.34.1) at 2024-06-26 02:36:03 +0000