Commits · trunk · tacoq / storebuffer · GitLab

Snippets Groups Projects

Jan 25, 2023
- Prepare for publication · f5028430
  Alban Gruin authored 2 years ago
  f5028430
Dec 29, 2022
- src: remove old files · f69ee741
  Alban Gruin authored 2 years ago
  f69ee741
- modular_store_buffer: ??? · a9b3dd9c
  Alban Gruin authored 2 years ago
  a9b3dd9c
- correct_store_buffer: remove unused definitions · 37796cba
  Alban Gruin authored 2 years ago
  37796cba
- modular_definitions: remove unused definitions · 89a90377
  Alban Gruin authored 2 years ago
  89a90377
- utils: cleanup · 773f2fc5
  Alban Gruin authored 2 years ago
  773f2fc5
- fivestage: cleanup · b8bd03d3
  Alban Gruin authored 2 years ago
  b8bd03d3
Oct 05, 2022
- modular_store_buffer: support latencies in all stages · 57ee160b
  Alban Gruin authored 2 years ago
  57ee160b
- Modular definitions · c5b3c190
  Alban Gruin authored 2 years ago
  c5b3c190
Jul 29, 2022
- correct_store_buffer: exclude cases that are not possible · 335b54b2
  Alban Gruin authored 2 years ago
  335b54b2
- correct_store_buffer: add a parameter to HbusFree · 6977e6b7
  Alban Gruin authored 2 years ago
  6977e6b7
- correct_store_buffer: generalize work_on_e for two instructions · 7350a43b
  Alban Gruin authored 2 years ago
  7350a43b
- correct_store_buffer: add comments for clarity · e4a71034
  Alban Gruin authored 2 years ago
  e4a71034
- correct_store_buffer: rename lemmas for clarity · b5678f75
  Alban Gruin authored 2 years ago
  b5678f75
- correct_store_buffer: the store buffer is monotonic · 9cfc8c03
  Alban Gruin authored 2 years ago
  9cfc8c03
- correct_store_buffer: the behaviour is monotonic if e ⊏ e' · 47a9db6d
  Alban Gruin authored 2 years ago
  47a9db6d
Jul 27, 2022
- correct_store_buffer: proof simplification · 71722fe9
  Alban Gruin authored 2 years ago
  71722fe9
- definitions: instr_kinds are either the same or different · 75e2fe1f
  Alban Gruin authored 2 years ago
  75e2fe1f
Jul 26, 2022
- definitions, correct_store_buffer: latencies in Loads · ccb0db5d
  Alban Gruin authored 2 years ago
  ccb0db5d
- correct_store_buffer: an more advanced instruction stays more advanced · 10da722c
  Alban Gruin authored 2 years ago
  10da722c
- correct_store_buffer: if an instruction remains in the same stage, it progresses · 62aa10be
  Alban Gruin authored 2 years ago
  62aa10be
- correct_store_buffer: base hypothesis for monotonicity proofs · d535301a
  Alban Gruin authored 2 years ago
  d535301a
- correct_store_buffer: specify how the store buffer can evolve · 658b618b
  Alban Gruin authored 2 years ago
  658b618b
- correct_store_buffer: simplify proofs · 236fb32e
  Alban Gruin authored 2 years ago
  236fb32e
- correct_store_buffer: add comments in luFree and suFree · 97f0021e
  Alban Gruin authored 2 years ago
  97f0021e
- correct_store_buffer: fix ready and free functions · cb51a550
  Alban Gruin authored 2 years ago
  cb51a550
- definitions: add a function to compare the whole pipeline · 1c22af68
  Alban Gruin authored 2 years ago
  1c22af68
- definitions: fix state_leb, proofs related to that function · 2b6149c0
  Alban Gruin authored 2 years ago
  2b6149c0
- definitions: prove that stage_beq s s = true · 4deb1b6e
  Alban Gruin authored 2 years ago
  4deb1b6e
- definitions: simplify proofs · a543cf79
  Alban Gruin authored 2 years ago
  a543cf79
- utils: simplification of proofs · 6ae7da3d
  Alban Gruin authored 2 years ago
  6ae7da3d
Jul 05, 2022
- correct_sb: define cycle_on_more_advanced · 53b81285
  Alban Gruin authored 2 years ago
  53b81285
- correct_sb: cleanup proofs · 23412a35
  Alban Gruin authored 2 years ago
  23412a35
- rc: move sbStateT to definitions · c59de73d
  Alban Gruin authored 2 years ago
  c59de73d
Jul 04, 2022
- correct_store_buffer: prove that an unconstrained Load in Lsu can advance · c6795c42
  Alban Gruin authored 2 years ago
  c6795c42
- correct_store_buffer: redefine constaints and use it in the proofs · 7ee4f352
  Alban Gruin authored 2 years ago
  7ee4f352
- correct_store_buffer: prove that a constrained store can advance · d943294e
  Alban Gruin authored 2 years ago
  d943294e
- correct_store_buffer: prove that an unconstrained Sp can advance · ae48254e
  Alban Gruin authored 2 years ago
  ae48254e
- correct_store_buffer: new store buffer definition · 4b36b928
  Alban Gruin authored 2 years ago
  4b36b928
- store_buffer: move compare_two to definitions · 3d4f7f60
  Alban Gruin authored 2 years ago
  3d4f7f60