aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgen.v
Commit message (Expand)AuthorAgeFilesLines
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-654/+0
* Finished all the proofsv1.0.0Yann Herklotz2020-08-131-2/+3
* Remove alignment constraint during translation.James Pollard2020-08-111-12/+10
* Change name to VericertYann Herklotz2020-07-141-2/+2
* Fixes to operatorsYann Herklotz2020-07-071-1/+3
* Finished transl_condYann Herklotz2020-07-071-4/+0
* Only translate_cond leftYann Herklotz2020-07-071-10/+34
* Fix InopYann Herklotz2020-07-051-11/+22
* No addmitted in VeriloggenproofYann Herklotz2020-07-051-25/+60
* Fixing HTLgenproofYann Herklotz2020-07-031-11/+11
* Add new value type to fix Iop proofYann Herklotz2020-07-031-2/+2
* Updates to Iop proofYann Herklotz2020-07-031-2/+0
* Develop compiles againYann Herklotz2020-06-291-5/+5
* Fix unsigned/signed issues.James Pollard2020-06-281-12/+16
* HTLgenproof passing.James Pollard2020-06-241-4/+0
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-241-3/+2
|\
| * Fixes to make develop compileYann Herklotz2020-06-241-1/+1
* | Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proofJames Pollard2020-06-241-28/+90
|\|
| * Merge branch 'master' into developYann Herklotz2020-06-241-7/+14
| |\
| | * Fix assumption of mainYann Herklotz2020-06-241-8/+14
| * | Merge branch 'master' into developYann Herklotz2020-06-221-1/+50
| |\|
| | * Admit everything temporarilyYann Herklotz2020-06-221-1/+50
| * | Merge branch 'arrays-proof' into developYann Herklotz2020-06-221-17/+27
| |\ \
| * \ \ Merge branch 'master' into developYann Herklotz2020-06-221-5/+5
| |\ \ \ | | | |/ | | |/|
| | * | Some fixes, but still buggy probablyYann Herklotz2020-06-201-2/+2
| | * | Add bugs to support more operationsYann Herklotz2020-06-201-4/+4
| * | | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-201-19/+22
| |\ \ \ | | |/ / | |/| |
| * | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-141-19/+24
* | | | Finish ILoad proof with some assumptions:James Pollard2020-06-241-1/+5
* | | | Normalise entire expression to avoid overflow issues.James Pollard2020-06-231-5/+6
* | | | Start Aindexed proof.James Pollard2020-06-221-2/+7
* | | | Tidy up proof for Aindexed2scaled.James Pollard2020-06-221-2/+5
| |_|/ |/| |
* | | Factor out addressing checks, check signed range.James Pollard2020-06-211-10/+17
* | | Lea op now checks alignment.James Pollard2020-06-211-12/+15
| |/ |/|
* | Enforce stack size alignment to fix proof.James Pollard2020-06-181-1/+3
* | Use NBAs for loads and stores.James Pollard2020-06-171-2/+2
* | Array semantics now uses dependent Array type.James Pollard2020-06-141-7/+7
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-4/+6
|\|
| * Fix addressing bug.James Pollard2020-06-121-4/+6
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-32/+76
|\|
| * Add declaration of loadsYann Herklotz2020-06-121-0/+1
| * Fix declaring function arguments correctlyYann Herklotz2020-06-121-6/+7
| * Declare all registers properly in HTLYann Herklotz2020-06-121-32/+74
* | Rough outline of stack address proofJames Pollard2020-06-111-6/+6
* | Working on proof.James Pollard2020-06-111-3/+4
|/
* HTLgenspec status in line with developJames Pollard2020-06-031-1/+2
* Copy over load/store from Veriloggen to HTLgen.James Pollard2020-06-031-5/+36
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-031-1/+7
|\
| * Add proof for initial stateYann Herklotz2020-06-021-1/+7
* | Keep track of declarations in HTLgen.James Pollard2020-06-031-23/+62
|/
generated by cgit (git 2.34.1) at 2024-07-03 00:45:50 +0000