aboutsummaryrefslogtreecommitdiffstats
path: root/src/extraction
Commit message (Expand)AuthorAgeFilesLines
* Remove unnecessary files and proofsYann Herklotz2021-07-111-4/+4
* Add option to turn on/off ram inferrenceYann Herklotz2021-03-021-0/+2
* Change lists in case statements to stmnt_listYann Herklotz2021-03-011-0/+1
* Add option to turn off if-conversionYann Herklotz2021-02-161-1/+5
* Add temporary fixes to get everything to compileYann Herklotz2021-02-121-0/+1
* Fix compilation of CoqYann Herklotz2021-01-301-1/+3
* Add missing modules to extraction and compileYann Herklotz2021-01-131-2/+1
* Add extraction and loop pipelining stageYann Herklotz2020-12-171-2/+4
* Fix build for Coq 8.12.1Yann Herklotz2020-11-261-2/+1
* Add optimisations to outputYann Herklotz2020-11-021-0/+1
* Add tbl_to_casestatement into extractionYann Herklotz2020-10-261-1/+3
* Add printing of intermediate rtlblock languageYann Herklotz2020-10-231-0/+1
* Finish implementing scheduling and add top level exportYann Herklotz2020-10-201-1/+3
* Add fixes to run scheduling on compilationYann Herklotz2020-09-031-0/+1
* Continue on Partitioning algorithmYann Herklotz2020-08-301-2/+3
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-1/+8
* Change name to VericertYann Herklotz2020-07-141-4/+4
* Add htl pretty printingYann Herklotz2020-06-301-0/+1
* Remove extraction of simulatorYann Herklotz2020-06-121-2/+2
* Add equality check for valueYann Herklotz2020-05-041-1/+1
* Extract simulatorYann Herklotz2020-04-171-3/+3
* Fix extraction on linuxYann Herklotz2020-04-021-1/+1
* Update compilationYann Herklotz2020-04-011-1/+1
* Convert from RTL to Verilog directlyYann Herklotz2020-03-311-0/+3
* Use Compcert extractionYann Herklotz2020-03-311-2/+161
* Remove dunes and make the build recursiveYann Herklotz2020-03-251-4/+0
* Lower case foldersYann Herklotz2020-03-192-0/+34