aboutsummaryrefslogtreecommitdiffstats
path: root/src/Compiler.v
Commit message (Expand)AuthorAgeFilesLines
* Fix compilation of new intermediate languagesYann Herklotz2021-10-011-5/+8
* Compile HTLPargen againYann Herklotz2021-09-241-2/+2
* Remove unnecessary files and proofsYann Herklotz2021-07-111-2/+2
* Add docker file and some commentsYann Herklotz2021-07-091-0/+2
* Remove Admitted in the highest of top-levelsv1.2.0Yann Herklotz2021-04-071-5/+10
* Add option to turn on/off ram inferrenceYann Herklotz2021-03-021-2/+4
* Add option to turn off if-conversionYann Herklotz2021-02-161-1/+2
* Add predicated values and instructionsYann Herklotz2021-02-021-2/+5
* Add Vrange and predicatesYann Herklotz2021-02-021-2/+0
* Fix imports in Coq modulesYann Herklotz2021-01-211-43/+33
* Add missing modules to extraction and compileYann Herklotz2021-01-131-2/+4
* Add extraction and loop pipelining stageYann Herklotz2020-12-171-1/+4
* Update Compiler proof with all optimisationsYann Herklotz2020-11-281-39/+72
* Update documentation for Compiler.vYann Herklotz2020-11-261-0/+84
* Add optimisations to outputYann Herklotz2020-11-021-15/+73
* Add printing of intermediate rtlblock languageYann Herklotz2020-10-231-1/+5
* Finish implementing scheduling and add top level exportYann Herklotz2020-10-201-3/+7
* Add renumbering to compiler passesYann Herklotz2020-10-181-0/+1
* Add fixes to run scheduling on compilationYann Herklotz2020-09-031-1/+14
* Remove check mpassYann Herklotz2020-07-241-2/+0
* Change name to VericertYann Herklotz2020-07-141-3/+3
* Fixes to operatorsYann Herklotz2020-07-071-0/+2
* Rename asm to verilogYann Herklotz2020-07-061-9/+10
* Add top level backward simulationYann Herklotz2020-07-061-15/+112
* HTLgenproof compiles againYann Herklotz2020-07-061-1/+6
* Add htl pretty printingYann Herklotz2020-06-301-0/+2
* Fix top level invocation to translate through HTLYann Herklotz2020-06-121-3/+6
* Add equality check for valueYann Herklotz2020-05-041-1/+1
* Extract simulatorYann Herklotz2020-04-171-2/+2
* Update compilationYann Herklotz2020-04-011-2/+2
* Convert from RTL to Verilog directlyYann Herklotz2020-03-311-3/+22
* Move compilerYann Herklotz2020-03-291-0/+113