aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
* | First draft of array semantics.James Pollard2020-06-011-112/+188
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-012-13/+19
|\|
| * Copy over RTL global stateYann Herklotz2020-06-011-8/+15
| * Small optimisations to proofYann Herklotz2020-05-311-5/+4
* | Merge branch 'develop' into arrays-proofJames Pollard2020-05-3017-348/+2195
|\|
| * 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-296-36/+48
| |/
| * Fix indentationYann Herklotz2020-05-291-6/+6
| * New and improved AssocmapYann Herklotz2020-05-291-7/+32
| * Change AssocMap to Maps.PTreeYann Herklotz2020-05-292-50/+71
| * Finish Assocmap proofsYann Herklotz2020-05-281-0/+59
| * Add more proofs and remove AdmittedYann Herklotz2020-05-273-65/+94
| * 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-253-22/+224
| * Add HTLgenYann Herklotz2020-05-242-6/+341
| * Add statemonad declarationYann Herklotz2020-05-242-0/+103
| * Finish the proof with most assumptionsYann Herklotz2020-05-213-35/+161
| * Add proof of translation correctnessYann Herklotz2020-05-202-17/+200
| * Fix the semantics to properly evaluate the stateYann Herklotz2020-05-201-2/+4
| * Switch position of empty ruleYann Herklotz2020-05-201-4/+4
| * Fix definitions in Value and add lemmasYann Herklotz2020-05-201-7/+35
| * Add theorems about mergeYann Herklotz2020-05-201-2/+12
| * Add simulation diagramYann Herklotz2020-05-081-5/+53
| * Add lessdef for valuesYann Herklotz2020-05-081-3/+10
| * Add AssocMapYann Herklotz2020-05-084-47/+93
| * 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-072-76/+87
| * Use associations instead of stateYann Herklotz2020-05-072-70/+69
| * Rename assoclist to assocsetYann Herklotz2020-05-072-28/+28
| * Remove Admitted Maps LemmaYann Herklotz2020-05-071-6/+0
| * Add changes to valueYann Herklotz2020-05-061-2/+9
| * Refine test fileYann Herklotz2020-05-051-5/+2
| * Minimised manual simulationYann Herklotz2020-05-052-45/+14
| * Simplifications to proofYann Herklotz2020-05-053-18/+15
| * Finish manual simulationYann Herklotz2020-05-052-5/+68
| * Add equality check for valueYann Herklotz2020-05-047-21/+27
| * Refine the semanticsYann Herklotz2020-05-043-56/+130
| * Add code to debug execution of HLSYann Herklotz2020-05-031-0/+73
| * Add proofs and specification of Verilog conversionYann Herklotz2020-05-032-0/+158
| * Add state transition conversion functionsYann Herklotz2020-05-031-2/+14
| * Add hex notation to valuesYann Herklotz2020-05-031-0/+9
| * Change to StateYann Herklotz2020-05-031-21/+22
| * Add documentation and conform to specificationYann Herklotz2020-04-291-24/+41
| * Add CompCert semantics for VerilogYann Herklotz2020-04-241-81/+152
generated by cgit (git 2.34.1) at 2024-07-07 15:56:00 +0000