aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
...
| * Basically done with proofYann Herklotz2021-04-076-18/+62
| |
| * Let everything compile againYann Herklotz2021-04-061-7/+18
| |
| * Finish load and store proof, but broke top-levelYann Herklotz2021-04-067-289/+317
| |
| * Finish Veriloggenproof completelyYann Herklotz2021-04-044-57/+339
| |
| * Prove all admit in load but oneYann Herklotz2021-04-041-162/+183
| |
| * Finish most of load proofYann Herklotz2021-04-041-21/+167
| |
| * Finish store proof without admitYann Herklotz2021-04-042-189/+533
| |
| * Fix initialisation moreYann Herklotz2021-04-011-7/+7
| |
| * Add 0 initialisationYann Herklotz2021-04-011-1/+1
| |
| * Add declarationsYann Herklotz2021-04-011-6/+7
| |
| * Add new enable interfaceYann Herklotz2021-04-014-53/+66
| |
| * Add memory disableYann Herklotz2021-03-314-163/+306
| |
| * Temporary doneYann Herklotz2021-03-301-48/+247
| |
| * Add more checks to the implementationYann Herklotz2021-03-291-27/+82
| |
| * Update declared sizeYann Herklotz2021-03-281-1/+1
| |
| * Finish main match proof in storeYann Herklotz2021-03-281-50/+555
| |
| * Add proofs of size preservation of statements and ramYann Herklotz2021-03-251-47/+92
| |
| * Work more on size-preserving lemmasYann Herklotz2021-03-251-104/+129
| |
| * Add forall_ram proofYann Herklotz2021-03-251-6/+40
| |
| * Prove lt property for statementsYann Herklotz2021-03-251-4/+67
| |
| * Add many more array theoremsYann Herklotz2021-03-241-4/+100
| |
| * Completed match_arrs_gss proofYann Herklotz2021-03-231-21/+100
| |
| * Complete top-level again with smaller admittedYann Herklotz2021-03-221-24/+48
| |
| * Fix second part of proof againYann Herklotz2021-03-221-18/+43
| |
| * Finish unchanged proof without admitsYann Herklotz2021-03-221-21/+175
| |
| * Finish a merging proofYann Herklotz2021-03-211-12/+30
| |
| * Add many lemmas about arraysYann Herklotz2021-03-212-29/+250
| |
| * Add check for ram in moduleYann Herklotz2021-03-201-16/+161
| |
| * Prove very top-level theoremYann Herklotz2021-03-192-83/+176
| |
| * Fix proof with new array matchingYann Herklotz2021-03-171-20/+47
| |
| * Fix main proofs with smaller admitsYann Herklotz2021-03-171-25/+50
| |
| * Proof of equivalent stmnt runs with matching startYann Herklotz2021-03-171-155/+263
| |
| * Prove one case of transf_code correctYann Herklotz2021-03-161-1/+54
| |
| * Greatly simplify proofYann Herklotz2021-03-161-44/+23
| |
| * Finish proof of simple transformationYann Herklotz2021-03-161-0/+90
| |
| * Fix memory inferrence generationYann Herklotz2021-03-151-28/+32
| |
| * Move implicit argsYann Herklotz2021-03-151-2/+2
| |
| * Fix Verilog importsYann Herklotz2021-03-141-14/+20
| |
| * Remove comments in Verilog.vYann Herklotz2021-03-141-194/+0
| |
| * Prove top-level theorem with admitted theoremsYann Herklotz2021-03-122-159/+193
| |
| * Try and fix identity proof in MemorygenYann Herklotz2021-03-121-1/+12
| |
| * Prove idempotency of array mergeYann Herklotz2021-03-112-20/+86
| |
| * Update RAM generation proofsYann Herklotz2021-03-093-70/+472
| |
| * Add negative edge reasoning to HTLgenproofYann Herklotz2021-03-092-12/+109
| |
| * Add RAM semantics to HTL and fix proofYann Herklotz2021-03-034-18/+132
| |
| * Add implementationYann Herklotz2021-03-022-29/+80
| |
| * Add option to turn on/off ram inferrenceYann Herklotz2021-03-024-2/+9
| |
| * Add RAM to HTLYann Herklotz2021-03-024-1/+4
| |
| * Fix memory generation by generating a power of 2Yann Herklotz2021-03-021-34/+50
| |
| * Print Verilog in reverse orderYann Herklotz2021-03-021-1/+1
| |
generated by cgit (git 2.34.1) at 2024-06-30 21:06:35 +0000