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

module Spartan6.Examples.RawMux 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 ∷ᴸ []ᴸ)

rawMUXF7 : Raw.RawInstance
rawMUXF7 =
  Raw.rawInstance
    "mux"
    (Raw.knownPrimitive Architecture.MUXF7)
    (inputPort "I0" 0
     ∷ᴸ inputPort "I1" 1
     ∷ᴸ inputPort "S" 2
     ∷ᴸ outputPort "O" 3
     ∷ᴸ []ᴸ)
    []ᴸ
    nothing

rawMuxDesign : Raw.RawDesign
rawMuxDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input0" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "input1" Raw.inputPort 1 (Raw.net 1 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "select" Raw.inputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort 1 (Raw.net 3 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawMUXF7 ∷ᴸ []ᴸ)

raw-mux-is-structurally-valid : Validation.StructurallyValid rawMuxDesign
raw-mux-is-structurally-valid = refl

input0Index : Fin 3
input0Index = fzero

input1Index : Fin 3
input1Index = fsuc fzero

selectIndex : Fin 3
selectIndex = fsuc (fsuc fzero)

muxNetlist : Checked.CheckedNetlist 3 1 0 1
muxNetlist =
  Checked.checkedNetlist
    []
    (Checked.noNodes Checked.▻
      Checked.muxNode
        (Checked.externalWire selectIndex)
        (Checked.externalWire input0Index)
        (Checked.externalWire input1Index))
    (Checked.localWire fzero ∷ [])
    []

muxCandidate : Normalize.CheckedCombinationalCandidate
muxCandidate =
  Normalize.checkedCombinationalCandidate
    rawMuxDesign raw-mux-is-structurally-valid 3 1 1 muxNetlist

raw-mux-normalises :
  Normalize.normaliseCombinational
    (rawMuxDesign , raw-mux-is-structurally-valid)
  ≡ Diagnostic.accepted muxCandidate
raw-mux-normalises = refl

compiledMux : Semantics.Design 3 1 0
compiledMux = Checked.compileNetlist muxNetlist

select-low-chooses-input0 :
  Semantics.observe compiledMux (high ∷ low ∷ low ∷ []) [] ≡ high ∷ []
select-low-chooses-input0 = refl

select-high-chooses-input1 :
  Semantics.observe compiledMux (low ∷ high ∷ high ∷ []) [] ≡ high ∷ []
select-high-chooses-input1 = refl