aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLPargen.v
Commit message (Collapse)AuthorAgeFilesLines
* Fix backend hardware generation and schedulingYann Herklotz2023-08-101-9/+9
|
* Put every load/store into it's own cycleYann Herklotz2023-08-021-2/+2
|
* Add beginning to memory generation proofYann Herklotz2023-07-291-634/+334
|
* Work on implementing abstract predicatesYann Herklotz2022-07-191-0/+1
|
* Fix hardware generationYann Herklotz2022-05-311-59/+79
|
* Fix code generation in partitioning and schedulingYann Herklotz2022-05-271-4/+21
|
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-271-78/+104
|
* Remove literal files againYann Herklotz2022-03-261-1/+4
|
* Fix compilation with new HTL languageYann Herklotz2021-11-181-58/+64
|
* Fix generation of RTLParFUYann Herklotz2021-11-171-41/+17
|
* Merge remote-tracking branch 'origin/dev/divider' into dev/schedulingYann Herklotz2021-11-161-28/+29
|\
| * Get some Verilog output with dividersdev/dividerYann Herklotz2021-02-221-9/+16
| |
| * Fix arguments to RBassign and pipedYann Herklotz2021-02-221-1/+1
| |
| * Add new instructions for pipelinesYann Herklotz2021-02-211-18/+8
| |
| * Merge branch 'develop' into dev/dividerYann Herklotz2021-02-211-15/+18
| |\
| * | Add beginning to scheduling divisionYann Herklotz2021-02-151-72/+83
| | |
* | | Fix HTL generation from RTLParFUYann Herklotz2021-11-151-11/+34
| | |
* | | Replace HTLPargen by HTLParFUgenYann Herklotz2021-11-141-17/+19
| | |
* | | Add a predicate to RBsetpredYann Herklotz2021-10-301-1/+1
| | |
* | | Fix if-conversion and translation with PlitYann Herklotz2021-10-241-2/+2
| | |
* | | Add work towards decidability of SAT solverYann Herklotz2021-10-211-5/+6
| | |
* | | [sched] Fix passes with new predicatesYann Herklotz2021-10-141-1/+2
| | |
* | | Make HTLgenproof passYann Herklotz2021-10-081-1/+1
| | |
* | | Fix naming and remove warningsYann Herklotz2021-10-071-7/+7
| | |
* | | Compile HTLPargen againYann Herklotz2021-09-241-4/+3
| | |
* | | Merge branch 'master' into developYann Herklotz2021-09-181-3/+4
|\ \ \
| * | | Remove unnecessary files and proofsYann Herklotz2021-07-111-2/+3
| | | |
| * | | Add legup scriptYann Herklotz2021-07-111-1/+1
| | | |
* | | | Change naturals to positive in predicatesYann Herklotz2021-05-261-1/+1
|/ / /
* | | Basically done with proofYann Herklotz2021-04-071-4/+6
| | |
* | | Finish load and store proof, but broke top-levelYann Herklotz2021-04-061-6/+23
| | |
* | | Add RAM to HTLYann Herklotz2021-03-021-0/+1
| | |
* | | Change lists in case statements to stmnt_listYann Herklotz2021-03-011-1/+1
| |/ |/|
* | Fix RTLPar to use instr list list listYann Herklotz2021-02-161-15/+18
|/
* Add temporary fixes to get everything to compileYann Herklotz2021-02-121-12/+75
|
* Fix state generation for if-conversionYann Herklotz2021-02-031-4/+5
|
* Add predicated values and instructionsYann Herklotz2021-02-021-14/+34
|
* Add Vrange and predicatesYann Herklotz2021-02-021-14/+31
|
* Fix HTLPargen and RTLPargenYann Herklotz2021-01-291-5/+5
|
* Fix types with new changes in RTLBlockYann Herklotz2021-01-221-58/+89
| | | | | Also formatted some files so that they are under 80 columns, which is much nicer to read.
* Fix imports in Coq modulesYann Herklotz2021-01-211-5/+15
|
* Add HTLPargen translationYann Herklotz2021-01-131-50/+130
|
* Add conversion from RTLPar to HTLYann Herklotz2021-01-121-0/+633
generated by cgit (git 2.34.1) at 2024-06-28 21:01:50 +0000