aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Scheduleoracle.v
Commit message (Expand)AuthorAgeFilesLines
* Fix types with new changes in RTLBlockYann Herklotz2021-01-221-31/+40
* Fix imports in Coq modulesYann Herklotz2021-01-211-38/+73
* Improve expression equality proofYann Herklotz2021-01-211-57/+17
* Remove unnecessary definition of checkYann Herklotz2021-01-121-6/+4
* Add concat function to abstract_sequenceYann Herklotz2021-01-121-4/+11
* Define scheduleoracle functionYann Herklotz2021-01-121-6/+131
* Add proof of empty itemsYann Herklotz2021-01-111-0/+10
* Improve definition of forest for infinite registersYann Herklotz2021-01-111-4/+10
* Add top level semantics for forestsYann Herklotz2021-01-111-1/+19
* Add equality check for symbolic expressionsYann Herklotz2021-01-111-0/+347