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

module Spartan6.Examples.RawToggle 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.NormalizeMixed as Normalize
import Spartan6.Netlist.NormalizeMixedSoundness as Soundness
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.Schedule as Schedule
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  (connection ∷ᴸ []ᴸ)

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

rawToggleRegister : Raw.RawInstance
rawToggleRegister =
  Raw.rawInstance
    "toggle.q"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "D" (Raw.net )
     ∷ᴸ inputPort "C" (Raw.net )
     ∷ᴸ inputPort "CE" (Raw.constant high)
     ∷ᴸ inputPort "R" (Raw.net )
     ∷ᴸ outputPort "Q" 
     ∷ᴸ []ᴸ)
    []ᴸ
    (just low)

rawToggleInverter : Raw.RawInstance
rawToggleInverter =
  Raw.rawInstance
    "toggle.next"
    (Raw.knownPrimitive Architecture.LUT1)
    (inputPort "I0" (Raw.net )
     ∷ᴸ outputPort "O" 
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "1" ∷ᴸ []ᴸ)
    nothing

-- Register appears before its D-driving combinational instance.  Partitioning
-- allocates Q first and the scheduler certifies the retained combinational
-- occurrence, so this source order is accepted without assigning traversal
-- order to the sequential transition.

rawToggleDesign : Raw.RawDesign
rawToggleDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clock" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "reset" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q" Raw.outputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawToggleRegister ∷ᴸ rawToggleInverter ∷ᴸ []ᴸ)

raw-toggle-is-structurally-valid :
  Validation.StructurallyValid rawToggleDesign
raw-toggle-is-structurally-valid = refl

clockIndex resetIndex : Fin 
clockIndex = fzero
resetIndex = fsuc fzero

toggleNetlist : Checked.CheckedNetlist    
toggleNetlist =
  Checked.checkedNetlist
    (low ∷ [])
    (((Checked.noNodes Checked.▻
      Checked.lutNode
        (high ∷ low ∷ [])
        (Checked.storedWire fzero ∷ []))
      Checked.▻
      Checked.muxNode
        (Checked.literalWire high)
        (Checked.storedWire fzero)
        (Checked.localWire fzero))
      Checked.▻
      Checked.muxNode
        (Checked.externalWire resetIndex)
        (Checked.localWire fzero)
        (Checked.literalWire low))
    (Checked.storedWire fzero ∷ [])
    (Checked.localWire fzero ∷ [])

toggleCandidate : Normalize.CheckedMixedCandidate
toggleCandidate =
  Normalize.checkedMixedCandidate
    rawToggleDesign raw-toggle-is-structurally-valid
        clockIndex toggleNetlist

raw-toggle-normalises :
  Normalize.normaliseMixed
    (rawToggleDesign , raw-toggle-is-structurally-valid)
  ≡ Diagnostic.accepted toggleCandidate
raw-toggle-normalises = refl

raw-toggle-witness :
  Soundness.MixedBuildWitness
    rawToggleDesign raw-toggle-is-structurally-valid toggleCandidate
raw-toggle-witness =
  Soundness.normaliseMixed-witness
    (rawToggleDesign , raw-toggle-is-structurally-valid)
    toggleCandidate
    raw-toggle-normalises

raw-toggle-boundary-is-exact :
  Soundness.candidateBoundary toggleCandidate
  ≡ (rawToggleDesign , raw-toggle-is-structurally-valid)
raw-toggle-boundary-is-exact =
  Soundness.candidate-boundary-preserved raw-toggle-witness

raw-toggle-common-clock-is-retained-input :
  Soundness.candidateInputClock toggleCandidate ≡ ( , clockIndex)
raw-toggle-common-clock-is-retained-input =
  Soundness.candidate-clock-matches-common raw-toggle-witness

raw-toggle-restricted-profile :
  Admission.RestrictedMixedProfile rawToggleDesign
raw-toggle-restricted-profile =
  Admission.restrictedMixedProfile
    raw-toggle-is-structurally-valid
    toggleCandidate
    raw-toggle-normalises
    raw-toggle-witness
    Admission.restrictedTranslationCandidate

raw-toggle-admission : Admission.RestrictedMixedAdmission
raw-toggle-admission =
  rawToggleDesign , raw-toggle-restricted-profile

raw-toggle-is-restricted-admitted :
  Admission.admitRestrictedMixed
    (rawToggleDesign , raw-toggle-is-structurally-valid)
  ≡ Diagnostic.accepted raw-toggle-admission
raw-toggle-is-restricted-admitted = refl

-- Scheduler regression: the consumer deliberately precedes its producer in
-- the retained combinational subsequence.  The dependency is acyclic because
-- the producer reads allocated register state; scheduling selects the
-- producer occurrence first and the mixed translator then builds both nodes.

