diff --git a/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL.v b/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL.v
index 8a4f5f9824375576272242b1425413784b22f2f7..a09de38de634c47e5f210d57eff2e3ba6a9d872c 100644
--- a/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL.v
+++ b/framework/DRAM/Implementations/BM/dsTDMimpSL/dsTDMimpSL.v
@@ -80,7 +80,7 @@ Section dsTDMimpSL.
 	(* ------------------------------------------------------------------ *)
 	(* ---------------- Requestor config -------------------------------- *)
 	(* ------------------------------------------------------------------ *)
-	Definition RequestorID_t := { id : nat | id < Treq}.
+	Definition RequestorID_t := {id : nat | id < Treq}.
 
 	Record dsTDM_requestor := mkRequestor {
 		(* Critical requestors have an associated slot, NC requestors do not *)
@@ -176,8 +176,9 @@ Section dsTDMimpSL.
 		specialize Treq_gt_SN as H; destruct s; simpl; lia.
 	Defined.
 
+	(* Need all elements of l to not be in s **)
 	Definition NoIntersection {T : eqType} (l s : seq T) := 
-		all (fun x => in_mem x (mem s)) l.
+		all (fun x => ~~ in_mem x (mem s)) l.
 
 	Definition AdjacentSlots (s0 s1 : Slot_t) :=
 		(s0 == Following_slot s1) || (s1 == Following_slot s0).
@@ -202,18 +203,15 @@ Section dsTDMimpSL.
 	Definition All_NC_requestors 	:= seq.iota SN NCreq.
 	Definition All_C_requestors 	:= seq.iota 0 SN.
 
-	Program Fixpoint sig_iota M n (H : n < M) : seq {x : nat | x < M} :=
+	Program Fixpoint sig_iota n M (H : n <= M) : seq {x : nat | x < M} :=
 		match n with
 		| 0 => [::]
-		| n'.+1 => (exist _ n' _) :: sig_iota M n' _
+		| n'.+1 => (exist _ n' _) :: sig_iota n' M _
 		end.
 
-	Program Definition All_requestors_sig := sig_iota Treq 0 _.
-	Next Obligation.
-		specialize Treq_gt_SN; specialize SN_pos; lia.
-	Defined.
+	Program Definition All_requestors_sig := sig_iota Treq Treq _.
 
-	Definition filter_diff_bank (s : Slot_t) := 
+	Definition filter_diff_bank (s : Slot_t) : seq RequestorID_t := 
 		filter (fun req_id =>
 			let s_id 		:= Slot_to_RequestorID s in
 			let s_bank 	:= Mapping s_id in
@@ -235,7 +233,7 @@ Section dsTDMimpSL.
 		(` TDM_st.(Slack))[@(nat_of_ord s) $0].
 
 	Definition getDeadlineFromID TDM_st (id : nat) :=
-		(` TDM_st.(Deadlines))[@id $0].
+		(` TDM_st.(Deadlines))[@id $1000].
 
 	Definition getArrivalFromID TDM_st (id : nat) :=
 		(` TDM_st.(Arrivals))[@id $false].
@@ -249,7 +247,11 @@ Section dsTDMimpSL.
 			end
 		) unfiltered_cmd_map in ~~ (f == seq.size unfiltered_cmd_map).
 
-	Definition checkIfPendingFromSlot (unfiltered_cmd_map : seq Command_kind_t) (s : Slot_t) :=
+	(* Only pick from requestors that have a pending request *)
+	Definition PendingReqs u_map (sub_list : seq RequestorID_t) := 
+		seq.filter (fun x => checkIfPendingFromID u_map (` x)) sub_list.
+	
+		Definition checkIfPendingFromSlot (unfiltered_cmd_map : seq Command_kind_t) (s : Slot_t) :=
 		let f := seq.find (fun cmd =>
 			match cmd with
 			| CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => 
@@ -282,8 +284,8 @@ Section dsTDMimpSL.
 	(* ------------------------------------------------------------------ *)
 	(* ----------- Defining update functions ---------------------------- *)
 	(* ------------------------------------------------------------------ *)
-	(* Chooses one requestor_id *)
-	Program Definition EDF (TDM_st : dsTDM_internal_state) 
+	Program Definition EDF 
+		(TDM_st : dsTDM_internal_state) 
 		(requestors : seq RequestorID_t) : RequestorID_t :=
 		foldr (fun i s =>
 			let min_deadline := getDeadlineFromID TDM_st (` s) in
@@ -294,12 +296,14 @@ Section dsTDMimpSL.
 					if (cur_deadline <= min_deadline) then i else s
 				)
 			) else ( (* non-critical requestor *)
-				if ((isCriticalRequestor s) && (min_deadline <= SL)) then s
+				if ( (* s is a critical requestor with an upcoming deadline *)
+					(isCriticalRequestor s) && 
+					(min_deadline <= SL + (SL - TDM_st.(Counter)))) then s
 				else (
 					if (cur_deadline < min_deadline) then i else s
 				)
 			)
