aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
...
| * 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
| * Finish initial implementation of memory genYann Herklotz2021-03-012-2/+89
| * Change lists in case statements to stmnt_listYann Herklotz2021-03-015-12/+29
| * Add initial memory generationYann Herklotz2021-03-011-0/+17
* | Use new HTLgenspec in proofMichalis Pardalos2021-08-221-3/+27
* | Move list lemmas to own fileMichalis Pardalos2021-08-221-21/+1
* | Add length args = length params to Icall specMichalis Pardalos2021-08-211-44/+80
* | Strengthen HTLgenspecMichalis Pardalos2021-08-201-9/+14
* | More progress in Icall proofMichalis Pardalos2021-08-191-14/+16
* | Find called module in Icall proofMichalis Pardalos2021-08-194-29/+39
* | Complete HTLspec (mostly)Michalis Pardalos2021-08-122-51/+130
* | Tie clocks in the ApplyExternctrl passMichalis Pardalos2021-08-122-2/+7
* | Get HTLgenproof passing with updated specMichalis Pardalos2021-08-061-3/+3
* | Correct lookup for called funcs, simplify tr_moduleMichalis Pardalos2021-08-043-32/+61
* | Check whether callee is internal for IcallMichalis Pardalos2021-08-022-25/+24
* | Add "join state is <=Int.max_unsigned" to HTLgenspecMichalis Pardalos2021-06-102-10/+13
* | Remove all Admitted from top-level Compiler.vMichalis Pardalos2021-06-105-383/+588
* | Make externctrl application its own HTL passMichalis Pardalos2021-06-063-184/+225
generated by cgit (git 2.34.1) at 2024-06-28 14:24:11 +0000