| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Finish load proofdev/scheduling | Yann Herklotz | 2023-11-05 | 7 | -1930/+3237 |
| * | 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 | 5 | -41/+131 |
| * | Add more sub languages | Yann Herklotz | 2023-10-19 | 3 | -0/+603 |
| * | 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 | 9 | -260/+493 |
| * | Finish eval_correct proof | Yann Herklotz | 2023-10-06 | 5 | -248/+1043 |
| * | Add incremental evaluability check | Yann Herklotz | 2023-09-25 | 4 | -6/+1116 |
| * | Add better implementation of evaluability | Yann Herklotz | 2023-09-22 | 1 | -28/+38 |
| * | Add new constraints checking | Yann Herklotz | 2023-09-22 | 1 | -1/+56 |
| * | Add Bambu synthesis and ClockRegisters | Yann Herklotz | 2023-08-11 | 1 | -0/+245 |
| * | Fix backend hardware generation and scheduling | Yann Herklotz | 2023-08-11 | 6 | -42/+80 |
| * | 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 | 17 | -2662/+6789 |
| * | Add equivalence classes | Yann Herklotz | 2023-07-11 | 6 | -191/+334 |
| * | Add if-conversion decision procedure | Yann Herklotz | 2023-07-06 | 5 | -27/+53 |
| * | Finish some proofs and remove unnecessary Admitted | Yann Herklotz | 2023-06-26 | 5 | -32/+74 |
| * | Finish mutual exclusivity check | Yann Herklotz | 2023-06-25 | 4 | -30/+121 |
| * | Finish SMT proof | Yann Herklotz | 2023-06-23 | 1 | -3/+100 |
| * | Add SMTCoq solver as dependency | Yann Herklotz | 2023-06-21 | 6 | -47/+216 |
| * | 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 |
| * | Move around generating functions | Yann Herklotz | 2023-06-03 | 2 | -68/+68 |
| * | Fix proof of predicates completely | Yann Herklotz | 2023-06-02 | 2 | -7/+24 |
| * | Fix top-level proof with Isetpred missing | Yann Herklotz | 2023-06-02 | 1 | -12/+55 |
| * | Finished the propert version of from_predicated_sem_pred_expr2 | Yann Herklotz | 2023-06-02 | 6 | -44/+304 |
| * | Finish from_predicated_sem_pred_expr | Yann Herklotz | 2023-05-31 | 1 | -8/+97 |
| * | Remove unnecessary assumption from sem_merge_list | Yann Herklotz | 2023-05-30 | 1 | -4/+3 |
| * | Fix other proofs and attempt from_predicated proof | Yann Herklotz | 2023-05-30 | 1 | -7/+26 |
| * | Prove merge list_translation | Yann Herklotz | 2023-05-30 | 1 | -2/+16 |
| * | Prove fold_right over Elist | Yann Herklotz | 2023-05-30 | 1 | -4/+74 |
| * | Finish second flap2 proof | Yann Herklotz | 2023-05-30 | 1 | -1/+9 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |