* missing: WR-to-RD

* prove that CAS commands are preceded by an ACT with the same row with no
  other ACT or PRE command in between

* less direct proofs
* instead use general properties of the FIFO implementation

Added upper-level module for the memory, also a RT module for separating the RT part from the functional part of the bank

Coming back to a single branch

See merge request florian.brandner/sdram!1

TLA+ : Model works, but income of requests is too heavy, have to model the system to be less charged