aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
...
* | | Use sumbool instead of option for decide_ram_wfMichalis Pardalos2021-09-013-12/+12
* | | Start renaming from 2, fixes wf_params checkMichalis Pardalos2021-09-011-1/+1
* | | Give specific reasons when ApplyExternctrl failsMichalis Pardalos2021-09-011-1/+5
* | | Fix control register ordering in Renaming passMichalis Pardalos2021-09-011-5/+7
* | | Give more specific reasons for Renaming failingMichalis Pardalos2021-09-011-1/+5
* | | Get HTLgenproof to compile with RAM inferenceMichalis Pardalos2021-08-311-2/+9
* | | Get Memorygen to compile againMichalis Pardalos2021-08-311-475/+484
* | | Get HTLgenspec compiling with RAM inferenceMichalis Pardalos2021-08-311-2/+2
* | | Get HTLgen compiling with RAM inferenceMichalis Pardalos2021-08-311-9/+9
* | | Get Renaming compiling with RAM inferenceMichalis Pardalos2021-08-313-24/+37
* | | Get ApplyExternctrl compiling with RAM inferenceMichalis Pardalos2021-08-311-8/+16
* | | WIPMichalis Pardalos2021-08-306-140/+160
* | | Merge branch 'oopsla21' into sharing-mergeMichalis Pardalos2021-08-2618-1405/+3927
|\| |
| * | Remove more OCaml files to compile successfully without admits.Yann Herklotz2021-07-114-1084/+0
| * | Remove unnecessary files and proofsYann Herklotz2021-07-114-9/+12
| * | Add legup scriptYann Herklotz2021-07-111-1/+1
| |/
| * Clean up Memorygen fileYann Herklotz2021-04-071-219/+1
| * 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
| * 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
generated by cgit (git 2.34.1) at 2024-06-28 15:57:39 +0000