Skip to content
Snippets Groups Projects
Select Git revision
  • _frozen_version_ default
  • finaldev
  • master protected
  • newimpl
  • newimpl_14_12_23
5 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.019Apr814Mar118121Feb1312830Jan214Dec616Nov27Oct24Aug20Jul105Jan3230Dec29252018Nov168Sep2131Aug27May84126Apr25201928Mar22721Jan201710Dec21Nov201918151426Oct1211827Jul19826May21191817167654329Apr282311Mar105326Feb232220121027JanUpdated README_frozen_version__frozen_version_Removed irrelevant submodulesRevert submodules changeChanged submodulesCavaDRAMUpdated TDMShelve -- RefreshGrantChanged axiom about private bank mapping in TDM; Renamed things to TDMShelveExample for thesis is fully functional. Corrected some errorsFixed scheduling alg error: looks to be OK nowdsTDMimpSL function, implemented grantsFirst complete implementation of dsTDM. Updated some CavaDRAM proofsRe-structured CavaDRAM library, updated some things in CoqDRAMCorrection on sub-module urlAdded silveroak as submoduleCleanning CavaDRAM code, added silveroak recompiled to sub-module listStable, clean, versionAdded refresh version of normal implementationsSuccesfull merge between CavaDRAM most updated version and CoqDRAMUpdated gitignorenewimpl_14_12_23newimpl_14_12_23New version of TDM fully functionalFinished refactoring FIFO conforming the new version of the frameworkFirst proof (T_RCD) of bank machine completedStable development, proof almost finishedUpdate on devUpdate codenewimplnewimplRe-structuring the code base, new implementation interfacefinaldevfinaldevNew version of the frameworkAdded new scheduling algorithms: dynamic TDMUpdated ddr4controller submodulemastermasterRecent changes in CavaDRAM proofsFinished subtractor proof, moved proofs to UtilSM, changed request definitionSix cases complete, separated proofsFourth case completed / Got rid of the pop signalEquivalence proof: 4th caseEquivalence proof: 3rd caseEquivalence proof: two cases completeFIFO proof breakpoint: changing refresh counter implementationUpdated READMEUpdated CavaDRAM proofsRenamed file path to match CoqDRAM / CavaDRAM