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

module Spartan6.Examples.Admission where

open import Spartan6.Prelude

import Spartan6.Examples.RawRegisters as RegistersExample
import Spartan6.Examples.RawScheduledCombinational as PureExample
import Spartan6.Examples.RawToggle as MixedExample
import Spartan6.Netlist.AdmissionCombinational as PureAdmission
import Spartan6.Netlist.AdmissionCore as Core
import Spartan6.Netlist.NormalizeRegisters as Registers
import Spartan6.Semantics.Design as Semantics
import Spartan6.Validation.Diagnostic as Diagnostic

-- The public restricted core chooses the scheduled zero-register route for a
-- pure netlist and the scheduled common-clock route when FDRE/FDSE instances
-- are present.  These examples pin both dispatch paths and their executable
-- width indices.

pureProfile :
  PureAdmission.RestrictedCombinationalProfile
    PureExample.forwardReferenceDesign
pureProfile =
  PureAdmission.restrictedCombinationalProfile
    PureExample.forward-reference-is-acyclic-and-structurally-valid
    PureExample.forwardReferenceCandidate
    PureExample.acyclic-forward-reference-schedules-and-normalises
    PureExample.forwardReferenceWitness
    PureAdmission.restrictedCombinationalCandidate

pureAdmission : PureAdmission.RestrictedCombinationalAdmission
pureAdmission = PureExample.forwardReferenceDesign , pureProfile

pure-forward-reference-is-core-admitted :
  Core.admitRestrictedCore
    ( PureExample.forwardReferenceDesign
    , PureExample.forward-reference-is-acyclic-and-structurally-valid
    )
  ≡ Diagnostic.accepted
      (Core.admittedCombinational pureAdmission)
pure-forward-reference-is-core-admitted = refl

mixed-toggle-is-core-admitted :
  Core.admitRestrictedCore
    ( MixedExample.rawToggleDesign
    , MixedExample.raw-toggle-is-structurally-valid
    )
  ≡ Diagnostic.accepted
      (Core.admittedMixed MixedExample.raw-toggle-admission)
mixed-toggle-is-core-admitted = refl

pureExecutable : Core.ExecutableCore
pureExecutable =
  Core.admittedExecutable (Core.admittedCombinational pureAdmission)

mixedExecutable : Core.ExecutableCore
mixedExecutable =
  Core.admittedExecutable
    (Core.admittedMixed MixedExample.raw-toggle-admission)

pure-executable-input-count :
  Core.executableInputCount pureExecutable ≡ 
pure-executable-input-count = refl

pure-executable-output-count :
  Core.executableOutputCount pureExecutable ≡ 
pure-executable-output-count = refl

pure-executable-register-count :
  Core.executableRegisterCount pureExecutable ≡ 
pure-executable-register-count = refl

mixed-executable-input-count :
  Core.executableInputCount mixedExecutable ≡ 
mixed-executable-input-count = refl

mixed-executable-output-count :
  Core.executableOutputCount mixedExecutable ≡ 
mixed-executable-output-count = refl

mixed-executable-register-count :
  Core.executableRegisterCount mixedExecutable ≡ 
mixed-executable-register-count = refl

pure-admitted-semantics-passes-high :
  Semantics.observe
    (Core.executableDesign pureExecutable)
    (high ∷ []) []
  ≡ high ∷ []
pure-admitted-semantics-passes-high = refl

mixed-admitted-semantics-toggles :
  Semantics.step
    (Core.executableDesign mixedExecutable)
    Semantics.risingEdge
    (high ∷ low ∷ [])
    (low ∷ [])
  ≡ high ∷ []
mixed-admitted-semantics-toggles = refl

-- Dispatch does not hide a mixed-route common-clock failure.

two-clock-core-admission-is-rejected :
  Core.admitRestrictedCore
    ( RegistersExample.twoClockDesign
    , RegistersExample.two-clock-design-is-structurally-valid
    )
  ≡ Diagnostic.rejected
      (Registers.singleton
        (Registers.issue Diagnostic.unsupportedEvent
          "q1"
          "the same raw clock net for every register"
          "1"
          "Multiple clock domains/interleavings are outside the initial event model."))
two-clock-core-admission-is-rejected = refl