aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Add print for debug always block in moduleYann Herklotz2020-06-223-7/+23
* Some fixes, but still buggy probablyYann Herklotz2020-06-201-2/+2
* Add bugs to support more operationsYann Herklotz2020-06-201-4/+4
* Add CHstoneYann Herklotz2020-06-1972-1/+15485
* Merge branch 'develop'Yann Herklotz2020-06-145-24/+32
|\
| * Fix coqprojectYann Herklotz2020-06-141-1/+1
| * Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-144-23/+31
|/
* Update matrix and use 32 bitYann Herklotz2020-06-123-12/+14
* Add matrix testYann Herklotz2020-06-121-0/+21
* Merge pull request #7 from p0llard/hotfixYann Herklotz2020-06-121-4/+6
|\
| * Fix addressing bug.James Pollard2020-06-121-4/+6
|/
* Add declaration of loadsYann Herklotz2020-06-122-4/+6
* Merge branch 'master' of github.com:ymherklotz/CoqUpYann Herklotz2020-06-1215-0/+19189
|\
| * Merge pull request #6 from ymherklotz/branch_jcYann Herklotz2020-06-1215-0/+19189
| |\
| | * fixed my grammarJianyi Cheng2020-06-121-2/+2
| | * Adding benchmarks to branch_jcJianyi Cheng2020-06-1215-0/+19189
| |/
* / Fix declaring function arguments correctlyYann Herklotz2020-06-123-12/+69
|/
* 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
|\
| * 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
generated by cgit (git 2.34.1) at 2024-07-03 12:56:37 +0000