aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLBlock.v
Commit message (Expand)AuthorAgeFilesLines
* Change Inductive to recordYann Herklotz2021-09-221-1/+1
* Add predicate semantics to RTLBlockYann Herklotz2021-05-261-7/+8
* Refactoring RTLBlock and RTLParYann Herklotz2021-01-291-120/+29
* Use basic blocks in context to help proofYann Herklotz2021-01-261-11/+15
* Fix types with new changes in RTLBlockYann Herklotz2021-01-221-1/+2
* Define RTLPar semanticsYann Herklotz2021-01-221-86/+0
* Add top-level semantics definitionsYann Herklotz2021-01-221-0/+17
* Add semantics for RTLBlockYann Herklotz2021-01-221-5/+67
* Add semantics for RTLBlockInstr and RTLBlockYann Herklotz2021-01-221-8/+51
* Share code between RTLBlock and ParYann Herklotz2021-01-211-40/+22
* Fix compilation issueYann Herklotz2020-11-101-3/+3
* Change and add back HTLgenYann Herklotz2020-11-091-2/+2
* Quick compile fixYann Herklotz2020-11-041-1/+4
* WIP on RTLBlock semanticsYann Herklotz2020-11-021-12/+98
* Add working partitioning algorithmYann Herklotz2020-08-311-1/+3
* Continue on Partitioning algorithmYann Herklotz2020-08-301-3/+13
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+69