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

module Spartan6.Netlist.RegisterMode where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter

open import Cubical.Data.Nat using (_≡ᵇ_)

-- Scalar register schema and exact mode decoding, independent of every
-- whole-design register normalizer.

singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton item = item ∷ᴸ []ᴸ

issue : Diagnostic.DiagnosticCode → String → String → String → String
      → Diagnostic.Diagnostic
issue code subject expected observed detail =
  Diagnostic.diagnostic code Diagnostic.reject subject expected observed detail

lookupInputIndex : (net-id : Raw.NetId) (input-nets : List Raw.NetId)
                 → Maybe (Fin (lengthList input-nets))
lookupInputIndex net-id []ᴸ = nothing
lookupInputIndex net-id (candidate ∷ᴸ input-nets) =
  if net-id ≡ᵇ candidate
  then just fzero
  else liftIndex (lookupInputIndex net-id input-nets)
  where
  liftIndex : Maybe (Fin (lengthList input-nets))
            → Maybe (Fin (suc (lengthList input-nets)))
  liftIndex nothing = nothing
  liftIndex (just index) = just (fsuc index)

record RegisterPorts : Type₀ where
  constructor registerPorts
  field
    registerD       : Raw.RawPort
    registerC       : Raw.RawPort
    registerCE      : Raw.RawPort
    registerControl : Raw.RawPort
    registerQ       : Raw.RawPort

open RegisterPorts public

parseRegisterPorts : List Raw.RawPort → Maybe RegisterPorts
parseRegisterPorts
  (data-port ∷ᴸ clock-port ∷ᴸ enable-port ∷ᴸ control-port
   ∷ᴸ output-port ∷ᴸ []ᴸ) =
  just
    (registerPorts
      data-port clock-port enable-port control-port output-port)
parseRegisterPorts ports = nothing

outputNet : Raw.RawInstance → RegisterPorts
          → Diagnostic.CheckResult Raw.NetId
outputNet item ports with Raw.rawPortConnections (registerQ ports)
... | Raw.net net-id ∷ᴸ []ᴸ = Diagnostic.accepted net-id
... | Raw.constant bit ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.directionMismatch (Raw.rawInstanceName item)
        "Q driving a net" "Q bound to a constant"
        "A storage output is a driver, not a constant sink."))
... | Raw.disconnected ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedMode (Raw.rawInstanceName item)
        "a retained Q net" "a discarded Q output"
        "The single-register correspondence requires the state output net."))
... | connections =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch (Raw.rawInstanceName item)
        "one scalar Q connection" "a non-scalar Q connection list"
        "The checked register interface is scalar."))

data RegisterMode : Type₀ where
  fdreMode : Bit → RegisterMode
  fdseMode : Bit → RegisterMode

modeInitial : RegisterMode → Bit
modeInitial (fdreMode initial-bit) = initial-bit
modeInitial (fdseMode initial-bit) = initial-bit

modeForcedValue : RegisterMode → Bit
modeForcedValue (fdreMode initial-bit) = low
modeForcedValue (fdseMode initial-bit) = high

normaliseFDREMode : Raw.RawInstance
                  → Diagnostic.CheckResult RegisterMode
normaliseFDREMode item with
  Parameter.normaliseCoreParameters
    Architecture.FDRE
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.fdreParameters initial-bit) =
  Diagnostic.accepted (fdreMode initial-bit)

normaliseFDSEMode : Raw.RawInstance
                  → Diagnostic.CheckResult RegisterMode
normaliseFDSEMode item with
  Parameter.normaliseCoreParameters
    Architecture.FDSE
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.fdseParameters initial-bit) =
  Diagnostic.accepted (fdseMode initial-bit)

normaliseRegisterMode : Raw.RawInstance
                      → Diagnostic.CheckResult RegisterMode
normaliseRegisterMode item with Raw.rawInstanceKind item
... | Raw.unknownPrimitive name =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unknownPrimitive (Raw.rawInstanceName item)
        "FDRE or FDSE" name "Unknown storage has no checked transition rule."))
... | Raw.knownPrimitive Architecture.FDRE = normaliseFDREMode item
... | Raw.knownPrimitive Architecture.FDSE = normaliseFDSEMode item
... | Raw.knownPrimitive kind =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedMode (Raw.rawInstanceName item)
        "exactly one FDRE or FDSE" "another primitive kind"
        "This initial sequential translation slice handles one synchronous scalar register only."))