aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
* Fix printing of Verilog with new datatypesYann Herklotz2020-06-122-17/+27
* Remove Verilog proofsYann Herklotz2020-06-123-133/+10
* Declare all registers properly in HTLYann Herklotz2020-06-123-51/+95
* Remove extraction of simulatorYann Herklotz2020-06-121-2/+2
* Fix top level invocation to translate through HTLYann Herklotz2020-06-122-4/+8
* Remove Test.vYann Herklotz2020-06-121-99/+0
* Generate Verilog from HTLYann Herklotz2020-06-122-713/+154
* Start fixing proofJames Pollard2020-06-091-94/+116
* Fix automation tactic for modified constructorJames Pollard2020-06-091-2/+4
* Start extending HTL proof to cover arrays.James Pollard2020-06-091-18/+31
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-094-56/+156
|\
| * Finished main proof with small assumptionsYann Herklotz2020-06-045-59/+157
* | Fix HTLgenspec proof for arrays.James Pollard2020-06-031-31/+43
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-033-47/+50
|\|
| * Uncomment proofYann Herklotz2020-06-033-43/+46
* | HTLgenspec status in line with developJames Pollard2020-06-033-26/+57
* | Copy over load/store from Veriloggen to HTLgen.James Pollard2020-06-031-5/+36
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-033-6/+32
|\|
| * Add proof to final_statesYann Herklotz2020-06-022-3/+5
| * Add proof for initial stateYann Herklotz2020-06-022-3/+27
* | Keep track of declarations in HTLgen.James Pollard2020-06-031-23/+62
* | Update HTL semantics to support arrays.James Pollard2020-06-022-19/+32
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-024-84/+185
|\|
| * 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-023-40/+143
| * Add lemmas for preservation of globalsYann Herklotz2020-06-012-29/+50
* | Paramterise associations type to avoid some duplication.James Pollard2020-06-021-44/+40
* | 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
generated by cgit (git 2.34.1) at 2024-07-01 13:47:43 +0000