aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Collapse)AuthorAgeFilesLines
* Finished main proof with small assumptionsYann Herklotz2020-06-042-34/+94
|
* Uncomment proofYann Herklotz2020-06-032-43/+41
|
* Add proof to final_statesYann Herklotz2020-06-021-1/+3
|
* Add proof for initial stateYann Herklotz2020-06-022-3/+27
|
* Get whole proof to compileYann Herklotz2020-06-021-14/+17
|
* Shorten the proof a bitYann Herklotz2020-06-021-41/+15
|
* Add proof for equivalence of movYann Herklotz2020-06-022-38/+110
|
* Add lemmas for preservation of globalsYann Herklotz2020-06-012-29/+50
|
* Small optimisations to proofYann Herklotz2020-05-311-5/+4
|
* 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
| | | | Modified-by: Yann Herklotz <git@yannherklotz.com>
* 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
|
* Only generate clocked always blocksYann Herklotz2020-04-171-13/+13
|
* Make proofs simpler using autoYann Herklotz2020-04-151-59/+45
| | | | | This makes changes to theorems easier, as the proofs will likely not have to be fixed. The runtime is also not much slower.
* 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-16 05:00:50 +0000