aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Add the dividerdev/divYann Herklotz2021-07-071-0/+545
|
* Add dividerYann Herklotz2021-05-033-50/+202
|
* Clean up Memorygen fileYann Herklotz2021-04-071-219/+1
|
* Remove Admitted in the highest of top-levelsv1.2.0Yann Herklotz2021-04-071-5/+10
|
* No admitted theorems in Memorygen proof (~‾▿‾)~Yann Herklotz2021-04-071-76/+99
|
* 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
|
* Add logo to readmeYann Herklotz2021-04-021-6/+3
|
* 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
|