aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Collapse)AuthorAgeFilesLines
* Icall proof progressMichalis Pardalos2021-09-131-35/+85
|
* Name the externctrl correctness clausesMichalis Pardalos2021-09-121-11/+18
|
* Guard join state with called module finishMichalis Pardalos2021-09-113-6/+14
| | | | | | Needed to match RTL semantics, since the join state executes once before the call is initiated, and we need the destination register to not be affected until after the call has returned.
* Progress with stackframe matching for IcallMichalis Pardalos2021-09-101-1/+8
|
* Prove that called module exists for IcallMichalis Pardalos2021-09-101-2/+26
|
* Fix duplicated verilog module instantiationsMichalis Pardalos2021-09-081-75/+92
|
* Print declarations in HTL outputMichalis Pardalos2021-09-082-0/+18
|
* Fix renamer skipping ram_memMichalis Pardalos2021-09-031-1/+2
|
* Print control registers in HTL outputMichalis Pardalos2021-09-031-0/+13
|
* Print RAM in HTL outputMichalis Pardalos2021-09-031-0/+17
|
* Fix error in map_externctrlMichalis Pardalos2021-09-031-1/+1
|
* Remove double clockMichalis Pardalos2021-09-031-10/+2
|
* Do not apply externctrl to control registersMichalis Pardalos2021-09-031-34/+18
|
* Address ram in renaming passMichalis Pardalos2021-09-023-14/+39
|
* 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
| |
generated by cgit (git 2.34.1) at 2024-06-28 14:30:50 +0000