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

module Spartan6.Examples.RawBuffers where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeCombinational 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 ∷ᴸ []ᴸ)

rawBUFGCE : Raw.RawInstance
rawBUFGCE =
  Raw.rawInstance
    "gated_clock"
    (Raw.knownPrimitive Architecture.BUFGCE)
    (inputPort "I" 0
     ∷ᴸ inputPort "CE" 1
     ∷ᴸ outputPort "O" 2
     ∷ᴸ []ᴸ)
    []ᴸ
    nothing

rawBUFGCEDesign : Raw.RawDesign
rawBUFGCEDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clock_in" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "enable" Raw.inputPort 1 (Raw.net 1 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "clock_out" Raw.outputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawBUFGCE ∷ᴸ []ᴸ)

raw-bufgce-is-structurally-valid :
  Validation.StructurallyValid rawBUFGCEDesign
raw-bufgce-is-structurally-valid = refl

clockIndex : Fin 2
clockIndex = fzero

enableIndex : Fin 2
enableIndex = fsuc fzero

bufgceNetlist : Checked.CheckedNetlist 2 1 0 1
bufgceNetlist =
  Checked.checkedNetlist
    []
    (Checked.noNodes Checked.▻
      Checked.muxNode
        (Checked.externalWire enableIndex)
        (Checked.literalWire low)
        (Checked.externalWire clockIndex))
    (Checked.localWire fzero ∷ [])
    []

bufgceCandidate : Normalize.CheckedCombinationalCandidate
bufgceCandidate =
  Normalize.checkedCombinationalCandidate
    rawBUFGCEDesign raw-bufgce-is-structurally-valid 2 1 1 bufgceNetlist

raw-bufgce-normalises :
  Normalize.normaliseCombinational
    (rawBUFGCEDesign , raw-bufgce-is-structurally-valid)
  ≡ Diagnostic.accepted bufgceCandidate
raw-bufgce-normalises = refl

compiledBUFGCE : Semantics.Design 2 1 0
compiledBUFGCE = Checked.compileNetlist bufgceNetlist

disabled-clock-is-low :
  Semantics.observe compiledBUFGCE (high ∷ low ∷ []) [] ≡ low ∷ []
disabled-clock-is-low = refl

enabled-clock-is-passed :
  Semantics.observe compiledBUFGCE (high ∷ high ∷ []) [] ≡ high ∷ []
enabled-clock-is-passed = refl

rawIBUF : Raw.RawInstance
rawIBUF =
  Raw.rawInstance
    "input_buffer"
    (Raw.knownPrimitive Architecture.IBUF)
    (inputPort "I" 10 ∷ᴸ outputPort "O" 11 ∷ᴸ []ᴸ)
    []ᴸ nothing

rawOBUF : Raw.RawInstance
rawOBUF =
  Raw.rawInstance
    "output_buffer"
    (Raw.knownPrimitive Architecture.OBUF)
    (inputPort "I" 11 ∷ᴸ outputPort "O" 12 ∷ᴸ []ᴸ)
    []ᴸ nothing

rawIOBufferDesign : Raw.RawDesign
rawIOBufferDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "pad_in" Raw.inputPort 1 (Raw.net 10 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "pad_out" Raw.outputPort 1 (Raw.net 12 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawIBUF ∷ᴸ rawOBUF ∷ᴸ []ᴸ)

raw-io-buffers-are-structurally-valid :
  Validation.StructurallyValid rawIOBufferDesign
raw-io-buffers-are-structurally-valid = refl

ioBufferNetlist : Checked.CheckedNetlist 1 1 0 0
ioBufferNetlist =
  Checked.checkedNetlist
    [] Checked.noNodes
    (Checked.externalWire fzero ∷ [])
    []

ioBufferCandidate : Normalize.CheckedCombinationalCandidate
ioBufferCandidate =
  Normalize.checkedCombinationalCandidate
    rawIOBufferDesign raw-io-buffers-are-structurally-valid
    1 1 0 ioBufferNetlist

raw-io-buffers-normalise-as-digital-aliases :
  Normalize.normaliseCombinational
    (rawIOBufferDesign , raw-io-buffers-are-structurally-valid)
  ≡ Diagnostic.accepted ioBufferCandidate
raw-io-buffers-normalise-as-digital-aliases = refl

compiledIOBuffers : Semantics.Design 1 1 0
compiledIOBuffers = Checked.compileNetlist ioBufferNetlist

io-buffer-chain-passes-high :
  Semantics.observe compiledIOBuffers (high ∷ []) [] ≡ high ∷ []
io-buffer-chain-passes-high = refl