Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • trunk default protected
1 result
Created with Raphaël 2.2.025Jan29Dec5Oct29Jul272654Prepare for publicationtrunktrunksrc: remove old filesmodular_store_buffer: ???correct_store_buffer: remove unused definitionsmodular_definitions: remove unused definitionsutils: cleanupfivestage: cleanupmodular_store_buffer: support latencies in all stagesModular definitionscorrect_store_buffer: exclude cases that are not possiblecorrect_store_buffer: add a parameter to HbusFreecorrect_store_buffer: generalize work_on_e for two instructionscorrect_store_buffer: add comments for claritycorrect_store_buffer: rename lemmas for claritycorrect_store_buffer: the store buffer is monotoniccorrect_store_buffer: the behaviour is monotonic if e ⊏ e'correct_store_buffer: proof simplificationdefinitions: instr_kinds are either the same or differentdefinitions, correct_store_buffer: latencies in Loadscorrect_store_buffer: an more advanced instruction stays more advancedcorrect_store_buffer: if an instruction remains in the same stage, it progressescorrect_store_buffer: base hypothesis for monotonicity proofscorrect_store_buffer: specify how the store buffer can evolvecorrect_store_buffer: simplify proofscorrect_store_buffer: add comments in luFree and suFreecorrect_store_buffer: fix ready and free functionsdefinitions: add a function to compare the whole pipelinedefinitions: fix state_leb, proofs related to that functiondefinitions: prove that stage_beq s s = truedefinitions: simplify proofsutils: simplification of proofscorrect_sb: define cycle_on_more_advancedcorrect_sb: cleanup proofsrc: move sbStateT to definitionscorrect_store_buffer: prove that an unconstrained Load in Lsu can advancecorrect_store_buffer: redefine constaints and use it in the proofscorrect_store_buffer: prove that a constrained store can advancecorrect_store_buffer: prove that an unconstrained Sp can advancecorrect_store_buffer: new store buffer definitionstore_buffer: move compare_two to definitions