aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-011-5/+4
|\
| * Small optimisations to proofYann Herklotz2020-05-311-5/+4
* | Merge branch 'develop' into arrays-proofJames Pollard2020-05-306-162/+1327
|\|
| * Merge branch 'develop' of github.com:ymherklotz/CoqUp into developYann Herklotz2020-05-291-6/+3
| |\
| | * Improve automation in HTLgenspec.James Pollard2020-05-291-6/+3
| * | Fix compilation moving to PTreeYann Herklotz2020-05-293-25/+34
| |/
| * Change AssocMap to Maps.PTreeYann Herklotz2020-05-291-3/+5
| * Add more proofs and remove AdmittedYann Herklotz2020-05-271-49/+43
| * Add top level definitionYann Herklotz2020-05-272-138/+153
| * Working on automationYann Herklotz2020-05-261-62/+48
| * Finished proof of spec completelyYann Herklotz2020-05-262-5/+94
| * Finished second pass and fixed bugYann Herklotz2020-05-262-18/+37
| * Finished proving the first caseYann Herklotz2020-05-251-1/+6
| * Continuing work on proving specificationYann Herklotz2020-05-252-22/+218
| * Add HTLgenYann Herklotz2020-05-241-1/+337
| * Finish the proof with most assumptionsYann Herklotz2020-05-212-29/+150
| * Add proof of translation correctnessYann Herklotz2020-05-202-17/+200
| * Add simulation diagramYann Herklotz2020-05-081-5/+53
| * Add match_states InductiveYann Herklotz2020-05-071-0/+29
| * Remove HTLgen and create the specificationYann Herklotz2020-05-072-163/+92
| * Redefine HTL for intermediate Verilog languageYann Herklotz2020-05-071-0/+18
| * Add equality check for valueYann Herklotz2020-05-042-2/+2
| * Add proofs and specification of Verilog conversionYann Herklotz2020-05-032-0/+158
| * Add state transition conversion functionsYann Herklotz2020-05-031-2/+14
| * Add documentation and conform to specificationYann Herklotz2020-04-291-24/+41
* | Stop using tuples for register declarationsJames Pollard2020-05-301-37/+39
* | Fix addressing to add support for arbitraty pointer operationsJames Pollard2020-05-271-10/+19
* | Bug fix: stack address normalisationJames Pollard2020-05-261-1/+1
* | (Tentatively) working stack array/memory support.James Pollard2020-05-261-37/+50
* | Add pattern matches and plumb through stack regJames Pollard2020-05-251-5/+21
* | Start work on array supportJames Pollard2020-05-251-0/+1
|/
* Only generate clocked always blocksYann Herklotz2020-04-171-13/+13
* Make proofs simpler using autoYann Herklotz2020-04-151-59/+45
* Add proof about state wfYann Herklotz2020-04-081-40/+193
* Add partial proof of well formed stateYann Herklotz2020-04-061-24/+136
* Handle loops and conditionals correctlyYann Herklotz2020-04-021-100/+128
* Complete translation from simple RTL to VerilogYann Herklotz2020-04-011-101/+162
* Convert from RTL to Verilog directlyYann Herklotz2020-03-311-18/+20
* Add more operators and print themYann Herklotz2020-03-311-37/+69
* Improve Verilog error messagesYann Herklotz2020-03-311-1/+7
* Rename to transf_programYann Herklotz2020-03-291-1/+1
* Complete conversion from HTL to VerilogYann Herklotz2020-03-291-8/+91
* Add Verilog generation from HTLYann Herklotz2020-03-291-0/+135
* Remove unnecessary examples from HTLYann Herklotz2020-03-291-6/+1
* Create HTLgenYann Herklotz2020-03-253-148/+5
* Add Maps and HTL.vYann Herklotz2020-03-251-0/+186
* Create a new direct translationYann Herklotz2020-03-222-14/+125
* Update names of directoriesYann Herklotz2020-03-191-0/+37
generated by cgit (git 2.34.1) at 2024-07-09 06:47:51 +0000