aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Copy over RTL global stateYann Herklotz2020-06-011-8/+15
|
* 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-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
| | | | Modified-by: Yann Herklotz <git@yannherklotz.com>
* 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 HLSsave/old-stepYann 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
|
* Add valueToInt functionYann Herklotz2020-04-241-0/+3
|
* Add stmnt_runp inductiveYann Herklotz2020-04-221-27/+106
|
* Return the actual result of the moduleYann Herklotz2020-04-221-2/+5
|
generated by cgit (git 2.34.1) at 2024-07-23 19:13:05 +0000