aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | | | Start Aindexed proof.James Pollard2020-06-222-19/+226
| * | | | | | Tidy up proof for Aindexed2scaled.James Pollard2020-06-224-90/+231
| | |_|_|/ / | |/| | | |
| * | | | | Factor out addressing checks, check signed range.James Pollard2020-06-211-10/+17
| * | | | | Lea op now checks alignment.James Pollard2020-06-211-12/+15
| * | | | | Finish structure of Aindexed2scaled ILoad proof.James Pollard2020-06-202-14/+177
| | |/ / / | |/| | |
| * | | | Working on proof.James Pollard2020-06-191-10/+86
| * | | | Enforce stack size alignment to fix proof.James Pollard2020-06-183-10/+22
| * | | | Tidy up proof.James Pollard2020-06-182-13/+16
| * | | | Finish AInStack proof with minor assertions.James Pollard2020-06-181-32/+21
| * | | | Fix up ILoad proof.James Pollard2020-06-181-95/+58
| * | | | Fix array semantics behaviour for undefined values.James Pollard2020-06-181-1/+1
| * | | | Fix Inop proof to work with new array semantics.James Pollard2020-06-172-7/+44
| * | | | Some (very) useful lemmas about arrays.James Pollard2020-06-173-7/+139
| * | | | Use NBAs for loads and stores.James Pollard2020-06-172-4/+4
| * | | | Fix array semantics merge granularity.James Pollard2020-06-174-30/+87
| * | | | Array semantics now uses dependent Array type.James Pollard2020-06-144-48/+49
| * | | | Move some standard tactics to Coquplib.James Pollard2020-06-141-0/+10
| * | | | Add a basic length-indexed list type.James Pollard2020-06-131-0/+123
| * | | | Fix broken proof.James Pollard2020-06-121-4/+4
| * | | | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-4/+6
| |\ \ \ \
| * \ \ \ \ Merge branch 'master' into arrays-proofJames Pollard2020-06-1214-1028/+364
| |\ \ \ \ \
| * | | | | | 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
* | | | | | | Add optimisationsYann Herklotz2020-06-251-0/+16
* | | | | | | Add instructions for Cmaskzero and CmasknotzeroYann Herklotz2020-06-241-2/+2
| |_|_|_|_|/ |/| | | | |
* | | | | | Admit everything temporarilyYann Herklotz2020-06-223-9/+58
| |_|_|_|/ |/| | | |
* | | | | Only print out main as everything is inlinedYann Herklotz2020-06-221-8/+10
* | | | | Add print for debug always block in moduleYann Herklotz2020-06-222-6/+19
* | | | | Some fixes, but still buggy probablyYann Herklotz2020-06-201-2/+2
* | | | | Add bugs to support more operationsYann Herklotz2020-06-201-4/+4
| |_|_|/ |/| | |
* | | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-144-23/+31
| |_|/ |/| |
* | | Fix addressing bug.James Pollard2020-06-121-4/+6
| |/ |/|
* | Add declaration of loadsYann Herklotz2020-06-122-4/+6
* | Fix declaring function arguments correctlyYann Herklotz2020-06-123-12/+69
* | 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
generated by cgit (git 2.34.1) at 2024-07-09 01:05:00 +0000