| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Finish load proofdev/scheduling | Yann Herklotz | 2023-11-05 | 8 | -1930/+3243 |
| * | Changed and proved some more theorems | Yann Herklotz | 2023-10-30 | 4 | -1338/+2192 |
| * | Fix more proofs moving to proving instructions | Yann Herklotz | 2023-10-20 | 2 | -13/+247 |
| * | Fix compilation without FunctionUnits | Yann Herklotz | 2023-10-20 | 1 | -1/+1 |
| * | Finish Giblesubpargenproof | Yann Herklotz | 2023-10-20 | 1 | -7/+13 |
| * | Nearly finish the subpargenproof | Yann Herklotz | 2023-10-20 | 1 | -2/+130 |
| * | Add the actual proof | Yann Herklotz | 2023-10-19 | 3 | -0/+2025 |
| * | Finished most of the giblesubpar proof | Yann Herklotz | 2023-10-19 | 9 | -41/+138 |
| * | Add more sub languages | Yann Herklotz | 2023-10-19 | 4 | -1/+608 |
| * | More work on proof | Yann Herklotz | 2023-10-18 | 6 | -118/+676 |
| * | Add callstate correct proof | Yann Herklotz | 2023-10-13 | 2 | -13/+248 |
| * | Add changes for HTL proof | Yann Herklotz | 2023-10-13 | 10 | -262/+498 |
| * | Add settings file | Yann Herklotz | 2023-10-06 | 2 | -0/+5 |
| * | Finish eval_correct proof | Yann Herklotz | 2023-10-06 | 5 | -248/+1043 |
| * | Add incremental evaluability check | Yann Herklotz | 2023-09-25 | 6 | -11/+1127 |
| * | Add better implementation of evaluability | Yann Herklotz | 2023-09-22 | 1 | -28/+38 |
| * | Add timing of scheduling to Compiler.v | Yann Herklotz | 2023-09-22 | 2 | -40/+40 |
| * | Add new constraints checking | Yann Herklotz | 2023-09-22 | 1 | -1/+56 |
| * | Fix documentation generation | Yann Herklotz | 2023-09-17 | 4 | -330/+625 |
| * | Add Bambu synthesis and ClockRegisters | Yann Herklotz | 2023-08-11 | 4 | -0/+414 |
| * | Fix backend hardware generation and scheduling | Yann Herklotz | 2023-08-11 | 13 | -66/+114 |
| * | Put every load/store into it's own cycle | Yann Herklotz | 2023-08-02 | 3 | -179/+204 |
| * | Finish datapath memory generation | Yann Herklotz | 2023-08-02 | 2 | -409/+546 |
| * | Fixing store transformation | Yann Herklotz | 2023-08-01 | 3 | -96/+179 |
| * | Add fixes to main memory generation proof | Yann Herklotz | 2023-07-31 | 2 | -799/+808 |
| * | Remove RTLParFu and fix DMemorygen.v | Yann Herklotz | 2023-07-31 | 5 | -1974/+1949 |
| * | Add beginning to memory generation proof | Yann Herklotz | 2023-07-29 | 22 | -2671/+6810 |
| * | Add equivalence classes | Yann Herklotz | 2023-07-11 | 10 | -192/+552 |
| * | Add if-conversion decision procedure | Yann Herklotz | 2023-07-06 | 6 | -29/+60 |
| * | Fix man file generation | Yann Herklotz | 2023-06-26 | 2 | -4/+3 |
| * | Update cohpred with renamed files | Yann Herklotz | 2023-06-26 | 1 | -0/+0 |
| * | Add COHPREDSTAMP to .gitignore | Yann Herklotz | 2023-06-26 | 1 | -0/+2 |
| * | Finish some proofs and remove unnecessary Admitted | Yann Herklotz | 2023-06-26 | 7 | -33/+76 |
| * | Finish mutual exclusivity check | Yann Herklotz | 2023-06-25 | 5 | -31/+150 |
| * | Finish SMT proof | Yann Herklotz | 2023-06-23 | 1 | -3/+100 |
| * | Add SMTCoq solver as dependency | Yann Herklotz | 2023-06-21 | 14 | -71/+233 |
| * | Update makefile to build cohpred | Yann Herklotz | 2023-06-19 | 1 | -2/+6 |
| * | Update cohpred library | Yann Herklotz | 2023-06-18 | 1 | -0/+0 |
| * | Update cohpred git submodule | Yann Herklotz | 2023-06-14 | 2 | -1/+1 |
| * | Add CohPred and SMTCoq dependency | Yann Herklotz | 2023-06-12 | 4 | -2/+29 |
| * | Finish complete evaluability proof | Yann Herklotz | 2023-06-10 | 1 | -19/+88 |
| * | Try to prove main theorem | Yann Herklotz | 2023-06-10 | 1 | -0/+5 |
| * | Add more to proof of evaluability | Yann Herklotz | 2023-06-10 | 2 | -1/+57 |
| * | Finish abstract_sequence_evaluable_m | Yann Herklotz | 2023-06-09 | 1 | -1/+104 |
| * | Prove abstract_sequence_evaluable | Yann Herklotz | 2023-06-09 | 1 | -0/+2 |
| * | Finish abstract_sequence_evaluable_fold2 | Yann Herklotz | 2023-06-09 | 1 | -5/+42 |
| * | Finish abstract_sequence_evaluable_fold | Yann Herklotz | 2023-06-09 | 1 | -12/+68 |
| * | Add outline of proof of evaluable when predicate is false | Yann Herklotz | 2023-06-09 | 1 | -19/+54 |
| * | Add proof outline for evaluability | Yann Herklotz | 2023-06-08 | 2 | -20/+44 |
| * | Work towards proving evaluability | Yann Herklotz | 2023-06-05 | 3 | -38/+169 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |