aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
...
* | | 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 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
* | | Add Verilog generation for ramsYann Herklotz2021-03-021-18/+47
* | | Admit VeriloggenproofYann Herklotz2021-03-021-2/+3
generated by cgit (git 2.34.1) at 2024-07-18 04:30:45 +0000