forwardScheduledRegister : Raw.RawInstance
forwardScheduledRegister =
  Raw.rawInstance
    "forward.q"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "D" (Raw.net )
     ∷ᴸ inputPort "C" (Raw.net )
     ∷ᴸ inputPort "CE" (Raw.constant high)
     ∷ᴸ inputPort "R" (Raw.net )
     ∷ᴸ outputPort "Q" 
     ∷ᴸ []ᴸ)
    []ᴸ
    (just low)

forwardScheduledConsumer : Raw.RawInstance
forwardScheduledConsumer =
  Raw.rawInstance
    "forward.consumer"
    (Raw.knownPrimitive Architecture.LUT1)
    (inputPort "I0" (Raw.net )
     ∷ᴸ outputPort "O" 
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "2" ∷ᴸ []ᴸ)
    nothing

forwardScheduledProducer : Raw.RawInstance
forwardScheduledProducer =
  Raw.rawInstance
    "forward.producer"
    (Raw.knownPrimitive Architecture.LUT1)
    (inputPort "I0" (Raw.net )
     ∷ᴸ outputPort "O" 
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "1" ∷ᴸ []ᴸ)
    nothing

forwardScheduledDesign : Raw.RawDesign
forwardScheduledDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clock" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "reset" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "q" Raw.outputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (forwardScheduledRegister
     ∷ᴸ forwardScheduledConsumer
     ∷ᴸ forwardScheduledProducer
     ∷ᴸ []ᴸ)

forward-scheduled-is-structurally-valid :
  Validation.StructurallyValid forwardScheduledDesign
forward-scheduled-is-structurally-valid = refl

forwardScheduledNetlist : Checked.CheckedNetlist    
forwardScheduledNetlist =
  Checked.checkedNetlist
    (low ∷ [])
    ((((Checked.noNodes Checked.▻
      Checked.lutNode
        (high ∷ low ∷ [])
        (Checked.storedWire fzero ∷ []))
      Checked.▻
      Checked.lutNode
        (low ∷ high ∷ [])
        (Checked.localWire fzero ∷ []))
      Checked.▻
      Checked.muxNode
        (Checked.literalWire high)
        (Checked.storedWire fzero)
        (Checked.localWire fzero))
      Checked.▻
      Checked.muxNode
        (Checked.externalWire resetIndex)
        (Checked.localWire fzero)
        (Checked.literalWire low))
    (Checked.storedWire fzero ∷ [])
    (Checked.localWire fzero ∷ [])

forwardScheduledCandidate : Normalize.CheckedMixedCandidate
forwardScheduledCandidate =
  Normalize.checkedMixedCandidate
    forwardScheduledDesign forward-scheduled-is-structurally-valid
        clockIndex forwardScheduledNetlist

acyclic-forward-reference-now-normalises :
  Normalize.normaliseMixed
    (forwardScheduledDesign , forward-scheduled-is-structurally-valid)
  ≡ Diagnostic.accepted forwardScheduledCandidate
acyclic-forward-reference-now-normalises = refl

forwardScheduledWitness :
  Soundness.MixedBuildWitness
    forwardScheduledDesign
    forward-scheduled-is-structurally-valid
    forwardScheduledCandidate
forwardScheduledWitness =
  Soundness.normaliseMixed-witness
    (forwardScheduledDesign , forward-scheduled-is-structurally-valid)
    forwardScheduledCandidate
    acyclic-forward-reference-now-normalises

forward-reference-is-reordered-by-occurrence :
  Schedule.scheduledInstances
    (Soundness.scheduledCombinational forwardScheduledWitness)
  ≡ forwardScheduledProducer
    ∷ᴸ forwardScheduledConsumer ∷ᴸ []ᴸ
forward-reference-is-reordered-by-occurrence = refl

compiledToggle : Semantics.Design   
compiledToggle = Checked.compileNetlist toggleNetlist

admitted-toggle-semantics-is-compiled :
  Admission.admittedSemantics raw-toggle-restricted-profile
  ≡ compiledToggle
admitted-toggle-semantics-is-compiled = refl

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

first-edge-toggles-high :
  Semantics.step compiledToggle Semantics.risingEdge
    (high ∷ low ∷ [])
    (low ∷ [])
  ≡ high ∷ []
first-edge-toggles-high = refl

second-edge-toggles-low :
  Semantics.step compiledToggle Semantics.risingEdge
    (high ∷ low ∷ [])
    (high ∷ [])
  ≡ low ∷ []
second-edge-toggles-low = refl

reset-overrides-feedback :
  Semantics.step compiledToggle Semantics.risingEdge
    (high ∷ high ∷ [])
    (high ∷ [])
  ≡ low ∷ []
reset-overrides-feedback = refl

tick : Semantics.Stimulus 
tick = Semantics.stimulus (high ∷ low ∷ []) Semantics.risingEdge

two-ticks-return-to-initial :
  Semantics.run compiledToggle (Semantics.initial compiledToggle)
    (tick ∷ᴸ tick ∷ᴸ []ᴸ)
  ≡ low ∷ []
two-ticks-return-to-initial = refl