aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLPar.v
Commit message (Collapse)AuthorAgeFilesLines
* Change Inductive to recordYann Herklotz2021-09-221-1/+1
|
* Add predicate semantics to RTLParYann Herklotz2021-05-261-7/+8
|
* Fix RTLPar to use instr list list listYann Herklotz2021-02-161-3/+14
|
* Fix definitions of proofs some moreYann Herklotz2021-01-291-1/+11
|
* Refactoring RTLBlock and RTLParYann Herklotz2021-01-291-150/+44
|
* Add more proofs for RTLPargen correctnessYann Herklotz2021-01-271-12/+22
|
* Add an inductive to enter the basic blockYann Herklotz2021-01-261-3/+3
|
* Fix types with new changes in RTLBlockYann Herklotz2021-01-221-1/+2
| | | | | Also formatted some files so that they are under 80 columns, which is much nicer to read.
* Define RTLPar semanticsYann Herklotz2021-01-221-86/+85
| | | | | | These semantics are similar to the RTLBlock semantics, except that more states are needed to reason about the parallel execution in multiple cycles.
* Share code between RTLBlock and ParYann Herklotz2021-01-211-65/+138
|
* Add calculations of max_reg and state in RTLParYann Herklotz2021-01-121-0/+42
|
* Fix compilation issueYann Herklotz2020-11-101-4/+4
|
* Change and add back HTLgenYann Herklotz2020-11-091-3/+3
|
* Quick compile fixYann Herklotz2020-11-041-1/+2
|
* Add RTLParYann Herklotz2020-11-021-0/+98