aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLBlockgen.v
Commit message (Expand)AuthorAgeFilesLines
* Add new block generation for GibleYann Herklotz2022-05-261-299/+0
* Translate the base languagesYann Herklotz2022-05-251-2/+2
* Completely finish RTLBlockgenproofYann Herklotz2022-05-121-6/+106
* Extract some lemmas from the main proofYann Herklotz2022-04-181-2/+10
* Proof of the initial state matchingYann Herklotz2022-04-121-1/+2
* Add specification for RTLBlockgenproofYann Herklotz2022-03-281-2/+4
* Work on specification of RTLBlock generationYann Herklotz2022-03-281-137/+34
* Remove literal files againYann Herklotz2022-03-261-7/+8
* Rename lit directoryYann Herklotz2022-03-241-2/+2
* Change origin of tangled filesYann Herklotz2022-03-231-4/+2
* Add back equalitiesYann Herklotz2022-03-221-2/+0
* Add first descriptions to org fileYann Herklotz2022-03-221-10/+16
* Add literate Coq fileYann Herklotz2022-03-221-2/+0
* Add comments to allow for literate detanglingYann Herklotz2022-03-221-2/+262
* Fix imports to remove warnings when compilingYann Herklotz2021-01-221-7/+5
* Add working partitioning algorithmYann Herklotz2020-08-311-11/+4
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+39