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

module Spartan6.Examples.RawRegister where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeRegister 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.NetId → Raw.RawPort
inputPort name net-id =
  Raw.rawPort name Raw.inputPort 1 (Raw.net net-id ∷ᴸ []ᴸ)

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

rawFDRE : Raw.RawInstance
rawFDRE =
  Raw.rawInstance
    "q"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "D" 0
     ∷ᴸ inputPort "C" 1
     ∷ᴸ inputPort "CE" 2
     ∷ᴸ inputPort "R" 3
     ∷ᴸ outputPort "Q" 4
     ∷ᴸ []ᴸ)
    []ᴸ
    nothing

rawRegisterDesign : Raw.RawDesign
rawRegisterDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "data" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "clock" Raw.inputPort 1 (Raw.net 1 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "enable" Raw.inputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "reset" Raw.inputPort 1 (Raw.net 3 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q" Raw.outputPort 1 (Raw.net 4 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawFDRE ∷ᴸ []ᴸ)

raw-register-is-structurally-valid :
  Validation.StructurallyValid rawRegisterDesign
raw-register-is-structurally-valid = refl

dataIndex clockIndex enableIndex resetIndex : Fin 4
dataIndex = fzero
clockIndex = fsuc fzero
enableIndex = fsuc (fsuc fzero)
resetIndex = fsuc (fsuc (fsuc fzero))

registerNetlist : Checked.CheckedNetlist 4 1 1 2
registerNetlist =
  Checked.checkedNetlist
    (low ∷ [])
    ((Checked.noNodes Checked.▻
      Checked.muxNode
        (Checked.externalWire enableIndex)
        (Checked.storedWire fzero)
        (Checked.externalWire dataIndex))
     Checked.▻
      Checked.muxNode
        (Checked.externalWire resetIndex)
        (Checked.localWire fzero)
        (Checked.literalWire low))
    (Checked.storedWire fzero ∷ [])
    (Checked.localWire fzero ∷ [])

registerCandidate : Normalize.CheckedRegisterCandidate
registerCandidate =
  Normalize.checkedRegisterCandidate
    rawRegisterDesign
    raw-register-is-structurally-valid
    4 1 clockIndex registerNetlist

raw-register-normalises :
  Normalize.normaliseSingleRegister
    (rawRegisterDesign , raw-register-is-structurally-valid)
  ≡ Diagnostic.accepted registerCandidate
raw-register-normalises = refl

compiledRegister : Semantics.Design 4 1 1
compiledRegister = Checked.compileNetlist registerNetlist

initial-output-is-low :
  Semantics.observe compiledRegister
    (low ∷ low ∷ low ∷ low ∷ [])
    (Semantics.initial compiledRegister)
  ≡ low ∷ []
initial-output-is-low = refl

enabled-rising-edge-loads :
  Semantics.step compiledRegister Semantics.risingEdge
    (high ∷ high ∷ high ∷ low ∷ [])
    (low ∷ [])
  ≡ high ∷ []
enabled-rising-edge-loads = refl

reset-overrides-enable-and-data :
  Semantics.step compiledRegister Semantics.risingEdge
    (high ∷ high ∷ high ∷ high ∷ [])
    (high ∷ [])
  ≡ low ∷ []
reset-overrides-enable-and-data = refl

idle-event-holds :
  Semantics.step compiledRegister Semantics.idle
    (low ∷ low ∷ low ∷ high ∷ [])
    (high ∷ [])
  ≡ high ∷ []
idle-event-holds = refl

rawFDSE : Raw.RawInstance
rawFDSE =
  Raw.rawInstance
    "q_set"
    (Raw.knownPrimitive Architecture.FDSE)
    (inputPort "D" 0
     ∷ᴸ inputPort "C" 1
     ∷ᴸ inputPort "CE" 2
     ∷ᴸ inputPort "S" 3
     ∷ᴸ outputPort "Q" 4
     ∷ᴸ []ᴸ)
    []ᴸ
    nothing

rawSetRegisterDesign : Raw.RawDesign
rawSetRegisterDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "data" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "clock" Raw.inputPort 1 (Raw.net 1 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "enable" Raw.inputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "set" Raw.inputPort 1 (Raw.net 3 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q" Raw.outputPort 1 (Raw.net 4 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawFDSE ∷ᴸ []ᴸ)

raw-set-register-is-structurally-valid :
  Validation.StructurallyValid rawSetRegisterDesign
raw-set-register-is-structurally-valid = refl

setRegisterNetlist : Checked.CheckedNetlist 4 1 1 2
setRegisterNetlist =
  Checked.checkedNetlist
    (high ∷ [])
    ((Checked.noNodes Checked.▻
      Checked.muxNode
        (Checked.externalWire enableIndex)
        (Checked.storedWire fzero)
        (Checked.externalWire dataIndex))
     Checked.▻
      Checked.muxNode
        (Checked.externalWire resetIndex)
        (Checked.localWire fzero)
        (Checked.literalWire high))
    (Checked.storedWire fzero ∷ [])
    (Checked.localWire fzero ∷ [])

setRegisterCandidate : Normalize.CheckedRegisterCandidate
setRegisterCandidate =
  Normalize.checkedRegisterCandidate
    rawSetRegisterDesign
    raw-set-register-is-structurally-valid
    4 1 clockIndex setRegisterNetlist

raw-set-register-normalises :
  Normalize.normaliseSingleRegister
    (rawSetRegisterDesign , raw-set-register-is-structurally-valid)
  ≡ Diagnostic.accepted setRegisterCandidate
raw-set-register-normalises = refl

compiledSetRegister : Semantics.Design 4 1 1
compiledSetRegister = Checked.compileNetlist setRegisterNetlist

fdse-default-output-is-high :
  Semantics.observe compiledSetRegister
    (low ∷ low ∷ low ∷ low ∷ [])
    (Semantics.initial compiledSetRegister)
  ≡ high ∷ []
fdse-default-output-is-high = refl

set-overrides-enable-and-data :
  Semantics.step compiledSetRegister Semantics.risingEdge
    (low ∷ high ∷ low ∷ high ∷ [])
    (low ∷ [])
  ≡ high ∷ []
set-overrides-enable-and-data = refl