-		) (exist _ 0 _ ) requestors. 
+		) (exist _ 0 _ ) requestors. (* Default is requestor 0 *)
 	Next Obligation.
 		specialize Treq_gt_SN; specialize SN_pos; lia.
 	Defined.
@@ -315,17 +319,17 @@ Section dsTDMimpSL.
 		| false => (* No request from next (or current) slot -> speculating based on slack *)
 			let slack := getSlackFromSlot TDM_st ns_slot in
 			if (slack >= SL - (cnt %% SL)) then (
-				EDF TDM_st All_requestors_sig
+				EDF TDM_st (PendingReqs u_map All_requestors_sig)
 			) else (
-				EDF TDM_st (filter_diff_bank ns_slot)
+				EDF TDM_st (PendingReqs u_map (filter_diff_bank ns_slot))
 			)
 		| true => 
 			let p_req_id := Slot_to_RequestorID ns_slot in
 			let p_req_deadline := getDeadlineFromID TDM_st (` p_req_id) in
-			if (p_req_deadline >= TDM_st.(Counter) + SL) then (
-				EDF TDM_st All_requestors_sig  (* EDF between everyone *)
+			if (p_req_deadline >= SL + (SL - TDM_st.(Counter))) then (
+				EDF TDM_st (PendingReqs u_map All_requestors_sig)  (* EDF between everyone *)
 			) else (
-				EDF TDM_st (filter_diff_bank ns_slot)
+				EDF TDM_st (PendingReqs u_map (filter_diff_bank ns_slot)) 
 			)
 		end.
 
@@ -363,19 +367,22 @@ Section dsTDMimpSL.
 			end
 		).
 
-	Definition UpdateDeadlines u_map TDM_st :=
+	Definition UpdateDeadlines sch_cmd u_map TDM_st :=
 		exist (fun s => seq.size s == Treq) (seq.map (fun requestor_id =>
 			(* Cycle counter *)
 			let cnt := TDM_st.(Counter) in
 			(* Dli counter *)
 			let deadl_i := getDeadlineFromID TDM_st requestor_id in
-			(* (` TDM_st.(Deadlines))[@requestor_id $ 0] in *)
 			(* Δi counter *)
 			let slack_i := getSlackFromID TDM_st requestor_id in
-			(* (` TDM_st.(Slack))[@requestor_id $ 0] in *)
 			if (requestor_id < SN) then ( (* Critical requestor *)
-				(* If deadline is 0, request completed -> replenish counter *)
-				if (deadl_i == 0) then ((SN * SL) - 1)
+				let replenish_cond := (
+					match get_req_from_cmdkind sch_cmd with
+					| None => false
+					| Some req => (isCAS_cmdkind sch_cmd) && (` req.(Requestor).(ID) == requestor_id)
+					end
+				) in
+				if ((deadl_i == 0) || replenish_cond) then (deadl_i + (SN * SL) - 1)
 				else (match checkIfPendingFromID u_map requestor_id with
 							| false =>	(* No outstanding request *)
 								if (deadl_i - slack_i <= SL - 1) then ( (* Unused slot condition *)
@@ -425,7 +432,7 @@ Section dsTDMimpSL.
 			(Next_slot TDM_st.(Slot) TDM_st.(Counter))
 			(Next_cycle TDM_st.(Counter))
 			(UpdateGrant cmd_map sch_cmd TDM_st)
-			(UpdateDeadlines cmd_map TDM_st)
+			(UpdateDeadlines sch_cmd cmd_map TDM_st)
 			(UpdateArrivals sch_cmd cmd_map TDM_st)
 			(UpdateSlack sch_cmd TDM_st).