Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From CoqDRAM Require Export ImplementationInterface.
From mathcomp Require Export fintype div.
Require Import Program.
Section TDM.
Context {SYS_CFG : System_configuration}.
Definition ACT_date := T_RP.
Definition CAS_date := ACT_date + T_RCD.
Definition PREA_date := (T_REFI - T_RP).
Definition REF_date := T_RP.-1.
Definition END_REF_date := REF_date + T_RFC.
Class TDM_configuration :=
{
SL : nat;
SN : nat;
SL_pos : 0 < SL;
SL_one : 1 < SL;
SL_ACT : ACT_date < SL;
SL_ACTS : ACT_date.+1 < SL;
SL_CAS : CAS_date < SL;
SL_CASS : CAS_date.+1 < SL;
SN_pos : 0 < SN;
SN_one : 1 < SN;
T_RP_GT_ONE : 1 < T_RP;
T_REFI_T_RP : T_RP < T_REFI;
T_RTP_SN_SL : T_RTP < SN * SL - CAS_date;
T_WTP_SN_SL : (T_WR + T_WL + T_BURST) < SN * SL - CAS_date;
T_RAS_SL : T_RP + T_RAS < SL;
T_RC_SL : T_RC < SL;
T_RRD_SL : T_RRD_l < SL;
T_RTW_SL : T_RTW < SL;
T_CCD_SL : T_CCD_l < SL;
WTR_SL : T_WTR_l + T_WL + T_BURST < SL;
T_FAW_3SL : T_FAW < SL + SL + SL;
PREA_date_pos : 0 < PREA_date ;
PREA_date_REF_date : REF_date < PREA_date ;
PREA_date_ENDREF_date : END_REF_date < PREA_date ;
}.
Context {TDM_CFG : TDM_configuration}.
(* SL counter *)
Definition Counter_t := ordinal SL.
Lemma Last_cycle:
SL.-1 < SL.
Proof.
rewrite ltn_predL; apply SL_pos.
Qed.
Definition OZCycle := Ordinal SL_pos.
Definition OACT_date := Ordinal SL_ACT.
Definition OCAS_date := Ordinal SL_CAS.
Definition OLastCycle := Ordinal Last_cycle.
(* SN counter *)
Definition Slot_t := ordinal_eqType SN.
Definition OZSlot := Ordinal SN_pos.
Instance REQESTOR_CFG : Requestor_configuration := {
Requestor_t := Slot_t
}.
(* REF counter *)
Definition Counter_ref_t := ordinal PREA_date.
Definition OCycle0REF := Ordinal PREA_date_pos.
Definition OREF_date := Ordinal PREA_date_REF_date.
Definition OENDREF_date := Ordinal PREA_date_ENDREF_date.
Definition Next_cycle_ref (c : Counter_ref_t) : Counter_ref_t :=
let nextcref := c.+1 < PREA_date in
(if nextcref as X return (nextcref = X -> Counter_ref_t) then
(fun (P : nextcref = true) => Ordinal (P : nextcref))
else (fun _ => OCycle0REF)) Logic.eq_refl.
Context {HAF : HW_Arrival_function_t}.
Definition Same_Slot (a b : Command_t) :=
a.(Request).(Requestor) == b.(Request).(Requestor).
Inductive TDM_state_t :=
| IDLE : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> TDM_state_t
| RUNNING : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> Request_t-> TDM_state_t
| REFRESHING : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> TDM_state_t.
Definition TDM_state_eqdef (a b : TDM_state_t) :=
match a, b with
| IDLE sa ca crefa Pa, IDLE sb cb crefb Pb
=> (sa == sb) && (ca == cb) && (crefa == crefb) && (Pa == Pb)
| RUNNING sa ca crefa Pa ra, RUNNING sb cb crefb Pb rb
=> (sa == sb) && (ca == cb) && (crefa == crefb) && (Pa == Pb) && (ra == rb)
| REFRESHING sa ca crefa Pa, REFRESHING sb cb crefb Pb
=> (sa == sb) && (ca == cb) && (crefa == crefb) && (Pa == Pb)
| _, _ => false
end.
Lemma TDM_state_eqn : Equality.axiom TDM_state_eqdef.
Proof.
Admitted.
Canonical TDM_state_eqMixin := EqMixin TDM_state_eqn.
Canonical TDM_state_eqType := Eval hnf in EqType TDM_state_t TDM_state_eqMixin.
Global Instance ARBITER_CFG : Arbiter_configuration := {
State_t := TDM_state_t;
}.
(*************************************************************************************************)
(** ARBITER IMPLEMENTATION ***********************************************************************)
(*************************************************************************************************)
(* Increment counter for cycle offset (with wrap-arround). *)
Definition Next_cycle (c : Counter_t) :=
let nextc := c.+1 < SL in
(if nextc as X return (nextc = X -> Counter_t) then
fun (P : nextc = true) => Ordinal (P : nextc)
else
fun _ => OZCycle) Logic.eq_refl.
(* Increment the slot counter (with wrap-arround) *)
Definition Next_slot (s : Slot_t) (c : Counter_t) : Slot_t :=
if (c.+1 < SL) then
s
else
let nexts := s.+1 < SN in
(if nexts as X return (nexts = X -> Slot_t) then
fun (P : nexts = true) => Ordinal (P : nexts)
else
fun _ => OZSlot) Logic.eq_refl.
Definition Enqueue (R : Request_t) (P : Requests_t) := P ++ [:: R].
Definition Dequeue r (P : Requests_t) := rem r P.
(* The set of pending requests of a slot *)
Definition Pending_of s (P : Requests_t) :=
[seq r <- P | r.(Requestor) == s].
Definition Init_state R :=
IDLE OZSlot OZCycle OCycle0REF (Enqueue R [::]).
Hint Unfold PRE_of_req : core.
Hint Unfold ACT_of_req : core.
Hint Unfold CAS_of_req : core.
Definition nullreq :=
mkReq OZSlot 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
(* The next-state function of the arbiter *)
Definition Next_state (R : Request_t) (AS : TDM_state_t)
: (TDM_state_t * (Command_kind_t * Request_t)) :=
match AS return (TDM_state_t * (Command_kind_t * Request_t)) with
| IDLE s c cref P => (* Currently no request is processed *)
let P' := Enqueue R P in (* enqueue newly arriving requests *)
let s' := Next_slot s c in (* advance slot counter (if needed) *)
let c' := Next_cycle c in (* advance slot counter (if needed) *)
let cref' := Next_cycle_ref cref in
if (cref + SN * SL < PREA_date) then (* there is enough time to start another TDM period *)
if (c == OZCycle) then
match Pending_of s P with (* Check if a request is pending *)
| [::] => (* No? Continue with IDLE *)
(IDLE s' c' cref' P', (NOP, nullreq))
| r::_ => (* Yes? Emit PRE, dequeue request, and continue with RUNNING *)
(RUNNING s' c' cref' (Enqueue R (Dequeue r P)) r, (PRE,r))
end
else (IDLE s' c' cref' P', (NOP, nullreq))
else if (nat_of_ord cref == PREA_date) then (REFRESHING s' c' OCycle0REF P', (PREA,nullreq))
else (IDLE s' c' cref' P', (NOP,nullreq))
| RUNNING s c cref P r => (* Currently a request is processed *)
let P' := Enqueue R P in (* enqueue newly arriving requests *)
let s' := Next_slot s c in (* advance slot counter (if needed) *)
let c' := Next_cycle c in (* advance slot counter (if needed) *)
let cref' := Next_cycle_ref cref in
if c == OACT_date then (* need to emit the ACT command *)
(RUNNING s' c' cref' P' r, (ACT, r))
else if c == OCAS_date then (* need to emit the CAS command *)
(RUNNING s' c' cref' P' r, (Kind_of_req r, r))
else if c == OLastCycle then (* return to IDLE state *)
(IDLE s' c' cref' P', (NOP, nullreq))
else (RUNNING s' c' cref' P' r, (NOP, r))
| REFRESHING s c cref P =>
let P' := Enqueue R P in
let s' := Next_slot s c in (* advance slot counter (if needed) *)
let c' := Next_cycle c in (* advance slot counter (if needed) *)
let cref' := Next_cycle_ref cref in
if (nat_of_ord cref == REF_date) then (REFRESHING s' c' cref' P', (REF,nullreq))
else if (nat_of_ord cref == END_REF_date) then (IDLE s' c' OCycle0REF P', (NOP, nullreq))
else (REFRESHING s' c' cref' P', (NOP,nullreq))
end.
Global Instance TDM_implementation : HWImplementation_t :=
mkHWImplementation Init_state Next_state.
(* Global Instance TDM_implementation : Implementation_t :=
mkImplementation Init_state Next_state. *)
Definition TDM_counter (AS : State_t) : Counter_t :=
match AS with
| IDLE _ c _ _ => c
| RUNNING _ c _ _ _ => c
| REFRESHING _ c _ _ => c
end.
Definition TDM_slot (AS : State_t) :=
match AS with
| IDLE s _ _ _ => s
| RUNNING s _ _ _ _ => s
| REFRESHING s _ _ _ => s
end.
Hypothesis Private_Mapping :
forall a b, Same_Bank a b ->
nat_of_ord (TDM_slot (HW_Default_arbitrate b.(CDate)).(Implementation_State)) =
nat_of_ord (TDM_slot (HW_Default_arbitrate a.(CDate)).(Implementation_State)).
(*
Definition TDM_pending (AS : State_t) :=
match AS with
| IDLE _ _ P => P
| RUNNING _ _ P _ => P
end.
Definition TDM_request (AS : State_t) :=
match AS with
| IDLE _ _ _ => None
| RUNNING _ _ _ r => Some r
end.
Definition isRUNNING (AS : State_t) :=
match AS with
| IDLE _ _ _ => false
| RUNNING _ _ _ _ => true
end. *)
End TDM.