aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
* 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 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
* Remove unnecessary LemmaYann Herklotz2020-04-221-8/+1
* Use State in semantics instead of splitting it upYann Herklotz2020-04-221-95/+98
* Improve printing of resultsYann Herklotz2020-04-222-7/+13
* Fix Verilog.vYann Herklotz2020-04-171-1/+1
* Add main module runYann Herklotz2020-04-172-51/+79
* Fix printing with new Verilog ASTYann Herklotz2020-04-172-26/+54
* Only generate clocked always blocksYann Herklotz2020-04-171-13/+13
* Extract simulatorYann Herklotz2020-04-172-5/+5
* Add Simulator.vYann Herklotz2020-04-171-0/+32
* Add do notation for optionYann Herklotz2020-04-151-0/+11
* Make proofs simpler using autoYann Herklotz2020-04-151-59/+45
* Add Verilog semantics with new Verilog moduleYann Herklotz2020-04-151-33/+326
* Create Value module for bitvectorsYann Herklotz2020-04-151-0/+217
* Add proof about state wfYann Herklotz2020-04-081-40/+193
* Add partial proof of well formed stateYann Herklotz2020-04-061-24/+136
* Fix extraction on linuxYann Herklotz2020-04-021-1/+1
generated by cgit (git 2.34.1) at 2024-07-03 10:45:15 +0000