aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | 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 .gitignore for *.vok *.vosYann Herklotz2020-05-241-0/+2
* | 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
* | Update coq version to 11Yann Herklotz2020-05-202-2/+2
* | 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
* | Move Verilog to .svYann Herklotz2020-05-041-3/+1
* | Refine the semanticsYann Herklotz2020-05-043-56/+130
* | Add code to debug execution of HLSYann Herklotz2020-05-033-0/+137
* | 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 OS detection to makefileYann Herklotz2020-04-232-16/+13
* | Add stmnt_runp inductiveYann Herklotz2020-04-221-27/+106
| * 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-263-37/+62
| * Add pattern matches and plumb through stack regJames Pollard2020-05-251-5/+21
| * Start work on array supportJames Pollard2020-05-251-0/+1
| * Merge pull request #4 from ymherklotz/developYann Herklotz2020-04-2212-158/+804
| |\ | |/ |/|
* | Improve the printing of resultsYann Herklotz2020-04-221-4/+5
generated by cgit (git 2.34.1) at 2024-07-01 14:37:33 +0000