Added upper-level module for the memory, also a RT module for separating the...

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

TLAplus/DRAMModules/Memory.tla

+------------------------------- MODULE Memory -------------------------------
+CONSTANTS 
+    NoOfBanks
+    
+VARIABLES
+    banks
+
+BANK(S) == INSTANCE Bank WITH 
+
+
+=============================================================================
+\* Modification History
+\* Last modified Thu Mar 11 09:04:53 CET 2021 by felipe
+\* Created Wed Mar 10 18:23:27 CET 2021 by felipe

TLAplus/DRAMModules/RTBank.tla

+-------------------------------- MODULE Bank --------------------------------
+\* Using integers for real time now
+EXTENDS Integers
+
+\* This is not the controller !!
+
+CONSTANTS
+    \* Excluseviley intra-bank constraints
+    t_RCD, \* ACT to RD/WR
+    t_RP, \* PRE to ACT
+    t_RC, \* ACT to ACT
+    t_RAS, \* ACT to PRE
+    t_WL, \* WR to USEBUS
+    t_RL, \* RD to USEBUS
+    t_RTP, \* RD to PRE
+    t_WR, \* RLSBUS (WR) to PRE
+    \* Inter- and intra-bank constraints
+    t_RTW, \* RD to WR
+    t_WR_to_RD, \* WR to RD
+    t_WTR, \* RLSBUS to RD
+    t_BURST, \* USEBUS to RLSBUS
+    t_CCD \* RD-to-RD or WR-to-WR
+
+\* Have to create bus module ?? Or do I just think about the bus effect on
+\* the bank constraints ? If that's case than I don't need to write a bus module
+\* INSTANCE
+
+\* The timing constraints should be part of the bank module
+\* This model should have the cont-down timers related to intra bank constraints
+CMDS == {"ACT","RD","WR","PRE"}
+CMDS_PLUSREF == CMDS \cup {"REF"}
+CMDS_PLUSBUS == CMDS \cup {"USEBUS","RLSBUS"}
+
+\* Maybe have a variable to know if it is a RD or a WR ??
+VARIABLES
+    input_cmd,
+    last_cmd,
+    ACT_lbtimer,
+    RD_lbtimer,
+    WR_lbtimer,
+    USEBUS_lbtimer,
+    RLSBUS_lbtimer,
+    PRE_lbtimer
+
+vars == <<input_cmd,last_cmd,ACT_lbtimer,RD_lbtimer,WR_lbtimer,USEBUS_lbtimer,RLSBUS_lbtimer,PRE_lbtimer>>
+
+TypeOK ==
+    /\ input_cmd \in CMDS_PLUSREF
+    /\ last_cmd \in CMDS_PLUSREF
+    /\ ACT_lbtimer \in [CMDS_PLUSBUS -> 0..100]
+    /\ RD_lbtimer \in [CMDS_PLUSBUS -> 0..100]
+    /\ WR_lbtimer \in [CMDS_PLUSBUS -> 0..100]
+    /\ USEBUS_lbtimer \in [CMDS_PLUSBUS -> 0..100]
+    /\ RLSBUS_lbtimer \in [CMDS_PLUSBUS -> 0..100]
+    /\ PRE_lbtimer \in [CMDS_PLUSBUS -> 0..100]
+
+Init_Bank ==
+    /\ input_cmd = "NONE"
+    /\ last_cmd = "PRE"
+    /\ ACT_lbtimer = [cmd \in CMDS_PLUSBUS |-> 0]
+    /\ RD_lbtimer = [cmd \in CMDS_PLUSBUS |-> 0]
+    /\ WR_lbtimer = [cmd \in CMDS_PLUSBUS |-> 0]
+    /\ USEBUS_lbtimer = [cmd \in CMDS_PLUSBUS |-> 0]
+    /\ RLSBUS_lbtimer = [cmd \in CMDS_PLUSBUS |-> 0]
+    /\ PRE_lbtimer = [cmd \in CMDS_PLUSBUS |-> 0]
+-----------------------------------------------------------------------------
+\* An ACT can happen at any moment but is restrained by timing constraints
+IssueACT ==
+    /\ input_cmd = "ACT"
+    /\ ACT_lbtimer["ACT"] = 0
+    /\ ACT_lbtimer["PRE"] = 0
+    /\ last_cmd' = "ACT"
+    /\ ACT_lbtimer' = [ACT_lbtimer EXCEPT !["ACT"] = t_RC]
+    /\ RD_lbtimer' = [RD_lbtimer EXCEPT !["ACT"] = t_RCD]
+    /\ WR_lbtimer' = [WR_lbtimer EXCEPT !["ACT"] = t_RCD]
+    /\ PRE_lbtimer' = [PRE_lbtimer EXCEPT !["ACT"] = t_RAS]
+    /\ UNCHANGED<<input_cmd,USEBUS_lbtimer,RLSBUS_lbtimer>>
+
+IssueRD ==
+    /\ input_cmd = "RD"
+    /\ last_cmd /= "PRE"
+    /\ \A cmds \in CMDS_PLUSBUS : RD_lbtimer[cmds] = 0
+    /\ last_cmd' = "RD"
+    /\ RD_lbtimer' = [RD_lbtimer EXCEPT !["RD"] = t_CCD]
+    /\ WR_lbtimer' = [WR_lbtimer EXCEPT !["RD"] = t_RTW]
+    /\ USEBUS_lbtimer' = [USEBUS_lbtimer EXCEPT !["RD"] = t_RL]
+    /\ PRE_lbtimer' = [PRE_lbtimer EXCEPT !["RD"] = t_RTP]
+    /\ UNCHANGED<<input_cmd,ACT_lbtimer,RLSBUS_lbtimer>>
+
+-----------------------------------------------------------------------------
+Next_Bank ==
+    \/ IssueACT
+    \/ IssueRD
+
+Spec_Bank = Init_Bank /\ [][Next_Bank]_vars
+=============================================================================
+\* Modification History
+\* Last modified Thu Mar 11 09:05:26 CET 2021 by felipe
+\* Created Wed Mar 10 16:03:58 CET 2021 by felipe