aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * Add function call testYann Herklotz2020-06-121-0/+10
| * Update compcert to always inline functionsYann Herklotz2020-06-121-0/+0
| * Fix main functionYann Herklotz2020-06-121-17/+3
| * Add array to testYann Herklotz2020-06-122-1/+5
| * 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
| * Merge pull request #5 from p0llard/arrays-proofYann Herklotz2020-06-107-351/+643
| |\
* | | Some work on store proof.James Pollard2020-06-121-11/+38
* | | Rough outline of stack address proofJames Pollard2020-06-113-34/+109
* | | Working on proof.James Pollard2020-06-115-47/+156
| |/ |/|
* | 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-098-56/+1160
|\|
| * Add optimisationsYann Herklotz2020-06-051-0/+1
| * Add dhrystone benchmarkYann Herklotz2020-06-054-0/+1003
| * 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-3025-369/+2277
|\|
| * 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
generated by cgit (git 2.34.1) at 2024-07-15 20:36:56 +0000