aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Update HTL proof for resource sharing (WIP)Michalis Pardalos2021-05-141-241/+304
* Get HTLgenproof passing again (with admits)Michalis Pardalos2021-05-131-230/+172
* Remove "active_call" from HTL semanticsMichalis Pardalos2021-05-131-16/+16
* Tie all modules' clock to mainMichalis Pardalos2021-04-301-6/+7
* Get HTLgenproof to compileMichalis Pardalos2021-04-201-193/+193
* Fix up rest of HTLgenproofMichalis Pardalos2021-04-091-62/+46
* Get HTLgenproof to compileMichalis Pardalos2021-04-081-87/+89
* Make top-level theorems passYann Herklotz2021-02-161-5/+7
* Merge branch 'michalis' of https://github.com/mpardalos/vericert into michali...Yann Herklotz2021-02-161-22/+27
* Add match_states for RTLPargen proofYann Herklotz2021-01-221-4/+18
* Add correct copyright notices in filesYann Herklotz2021-01-101-0/+1
* More fixes to the proofYann Herklotz2020-11-141-4/+5
* [Fix #9] Fix correctness proof for OshrximmYann Herklotz2020-11-141-4/+90
* Fix compilation issueYann Herklotz2020-11-101-5/+5
* Change and add back HTLgenYann Herklotz2020-11-091-1/+24
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+2683