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

module Spartan6.Examples.RawRegisters where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.AdmissionMixed as Admission
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeRegisters as Normalize
import Spartan6.Netlist.Raw as Raw
import Spartan6.Semantics.Design as Semantics
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

inputPort : String → Raw.Connection → Raw.RawPort
inputPort name connection =
  Raw.rawPort name Raw.inputPort 1 (connection ∷ᴸ []ᴸ)

outputPort : String → Raw.NetId → Raw.RawPort
outputPort name net-id =
  Raw.rawPort name Raw.outputPort 1 (Raw.net net-id ∷ᴸ []ᴸ)

rawSwapRegister : String → Raw.NetId → Raw.NetId → Bit → Raw.RawInstance
rawSwapRegister name q-net d-net initial-bit =
  Raw.rawInstance
    name
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "D" (Raw.net d-net)
     ∷ᴸ inputPort "C" (Raw.net 0)
     ∷ᴸ inputPort "CE" (Raw.constant high)
     ∷ᴸ inputPort "R" (Raw.constant low)
     ∷ᴸ outputPort "Q" q-net
     ∷ᴸ []ᴸ)
    []ᴸ
    (just initial-bit)

rawSwapDesign : Raw.RawDesign
rawSwapDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clock" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q0" Raw.outputPort 1 (Raw.net 10 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q1" Raw.outputPort 1 (Raw.net 11 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawSwapRegister "q0" 10 11 low
     ∷ᴸ rawSwapRegister "q1" 11 10 high
     ∷ᴸ []ᴸ)

raw-swap-is-structurally-valid :
  Validation.StructurallyValid rawSwapDesign
raw-swap-is-structurally-valid = refl

swapNetlist : Checked.CheckedNetlist 1 2 2 4
swapNetlist =
  Checked.checkedNetlist
    (low ∷ high ∷ [])
    ((((Checked.noNodes Checked.▻
      -- q1 enable stage is built first by tail recursion.
      Checked.muxNode
        (Checked.literalWire high)
        (Checked.storedWire (fsuc fzero))
        (Checked.storedWire fzero))
      Checked.▻
      -- q1 reset stage.
      Checked.muxNode
        (Checked.literalWire low)
        (Checked.localWire fzero)
        (Checked.literalWire low))
      Checked.▻
      -- q0 enable stage reads the same pre-event q1.
      Checked.muxNode
        (Checked.literalWire high)
        (Checked.storedWire fzero)
        (Checked.storedWire (fsuc fzero)))
      Checked.▻
      -- q0 reset stage.
      Checked.muxNode
        (Checked.literalWire low)
        (Checked.localWire fzero)
        (Checked.literalWire low))
    (Checked.storedWire fzero
     ∷ Checked.storedWire (fsuc fzero)
     ∷ [])
    (Checked.localWire fzero
     ∷ Checked.localWire (fsuc (fsuc fzero))
     ∷ [])

swapCandidate : Normalize.CheckedRegistersCandidate
swapCandidate =
  Normalize.checkedRegistersCandidate
    rawSwapDesign raw-swap-is-structurally-valid
    1 2 2 4 fzero swapNetlist

raw-registers-normalise :
  Normalize.normaliseRegisters
    (rawSwapDesign , raw-swap-is-structurally-valid)
  ≡ Diagnostic.accepted swapCandidate
raw-registers-normalise = refl

compiledSwap : Semantics.Design 1 2 2
compiledSwap = Checked.compileNetlist swapNetlist

initial-observation :
  Semantics.observe compiledSwap (low ∷ []) (Semantics.initial compiledSwap)
  ≡ low ∷ high ∷ []
initial-observation = refl

one-edge-swaps-simultaneously :
  Semantics.step compiledSwap Semantics.risingEdge
    (high ∷ [])
    (low ∷ high ∷ [])
  ≡ high ∷ low ∷ []
one-edge-swaps-simultaneously = refl

idle-keeps-both-registers :
  Semantics.step compiledSwap Semantics.idle
    (low ∷ [])
    (low ∷ high ∷ [])
  ≡ low ∷ high ∷ []
idle-keeps-both-registers = refl

secondClockRegister : Raw.RawInstance
secondClockRegister =
  Raw.rawInstance
    "q1"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "D" (Raw.net 10)
     ∷ᴸ inputPort "C" (Raw.net 1)
     ∷ᴸ inputPort "CE" (Raw.constant high)
     ∷ᴸ inputPort "R" (Raw.constant low)
     ∷ᴸ outputPort "Q" 11
     ∷ᴸ []ᴸ)
    []ᴸ
    (just high)

twoClockDesign : Raw.RawDesign
twoClockDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clock0" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "clock1" Raw.inputPort 1 (Raw.net 1 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q0" Raw.outputPort 1 (Raw.net 10 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q1" Raw.outputPort 1 (Raw.net 11 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawSwapRegister "q0" 10 11 low
     ∷ᴸ secondClockRegister
     ∷ᴸ []ᴸ)

two-clock-design-is-structurally-valid :
  Validation.StructurallyValid twoClockDesign
two-clock-design-is-structurally-valid = refl

multiple-clock-domains-are-rejected :
  Normalize.normaliseRegisters
    (twoClockDesign , two-clock-design-is-structurally-valid)
  ≡ Diagnostic.rejected
      (Normalize.singleton
        (Normalize.issue Diagnostic.unsupportedEvent
          "q1"
          "the same raw clock net for every register"
          "1"
          "Multiple clock domains/interleavings are outside the initial event model."))
multiple-clock-domains-are-rejected = refl

restricted-admission-preserves-two-clock-rejection :
  Admission.admitRestrictedMixed
    (twoClockDesign , two-clock-design-is-structurally-valid)
  ≡ Diagnostic.rejected
      (Normalize.singleton
        (Normalize.issue Diagnostic.unsupportedEvent
          "q1"
          "the same raw clock net for every register"
          "1"
          "Multiple clock domains/interleavings are outside the initial event model."))
restricted-admission-preserves-two-clock-rejection = refl