aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog
Commit message (Expand)AuthorAgeFilesLines
...
| * Fix array semantics merge granularity.James Pollard2020-06-173-30/+80
| * Array semantics now uses dependent Array type.James Pollard2020-06-142-39/+39
| * Add a basic length-indexed list type.James Pollard2020-06-131-0/+123
| * Merge branch 'master' into arrays-proofJames Pollard2020-06-125-188/+149
| |\
| * | Rough outline of stack address proofJames Pollard2020-06-111-4/+4
| * | Working on proof.James Pollard2020-06-112-6/+20
* | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-142-2/+5
| |/ |/|
* | Fix declaring function arguments correctlyYann Herklotz2020-06-121-3/+3
* | Fix printing of Verilog with new datatypesYann Herklotz2020-06-122-17/+27
* | Remove Verilog proofsYann Herklotz2020-06-121-1/+6
* | Remove Test.vYann Herklotz2020-06-121-99/+0
* | Generate Verilog from HTLYann Herklotz2020-06-121-69/+114
|/
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-093-25/+64
|\
| * Finished main proof with small assumptionsYann Herklotz2020-06-043-25/+63
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-031-0/+5
|\|
| * Uncomment proofYann Herklotz2020-06-031-0/+5
* | HTLgenspec status in line with developJames Pollard2020-06-031-0/+1
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-031-2/+2
|\|
| * Add proof to final_statesYann Herklotz2020-06-021-2/+2
* | Update HTL semantics to support arrays.James Pollard2020-06-022-19/+32
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-021-2/+33
|\|
| * Add proof for equivalence of movYann Herklotz2020-06-021-2/+33
* | 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-011-8/+15
|\|
| * Copy over RTL global stateYann Herklotz2020-06-011-8/+15
* | Merge branch 'develop' into arrays-proofJames Pollard2020-05-305-177/+756
|\|
| * Fix compilation moving to PTreeYann Herklotz2020-05-293-11/+14
| * Fix indentationYann Herklotz2020-05-291-6/+6
| * New and improved AssocmapYann Herklotz2020-05-291-7/+32
| * Change AssocMap to Maps.PTreeYann Herklotz2020-05-291-47/+66
| * Finish Assocmap proofsYann Herklotz2020-05-281-0/+59
| * Add more proofs and remove AdmittedYann Herklotz2020-05-272-16/+51
| * Add HTLgenYann Herklotz2020-05-241-5/+4
| * Finish the proof with most assumptionsYann Herklotz2020-05-211-6/+11
| * Fix the semantics to properly evaluate the stateYann Herklotz2020-05-201-2/+4
| * Switch position of empty ruleYann Herklotz2020-05-201-4/+4
| * Fix definitions in Value and add lemmasYann Herklotz2020-05-201-7/+35
| * Add theorems about mergeYann Herklotz2020-05-201-2/+12
| * Add lessdef for valuesYann Herklotz2020-05-081-3/+10
| * Add AssocMapYann Herklotz2020-05-084-47/+93
| * Redefine HTL for intermediate Verilog languageYann Herklotz2020-05-071-76/+69
| * Use associations instead of stateYann Herklotz2020-05-072-70/+69
| * Rename assoclist to assocsetYann Herklotz2020-05-072-28/+28
| * Add changes to valueYann Herklotz2020-05-061-2/+9
| * Refine test fileYann Herklotz2020-05-051-5/+2
| * Minimised manual simulationYann Herklotz2020-05-052-45/+14
| * Simplifications to proofYann Herklotz2020-05-053-18/+15
| * Finish manual simulationYann Herklotz2020-05-052-5/+68
| * Add equality check for valueYann Herklotz2020-05-042-16/+22
generated by cgit (git 2.34.1) at 2024-07-05 23:05:47 +0000