Spartan6.Semantics.StateAdapters

{-# OPTIONS --safe --cubical #-}

module Spartan6.Semantics.StateAdapters where

open import Spartan6.Prelude
open import Spartan6.Semantics.StateResource

import Spartan6.Primitive.FDRE as FDRE
import Spartan6.Primitive.FDSE as FDSE
import Spartan6.Primitive.BlockRAM as BlockRAM
import Spartan6.Primitive.RAM32X1S as RAM32X1S
import Spartan6.Primitive.RAM64X1S as RAM64X1S
import Spartan6.Primitive.RAM128X1D as RAM128X1D
import Spartan6.Primitive.RAM256X1S as RAM256X1S
import Spartan6.Primitive.SRL16E as SRL16E
import Spartan6.Semantics.Design as Design

-- Initial values are already typed here.  `nothing` selects the documented
-- semantic default; no raw parameter syntax is accepted by these adapters.

RegisterInitial : Type₀
RegisterInitial = Maybe Bit

decodeFDREInitial : RegisterInitial → Maybe Bit
decodeFDREInitial nothing      = just low
decodeFDREInitial (just state) = just state

decodeFDSEInitial : RegisterInitial → Maybe Bit
decodeFDSEInitial nothing      = just FDSE.fdseDefaultInit
decodeFDSEInitial (just state) = just state

record FDREInput : Type₀ where
  constructor fdreInput
  field
    fdreData   : Bit
    fdreEnable : Bit
    fdreReset  : Bit

open FDREInput public

record FDSEInput : Type₀ where
  constructor fdseInput
  field
    fdseData   : Bit
    fdseEnable : Bit
    fdseSet    : Bit

open FDSEInput public

fdreTransition : FDREInput → Bit → Bit
fdreTransition input state =
  FDRE.fdreStep
    (fdreData input) (fdreEnable input) (fdreReset input) state

fdseTransition : FDSEInput → Bit → Bit
fdseTransition input state =
  FDSE.fdseStep
    (fdseData input) (fdseEnable input) (fdseSet input) state

fdreResource : ∀ {Domain} → Domain
  → StateResource RegisterInitial FDREInput Bit Domain Bit
fdreResource domain =
  stateResource decodeFDREInitial (λ input state → state)
    domain fdreTransition

fdseResource : ∀ {Domain} → Domain
  → StateResource RegisterInitial FDSEInput Bit Domain Bit
fdseResource domain =
  stateResource decodeFDSEInitial (λ input state → state)
    domain fdseTransition

-- SRL16E's initializer is likewise typed semantic data.  Supporting this
-- adapter does not admit SRL16E cells or decode a raw INIT attribute.

SRL16EInitial : Type₀
SRL16EInitial = Maybe SRL16E.SRL16EState

decodeSRL16EInitial : SRL16EInitial → Maybe SRL16E.SRL16EState
decodeSRL16EInitial nothing      = just SRL16E.defaultInitialState
decodeSRL16EInitial (just state) = just state

record SRL16EInput : Type₀ where
  constructor srl16eInput
  field
    srl16eAddress : SRL16E.SRL16EAddress
    srl16eData    : Bit
    srl16eEnable  : Bit

open SRL16EInput public

srl16eObserve : SRL16EInput → SRL16E.SRL16EState → Bit
srl16eObserve input state =
  SRL16E.readSRL16E state (srl16eAddress input)

srl16eTransition : SRL16EInput → SRL16E.SRL16EState → SRL16E.SRL16EState
srl16eTransition input state =
  SRL16E.updateSRL16E Design.risingEdge
    (srl16eEnable input) (srl16eData input) state

srl16eResource : ∀ {Domain} → Domain
  → StateResource
      SRL16EInitial SRL16EInput Bit Domain SRL16E.SRL16EState
srl16eResource domain =
  stateResource decodeSRL16EInitial srl16eObserve
    domain srl16eTransition

-- Distributed RAM adapters retain address-indexed semantic initialization.
-- `nothing` selects only the primitive module's documented all-zero default;
-- arbitrary raw INIT text and undecoded raw address buses never enter here.

decodeTypedDefault : ∀ {State : Type₀}
  → State → Maybe State → Maybe State
decodeTypedDefault default-state nothing = just default-state
decodeTypedDefault default-state (just state) = just state

RAM32X1SInitial : Type₀
RAM32X1SInitial = Maybe RAM32X1S.RAM32X1SState

record RAM32X1SInput : Type₀ where
  constructor ram32x1sInput
  field
    ram32x1sAddress     : RAM32X1S.RAM32X1SAddress
    ram32x1sData        : Bit
    ram32x1sWriteEnable : Bit

open RAM32X1SInput public

ram32x1sObserve : RAM32X1SInput → RAM32X1S.RAM32X1SState → Bit
ram32x1sObserve input state =
  RAM32X1S.readRAM32X1S state (ram32x1sAddress input)

ram32x1sTransition :
  RAM32X1SInput → RAM32X1S.RAM32X1SState → RAM32X1S.RAM32X1SState
ram32x1sTransition input state =
  RAM32X1S.updateRAM32X1S Design.risingEdge
    (ram32x1sWriteEnable input) (ram32x1sAddress input)
    (ram32x1sData input) state

ram32x1sResource : ∀ {Domain} → Domain
  → StateResource
      RAM32X1SInitial RAM32X1SInput Bit Domain RAM32X1S.RAM32X1SState
ram32x1sResource domain =
  stateResource
    (decodeTypedDefault RAM32X1S.defaultInitialState)
    ram32x1sObserve domain ram32x1sTransition

RAM64X1SInitial : Type₀
RAM64X1SInitial = Maybe RAM64X1S.RAM64X1SState

record RAM64X1SInput : Type₀ where
  constructor ram64x1sInput
  field
    ram64x1sAddress     : RAM64X1S.RAM64X1SAddress
    ram64x1sData        : Bit
    ram64x1sWriteEnable : Bit

open RAM64X1SInput public

ram64x1sObserve : RAM64X1SInput → RAM64X1S.RAM64X1SState → Bit
ram64x1sObserve input state =
  RAM64X1S.readRAM64X1S state (ram64x1sAddress input)

ram64x1sTransition :
  RAM64X1SInput → RAM64X1S.RAM64X1SState → RAM64X1S.RAM64X1SState
ram64x1sTransition input state =
  RAM64X1S.updateRAM64X1S Design.risingEdge
    (ram64x1sWriteEnable input) (ram64x1sAddress input)
    (ram64x1sData input) state

ram64x1sResource : ∀ {Domain} → Domain
  → StateResource
      RAM64X1SInitial RAM64X1SInput Bit Domain RAM64X1S.RAM64X1SState
ram64x1sResource domain =
  stateResource
    (decodeTypedDefault RAM64X1S.defaultInitialState)
    ram64x1sObserve domain ram64x1sTransition

RAM128X1DInitial : Type₀
RAM128X1DInitial = Maybe RAM128X1D.RAM128X1DState

record RAM128X1DInput : Type₀ where
  constructor ram128x1dInput
  field
    ram128x1dWriteAddress    : RAM128X1D.RAM128X1DAAddress
    ram128x1dDualReadAddress : RAM128X1D.RAM128X1DDPRAAddress
    ram128x1dData            : Bit
    ram128x1dWriteEnable     : Bit

open RAM128X1DInput public

record RAM128X1DObservation : Type₀ where
  constructor ram128x1dObservation
  field
    ram128x1dSPO : Bit
    ram128x1dDPO : Bit

open RAM128X1DObservation public

ram128x1dObserve :
  RAM128X1DInput → RAM128X1D.RAM128X1DState → RAM128X1DObservation
ram128x1dObserve input state =
  ram128x1dObservation
    (RAM128X1D.readSPO state (ram128x1dWriteAddress input))
    (RAM128X1D.readDPO state (ram128x1dDualReadAddress input))

ram128x1dTransition :
  RAM128X1DInput → RAM128X1D.RAM128X1DState → RAM128X1D.RAM128X1DState
ram128x1dTransition input state =
  RAM128X1D.updateRAM128X1D Design.risingEdge
    (ram128x1dWriteEnable input) (ram128x1dWriteAddress input)
    (ram128x1dData input) state

ram128x1dResource : ∀ {Domain} → Domain
  → StateResource
      RAM128X1DInitial RAM128X1DInput RAM128X1DObservation
      Domain RAM128X1D.RAM128X1DState
ram128x1dResource domain =
  stateResource
    (decodeTypedDefault RAM128X1D.defaultInitialState)
    ram128x1dObserve domain ram128x1dTransition

RAM256X1SInitial : Type₀
RAM256X1SInitial = Maybe RAM256X1S.RAM256X1SState

record RAM256X1SInput : Type₀ where
  constructor ram256x1sInput
  field
    ram256x1sAddress     : RAM256X1S.RAM256X1SAddress
    ram256x1sData        : Bit
    ram256x1sWriteEnable : Bit

open RAM256X1SInput public

ram256x1sObserve : RAM256X1SInput → RAM256X1S.RAM256X1SState → Bit
ram256x1sObserve input state =
  RAM256X1S.readRAM256X1S state (ram256x1sAddress input)

ram256x1sTransition :
  RAM256X1SInput → RAM256X1S.RAM256X1SState → RAM256X1S.RAM256X1SState
ram256x1sTransition input state =
  RAM256X1S.updateRAM256X1S Design.risingEdge
    (ram256x1sWriteEnable input) (ram256x1sAddress input)
    (ram256x1sData input) state

ram256x1sResource : ∀ {Domain} → Domain
  → StateResource
      RAM256X1SInitial RAM256X1SInput Bit Domain RAM256X1S.RAM256X1SState
ram256x1sResource domain =
  stateResource
    (decodeTypedDefault RAM256X1S.defaultInitialState)
    ram256x1sObserve domain ram256x1sTransition

-- Block RAM has no invented default: its already-typed memory contents and
-- output latch are supplied together.  Observation exposes only the existing
-- synchronous output latch; the selected write mode is fixed by the resource.

blockRAMResource : ∀ {Domain depth width} → Domain → BlockRAM.WriteMode
  → StateResource
      (BlockRAM.SinglePortState depth width)
      (BlockRAM.PortCommand depth width)
      (Word width)
      Domain
      (BlockRAM.SinglePortState depth width)
blockRAMResource domain mode =
  stateResource just
    (λ command state → BlockRAM.outputLatch state)
    domain (BlockRAM.clockEdge mode)

-- The singleton-domain interpretation embeds the legacy idle/rising event.

singleClockEdges : Design.Event → EdgeSet Unit
singleClockEdges Design.idle       tt = low
singleClockEdges Design.risingEdge tt = high

fdreUpdate : Design.Event → FDREInput → Bit → Bit
fdreUpdate Design.idle       input state = state
fdreUpdate Design.risingEdge input state = fdreTransition input state

fdre-single-clock-recovery :
  ∀ event input state
  → stepResource (fdreResource tt) (singleClockEdges event) input state
  ≡ fdreUpdate event input state
fdre-single-clock-recovery Design.idle input state = refl
fdre-single-clock-recovery Design.risingEdge input state = refl

fdse-single-clock-recovery :
  ∀ event input state
  → stepResource (fdseResource tt) (singleClockEdges event) input state
  ≡ FDSE.fdseUpdate event
      (fdseData input) (fdseEnable input) (fdseSet input) state
fdse-single-clock-recovery Design.idle input state = refl
fdse-single-clock-recovery Design.risingEdge input state = refl

srl16e-single-clock-recovery :
  ∀ event input state
  → stepResource (srl16eResource tt) (singleClockEdges event) input state
  ≡ SRL16E.updateSRL16E event
      (srl16eEnable input) (srl16eData input) state
srl16e-single-clock-recovery Design.idle input state = refl
srl16e-single-clock-recovery Design.risingEdge
  (srl16eInput address false data-bit) state = refl
srl16e-single-clock-recovery Design.risingEdge
  (srl16eInput address true data-bit) state = refl

ram32x1s-single-clock-recovery :
  ∀ event input state
  → stepResource (ram32x1sResource tt) (singleClockEdges event) input state
  ≡ RAM32X1S.updateRAM32X1S event
      (ram32x1sWriteEnable input) (ram32x1sAddress input)
      (ram32x1sData input) state
ram32x1s-single-clock-recovery Design.idle input state = refl
ram32x1s-single-clock-recovery Design.risingEdge input state = refl

ram64x1s-single-clock-recovery :
  ∀ event input state
  → stepResource (ram64x1sResource tt) (singleClockEdges event) input state
  ≡ RAM64X1S.updateRAM64X1S event
      (ram64x1sWriteEnable input) (ram64x1sAddress input)
      (ram64x1sData input) state
ram64x1s-single-clock-recovery Design.idle input state = refl
ram64x1s-single-clock-recovery Design.risingEdge input state = refl

ram128x1d-single-clock-recovery :
  ∀ event input state
  → stepResource (ram128x1dResource tt) (singleClockEdges event) input state
  ≡ RAM128X1D.updateRAM128X1D event
      (ram128x1dWriteEnable input) (ram128x1dWriteAddress input)
      (ram128x1dData input) state
ram128x1d-single-clock-recovery Design.idle input state = refl
ram128x1d-single-clock-recovery Design.risingEdge input state = refl

ram256x1s-single-clock-recovery :
  ∀ event input state
  → stepResource (ram256x1sResource tt) (singleClockEdges event) input state
  ≡ RAM256X1S.updateRAM256X1S event
      (ram256x1sWriteEnable input) (ram256x1sAddress input)
      (ram256x1sData input) state
ram256x1s-single-clock-recovery Design.idle input state = refl
ram256x1s-single-clock-recovery Design.risingEdge input state = refl

blockRAMUpdate : ∀ {depth width}
  → Design.Event → BlockRAM.WriteMode
  → BlockRAM.PortCommand depth width
  → BlockRAM.SinglePortState depth width
  → BlockRAM.SinglePortState depth width
blockRAMUpdate Design.idle mode command state = state
blockRAMUpdate Design.risingEdge mode command state =
  BlockRAM.clockEdge mode command state

blockRAM-single-clock-recovery :
  ∀ {depth width} event mode
    (command : BlockRAM.PortCommand depth width) state
  → stepResource (blockRAMResource tt mode) (singleClockEdges event)
      command state
  ≡ blockRAMUpdate event mode command state
blockRAM-single-clock-recovery Design.idle mode command state = refl
blockRAM-single-clock-recovery Design.risingEdge mode command state = refl

-- Certified layouts are independent objects.  Registers use a one-bit
-- layout; SRL16E's existing semantic state already is the desired 16-bit
-- layout.

fdreBitLowering : ∀ {Domain} (domain : Domain)
  → CertifiedBitLowering (fdreResource domain) 1
encodeState (fdreBitLowering domain) state = state ∷ []
decodeState (fdreBitLowering domain) (state ∷ []) = state
decode-encode (fdreBitLowering domain) state = refl
observeBits (fdreBitLowering domain) input (state ∷ []) = state
observe-preserved (fdreBitLowering domain) input state = refl
transitionBits (fdreBitLowering domain) input (state ∷ []) =
  fdreTransition input state ∷ []
transition-preserved (fdreBitLowering domain) input state = refl

fdseBitLowering : ∀ {Domain} (domain : Domain)
  → CertifiedBitLowering (fdseResource domain) 1
encodeState (fdseBitLowering domain) state = state ∷ []
decodeState (fdseBitLowering domain) (state ∷ []) = state
decode-encode (fdseBitLowering domain) state = refl
observeBits (fdseBitLowering domain) input (state ∷ []) = state
observe-preserved (fdseBitLowering domain) input state = refl
transitionBits (fdseBitLowering domain) input (state ∷ []) =
  fdseTransition input state ∷ []
transition-preserved (fdseBitLowering domain) input state = refl

srl16eBitLowering : ∀ {Domain} (domain : Domain)
  → CertifiedBitLowering (srl16eResource domain) 16
encodeState (srl16eBitLowering domain) state = state
decodeState (srl16eBitLowering domain) state = state
decode-encode (srl16eBitLowering domain) state = refl
observeBits (srl16eBitLowering domain) input state =
  srl16eObserve input state
observe-preserved (srl16eBitLowering domain) input state = refl
transitionBits (srl16eBitLowering domain) input state =
  srl16eTransition input state
transition-preserved (srl16eBitLowering domain) input state = refl