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

module Spartan6.Examples.RawScheduledCombinational where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeCombinational as Combinational
import Spartan6.Netlist.NormalizeScheduledCombinational as Normalize
import Spartan6.Netlist.NormalizeScheduledCombinationalSoundness 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 1 (connection ∷ᴸ []ᴸ)

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

identityLUT1 : String → Raw.NetId → Raw.NetId → Raw.RawInstance
identityLUT1 name input-net output-net =
  Raw.rawInstance
    name
    (Raw.knownPrimitive Architecture.LUT1)
    (inputPort "I0" (Raw.net input-net)
     ∷ᴸ outputPort "O" output-net
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "2" ∷ᴸ []ᴸ)
    nothing

consumer producer : Raw.RawInstance
consumer = identityLUT1 "forward.consumer" 1 2
producer = identityLUT1 "forward.producer" 0 1

-- The consumer occurs first but depends on the producer.  Structural cycle
-- checking accepts the graph, and the scheduler can select the producer
-- occurrence without treating acyclicity itself as a completeness theorem.

forwardReferenceDesign : Raw.RawDesign
forwardReferenceDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (consumer ∷ᴸ producer ∷ᴸ []ᴸ)

forward-reference-is-acyclic-and-structurally-valid :
  Validation.StructurallyValid forwardReferenceDesign
forward-reference-is-acyclic-and-structurally-valid = refl

forwardReferenceNetlist : Checked.CheckedNetlist 1 1 0 2
forwardReferenceNetlist =
  Checked.checkedNetlist
    []
    ((Checked.noNodes Checked.▻
      Checked.lutNode
        (low ∷ high ∷ [])
        (Checked.externalWire fzero ∷ []))
      Checked.▻
      Checked.lutNode
        (low ∷ high ∷ [])
        (Checked.localWire fzero ∷ []))
    (Checked.localWire fzero ∷ [])
    []

forwardReferenceCandidate :
  Combinational.CheckedCombinationalCandidate
forwardReferenceCandidate =
  Combinational.checkedCombinationalCandidate
    forwardReferenceDesign
    forward-reference-is-acyclic-and-structurally-valid
    1 1 2 forwardReferenceNetlist

acyclic-forward-reference-schedules-and-normalises :
  Normalize.normaliseScheduledCombinational
    (forwardReferenceDesign
    , forward-reference-is-acyclic-and-structurally-valid)
  ≡ Diagnostic.accepted forwardReferenceCandidate
acyclic-forward-reference-schedules-and-normalises = refl

forwardReferenceWitness :
  Soundness.ScheduledCombinationalBuildWitness
    forwardReferenceDesign
    forward-reference-is-acyclic-and-structurally-valid
    forwardReferenceCandidate
forwardReferenceWitness =
  Soundness.normaliseScheduledCombinational-witness
    (forwardReferenceDesign
    , forward-reference-is-acyclic-and-structurally-valid)
    forwardReferenceCandidate
    acyclic-forward-reference-schedules-and-normalises

forward-reference-scheduled-producer-first :
  Schedule.scheduledInstances (Soundness.scheduled forwardReferenceWitness)
  ≡ producer ∷ᴸ consumer ∷ᴸ []ᴸ
forward-reference-scheduled-producer-first = refl

forward-reference-boundary-is-exact :
  Soundness.candidateBoundary forwardReferenceCandidate
  ≡
    (forwardReferenceDesign
    , forward-reference-is-acyclic-and-structurally-valid)
forward-reference-boundary-is-exact =
  Soundness.candidate-boundary-preserved forwardReferenceWitness

compiledForwardReference : Semantics.Design 1 1 0
compiledForwardReference = Checked.compileNetlist forwardReferenceNetlist

scheduled-forward-reference-passes-low :
  Semantics.observe compiledForwardReference (low ∷ []) []
  ≡ low ∷ []
scheduled-forward-reference-passes-low = refl

scheduled-forward-reference-passes-high :
  Semantics.observe compiledForwardReference (high ∷ []) []
  ≡ high ∷ []
scheduled-forward-reference-passes-high = refl